Z3セグメンテーションフォールト

Question

私は次のPerlスクリプトを書いて、指定された入力ファイルのためのsudokuパズルを解決するためのsmt2形式の論理制約を生成しました。

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スクリプトは次のとおりです：入力ファイルがこの形式である

#! /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; 

ワンセグ障害を引き起こしているスクリプトの一部は次のとおりです。

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"); 
    } 
} 

しかし、このフラグメントは次のようなものを出力します：

(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))) 

何かアドバイスは大歓迎です。

よろしくお願いいたします。

Answer 1

式(x = 1)は、SMT 2.0では無効です。 (= x 1)である必要があります。上記のコメントで説明したように、この変更が行われると、スクリプトは期待通りに機能します。