<p>基于@nikolaj注释,我使用下面的函数通过重命名标识符来转换SMT2文件,这些标识符在使用z3api时与Z3预先加载的定义冲突。[除了<code>List</code>,函数重命名SMT-LIB公式中常用的标识符。]</p>
<pre><code>import z3
import importlib
def get_formula(src_file_name):
try:
f = z3.parse_smt2_file(src_file_name)
return f
except z3.Z3Exception as e:
lines = open(src_file_name, 'rt').readlines()
tmp1 = ' '.join(lines).replace("max", "c_max")
tmp1 = tmp1.replace("sin", "c_sin")
tmp1 = tmp1.replace("cos", "c_cos")
tmp1 = tmp1.replace("tan", "c_tan")
tmp1 = tmp1.replace("tanh", "c_tanh")
tmp1 = tmp1.replace("atan", "c_atan")
tmp1 = tmp1.replace("min", "c_min")
tmp1 = tmp1.replace("max", "c_max")
tmp1 = tmp1.replace("pi", "c_pi")
tmp1 = tmp1.replace("List", "c_List")
tmp1 = tmp1.replace("subset", "c_subset")
tmp1 = tmp1.replace("difference", "c_difference")
tmp1 = tmp1.replace("union", "c_union")
tmp1 = tmp1.replace("fp", "c_fp")
tmp1 = tmp1.replace("repeat", "c_repeat")
importlib.reload(z3)
f = z3.parse_smt2_string(tmp1)
return f
</code></pre>
<p>有了这个函数,我能够成功地解析公式,但程序seg在退出时出错</strong>。似乎有一些引用即使在重新加载z3模块之后也没有被清除。在</p>