int2bv上的z3.parse_smt2_string失败

Question

当我对文档中的示例字符串使用parse_smt2_string时，它可以正常工作。但是，在int2bv上解析失败。我如何诊断这个问题？

>>> import z3
>>> z3.parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
[x > 0, x < 10]
>>> z3.parse_smt2_string('((_ int2bv 1) 1)')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3.py", line 8601, in parse_smt2_string
    return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3core.py", line 3222, in Z3_parse_smtlib2_string
    _elems.Check(a0)
  File "/home/elliot/miniconda3/envs/angr/lib/python3.6/site-packages/z3_solver-4.8.7.0-py3.6-linux-x86_64.egg/z3/z3core.py", line 1381, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 2: invalid command, symbol expected")\n'

Answer 1

这与int2bv无关，而是因为您没有提供在顶级有效的SMTLib行。举个例子，下面的代码是有效的：

>>> z3.parse_smt2_string('(assert (= #b1 ((_ int2bv 1) 1)))')
[1 == int2bv(1)]

在顶层，您可以使用声明、断言或通用SMTLib命令，而不是独立的表达式。