Z3分段错误 [英] Z3 Segmentation Fault

问题描述

我编写了以下 Perl 脚本来生成 smt2 格式的逻辑约束，以解决给定输入文件的数独难题.输入文件格式如下:

I have written the following Perl script to generate the logical constraints in smt2 format to solve a sudoku puzzle for a given input file. The input file is in this format:

5 3 * * 7 * * * *
6 * * 1 9 5 * * *
* 9 8 * * * * 6 *
8 * * * 6 * * * 3
4 * * 8 * 3 * * 1
7 * * * 2 * * * 6
* 6 * * * * 2 8 *
* * * 4 1 9 * * 5
* * * * 8 * * 7 9

丑陋的 Perl 脚本是:

The big ugly Perl script is:

#! /usr/local/bin/perl

# CSC 410 A2 Q2
# Sudoku

use strict;
use warnings;

# All of the indices in a sudoku array
my @row1 = qw(r1c1 r1c2 r1c3 r1c4 r1c5 r1c6 r1c7 r1c8 r1c9);
my @row2 = qw(r2c1 r2c2 r2c3 r2c4 r2c5 r2c6 r2c7 r2c8 r2c9);
my @row3 = qw(r3c1 r3c2 r3c3 r3c4 r3c5 r3c6 r3c7 r3c8 r3c9);
my @row4 = qw(r4c1 r4c2 r4c3 r4c4 r4c5 r4c6 r4c7 r4c8 r4c9);
my @row5 = qw(r5c1 r5c2 r5c3 r5c4 r5c5 r5c6 r5c7 r5c8 r5c9);
my @row6 = qw(r6c1 r6c2 r6c3 r6c4 r6c5 r6c6 r6c7 r6c8 r6c9);
my @row7 = qw(r7c1 r7c2 r7c3 r7c4 r7c5 r7c6 r7c7 r7c8 r7c9);
my @row8 = qw(r8c1 r8c2 r8c3 r8c4 r8c5 r8c6 r8c7 r8c8 r8c9);
my @row9 = qw(r9c1 r9c2 r9c3 r9c4 r9c5 r9c6 r9c7 r9c8 r9c9);

my @rows = (\@row1, \@row2, \@row3, \@row4, \@row5, \@row6, \@row7, \@row8, \@row9);

# All of the indices in a sudoku block
my @block1 = qw(r1c1 r1c2 r1c3 r2c1 r2c2 r2c3 r3c1 r3c2 r3c3);
my @block2 = qw(r1c4 r1c5 r1c6 r2c4 r2c5 r2c6 r3c4 r3c5 r3c6);
my @block3 = qw(r1c7 r1c8 r1c9 r2c7 r2c8 r2c9 r3c7 r3c8 r3c9);
my @block4 = qw(r4c1 r4c2 r4c3 r5c1 r5c2 r5c3 r6c1 r6c2 r6c3);
my @block5 = qw(r4c4 r4c5 r4c6 r5c4 r5c5 r5c6 r6c4 r6c5 r6c6);
my @block6 = qw(r4c7 r4c8 r4c9 r5c7 r5c8 r5c9 r6c7 r6c8 r6c9);
my @block7 = qw(r7c1 r7c2 r7c3 r8c1 r8c2 r8c3 r9c1 r9c2 r9c3);
my @block8 = qw(r7c4 r7c5 r7c6 r8c4 r8c5 r8c6 r9c4 r9c5 r9c6);
my @block9 = qw(r7c7 r7c8 r7c9 r8c7 r8c8 r8c9 r9c7 r9c8 r9c9);

my @blocks = (\@block1, \@block2, \@block3, \@block4, \@block5, \@block6, \@block7,   \@block8, \@block9);

open (FORMULA, ">", "sudoku.smt2") or die $!;

my $var;
my $i;
my $r;
my $c;

print (FORMULA "; Declare integers constants.\n");
for ($r = 0; $r < 9; $r++)
{
   for ($c = 0; $c < 9; $c++)
   {
      print (FORMULA "(declare-const $rows[$r][$c] Int)\n");
   }
}
print (FORMULA "\n");

