我正在嘗試決議一個字串并將其轉換為其等效的 z3 形式。
import z3
expr = 'x y = 10'
p = my_parse_expr_to_z3(expr) # results in: ([x, ' ', y], '==', [10])
p = my_flatten(p) # after flatten: [x, ' ', y, '==', 10]
決議字串的型別檢查：
for e in p:
print(type(e), e)
# -->
<class 'z3.z3.ArithRef'> x
<class 'str'>
<class 'z3.z3.ArithRef'> y
<class 'str'> ==
<class 'int'> 10
當我現在嘗試：
s = z3.Solver()
s.add(*p)
我得到：
Traceback (most recent call last):
File "<input>", line 1, in <module>
File "...\venv\lib\site-packages\z3\z3.py", line 6938, in add
self.assert_exprs(*args)
File "..\venv\lib\site-packages\z3\z3.py", line 6926, in assert_exprs
arg = s.cast(arg)
File "..\venv\lib\site-packages\z3\z3.py", line 1505, in cast
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
File "..\venv\lib\site-packages\z3\z3.py", line 112, in _z3_assert
raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value
等號和加號出現錯誤型別/用法？我該如何正確翻譯？
uj5u.com熱心網友回復：
parse_expr_to_z3從哪里來的定義？它絕對不是z3本身自帶的東西，所以你一定是從其他第三方那里得到的，或者你自己寫的。在不知道它是如何定義的情況下，堆疊溢位的任何人都不可能為您提供任何指導。
無論如何，正如您所懷疑的那樣，您無法將其結果反饋給 z3。它之所以失敗，正是因為您可以添加到求解器中的內容必須是約束條件，即Boolz3 中的型別運算式。顯然，這些成分都沒有這種型別。
所以，長話短說，這parse_expr_to_z3似乎不是為了做你想要的。聯系其開發人員以獲取有關預期用例的更多詳細資訊。
如果您嘗試將字串中的斷言加載到 z3，那么您可以使用所謂的 SMTLib 格式來實作。就像是：
from z3 import *
expr = """
(declare-const x Int)
(declare-const y Int)
(assert (= ( x y) 10))
"""
p = parse_smt2_string(expr)
s = Solver()
s.add(p)
print(s.check())
print(s.model())
這列印：
sat
[y = 0, x = 10]
您可以在https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf 中找到有關 SMTLib 語法的更多資訊
需要注意的是試圖做到這一點使用任何其他語法（如您的建議'x y = 10'）將需要在字串中的變數知識（x和y在這種情況下，但當然可以是任意的），和什么樣的符號（ 和=你的情況，但同樣可以是任意數量的不同符號）及其精確含義。在不知道您的確切需求的情況下，很難斷定，但使用除對 SMTLib 語法本身的現有支持之外的任何其他東西都需要大量的作業。
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/390900.html