z3py：如何在z3py中設置使用的邏輯？

使用下面的代碼：z3py：如何在z3py中設置使用的邏輯？

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.Solver()沒有給出一個新的z3.Context作爲參數的代碼工作

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中設置邏輯？
我應該使用哪種邏輯與數據類型？

來源

2017-04-27 John Smith

解決方案：SolverFor()

要設置與Z3Py邏輯，而不是使用Solver()函數構造函數創建解算器，你可以使用SolverFor(logic)函數，其中logic是你想用邏輯。

例如，如果鍵入：

s = SolverFor("LIA")

那麼變量s將包含基於線性整數運算在求解器，或如果鍵入

s = SolverFor("LRA")

則變量s將包含基於線性實數算術的求解器。

如果你指定一個不存在/不支持的邏輯，例如輸入SolverFor("abc")，那麼請注意，到目前爲止（但我還沒有使用z3一段時間，然後更新後的版本可能已經修復了這個問題）被生成並且邏輯會像往常一樣自動被猜測。

由於上述問題，測試您想要的邏輯是否真正被使用的唯一方法是將性能與自動選擇的邏輯進行比較，或嘗試解決某些邏輯不支持的問題您指定（例如，當您指定只接受整數varaibales的LIA時使用實變量）以查看是否生成錯誤。如果是的話，那麼求解器實際上就是試圖使用那個邏輯。

來源

2017-05-12 08:57:55

z3py：如何在z3py中設置使用的邏輯？

回答

相關問題