1 
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
try:
    f = open("read.txt","r")
    try:
        str = f.read()
        length = len(str)
        s.add(str)
    finally:
        f.close()
except IOError:
    pass

上記のコードを書きましたが、うまくいきません。入力として文字列を使用していないため、受け入れる入力の種類を見つけることができません。

4

1 に答える 1

2

martineauによって提案されたことを基本的に行うことができます。read.txtファイルには任意の Python コマンドが含まれている可能性があるため、これは大きなハックであり安全ではないことに注意してください。とにかく、次のコードは、入力ファイルの各行を評価し、結果のオブジェクトをソルバーに追加しますs。ファイルread.txtに が含まれている場合x + y == 2、出力は次のようになります。

sat
[y = 0, x = 2]

更新されたコードは次のとおりです。

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
try:
    f = open("read.txt","r")
    try:
        for l in f:
            s.add(eval(l))
    finally:
        f.close()
except IOError:
    pass
print s.check()
print s.model()

別の解決策は、SMT-LIB 2.0 形式でファイルを作成し、次の投稿で説明されている方法を使用することです。

于 2013-07-09T01:06:11.050 に答える