print (FORMULA "; Assert for each variable r_ic_j that 1 <= r_ic_j <= 9\n");
for ($r = 0; $r < 9; $r++)
{
   for ($c = 0; $c < 9; $c++)
   {
      print (FORMULA "(assert (not (and (not ($rows[$r][$c] = 1)) (not ($rows[$r][$c] = 2)) (not ($rows[$r][$c] = 3)) (not ($rows[$r][$c] = 4)) (not ($rows[$r][$c] = 5)) (not ($rows[$r][$c] = 6)) (not ($rows[$r][$c] = 7)) (not ($rows[$r][$c] = 8)) (not ($rows[$r][$c] = 9)))))\n");
   }
}
print (FORMULA "\n");

print (FORMULA "; Assert that each row and column contains a number only once.\n");
for ($r = 0; $r < 9; $r++)
{
   for ($c = 0; $c < 9; $c++)
   {
      $var = $rows[$r][$c];
      for ($i = 0; $i < 9; $i++)
      {
         if ($var ne $rows[$r][$i])
         {
            print (FORMULA "(assert (not (= $var $rows[$r][$i])))\n");
         }
      }
      for ($i = 0; $i < 9; $i++)
      {
         if ($var ne $rows[$i][$c])
         {
            print (FORMULA "(assert (not (= $var $rows[$i][$c])))\n");
         }
      }
   }
}
print (FORMULA "\n");

print (FORMULA "; Assert that each number appears only once in each block.\n");
for ($r = 0; $r < 9; $r++)
{
   for ($c = 0; $c < 9; $c++)
   {
      $var = $blocks[$r][$c];
      for ($i = 0; $i < 9; $i++)
      {
         if ($var ne $blocks[$r][$i])
         {
            print (FORMULA "(assert (not (= $var $blocks[$r][$i])))\n");
         }
      }
   }
}
print (FORMULA "\n");

print (FORMULA "; Declare input constants\n");
open (INPUT, "<", $ARGV[0]) or die $!;
my @lines;
my $line_num = 0;
while (@lines = split(/ /, <INPUT>))
{
   for ($i = 0; $i <= $#lines; $i++)
   {
      chomp($lines[$i]);
      if ($lines[$i] ne "*")
      {
         print (FORMULA "(assert (= $rows[$line_num][$i] $lines[$i]))\n");
      }
   }
   $line_num++;
}
print (FORMULA "\n");

print (FORMULA "(check-sat)\n");
print (FORMULA "(get-model)\n");

close (FORMULA);

exit;

导致段错误的脚本部分是:

The portion of the script that is causing the seg fault is:

print (FORMULA "; Assert for each variable r_ic_j that 1 <= r_ic_j <= 9\n");
for ($r = 0; $r < 9; $r++)
{
   for ($c = 0; $c < 9; $c++)
   {
      print (FORMULA "(assert (not (and (not ($rows[$r][$c] = 1)) (not ($rows[$r][$c] = 2)) (not ($rows[$r][$c] = 3)) (not ($rows[$r][$c] = 4)) (not ($rows[$r][$c] = 5)) (not ($rows[$r][$c] = 6)) (not ($rows[$r][$c] = 7)) (not ($rows[$r][$c] = 8)) (not ($rows[$r][$c] = 9)))))\n");
   }
}

但是这个片段只是打印了这样的东西:

But this fragment just prints something like this:

(assert (not (and (not (x = 1)) (not (x = 2)) (not (x = 3)) ... (not (x = 9)))))

逻辑上等价于:

(assert (or (= x 1) (= x 2) (= x 3) ... (= x 9)))

感谢任何建议.

问候.

推荐答案

表达式 (x = 1) 在 SMT 2.0 中无效.它应该是 (= x 1).正如您在上面的评论中所描述的，进行此更改后，脚本会按预期工作.

The expression (x = 1) is not valid in SMT 2.0. It should be (= x 1). As you described in the comment above, after this change is made, the script works as expected.

这篇关于Z3分段错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！