z3py：z3pyでどのように使用するロジックを設定しますか？次のコードを使用して

Question

：

import z3 

solver = z3.Solver(ctx=z3.Context()) 
#solver = z3.Solver() 

Direction = z3.Datatype('Direction') 
Direction.declare('up') 
Direction.declare('down') 
Direction = Direction.create() 

Cell = z3.Datatype('Cell') 
Cell.declare('cons', ('front', Direction), ('back', z3.IntSort())) 
Cell = Cell.create() 

mycell = z3.Const("mycell", Cell) 

solver.add(Cell.cons(Direction.up, 10) == Cell.cons(Direction.up, 10)) 

私は次のエラーを取得：コードのみが動作しているパラメータとして新しいz3.Contextを与えることなくz3.Solver()を使用する場合

Traceback (most recent call last): 
    File "thedt2opttest.py", line 17, in <module> 
    solver.add(Cell.cons(Direction.up, 10) == Cell.cons(Direction.up, 10)) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 6052, in add 
    self.assert_exprs(*args) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 6040, in assert_exprs 
    arg = s.cast(arg) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 1304, in cast 
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 90, in _z3_assert 
    raise Z3Exception(msg) 
z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value 

を。

• ここでの違いは何ですか：

  は、誰かが次の質問に答えていただけますか？

• z3pyでロジックを設定するにはどうすればよいですか？
• データ型にはどのようなロジックを使用する必要がありますか？

Answer 1

ソリューション：SolverFor()

ではなくSolver()関数コンストラクタを使用してソルバを作成するのではなく、あなたが使用したいロジックがあるlogicSolverFor(logic)機能を使用することができ、Z3Pyとロジックを設定するには。

あなたが入力した場合たとえば、：

s = SolverFor("LIA")

をその変数sリニア整数算数に基づいてソルバーを含んでいるでしょうか、その変数を

s = SolverFor("LRA")

を入力した場合sには、Linear Real Arithmeticsに基づくソルバーが含まれています。

存在しない/サポートされていないロジックを指定した場合、例えばSolverFor("abc")と入力するとエラーが発生することはありませんが（これまではz3を使用していませんでした。ロジックは通常どおり自動的に推測されます。

上記の問題のため、実際に使用しているロジックが実際に使用されているかどうかをテストする唯一の方法は、自動的に選択されたロジックに関するパフォーマンスを比較するか、ロジックでサポートされていないものエラーが生成されたかどうかを確認するために指定した（たとえば、整数変数を受け入れるLIAを指定したときに実変数を使用して）。 yesの場合、ソルバーは実際にそのロジックを使用しようとしています。