Z3:将 Z3py 表达式从 Solver 对象转换为 SMT-LIB2 [英] Z3: convert Z3py expression to SMT-LIB2 from Solver object

问题描述

这个问题非常类似于:Z3: convert Z3py expression to SMT-LIB2?

是否可以从 Solver 对象生成 SMT-LIB2 输出?

Is it possible to generate SMT-LIB2 output from Solver object ?

推荐答案

Solver 类具有名为 assertions() 的方法.它返回所有在给定求解器中断言的公式.提取断言后，我们可以使用上一个问题中使用的相同方法.这是对

The Solver class has method called assertions(). It returns all formulas asserted into the given solver. After we extract the assertions, we can use the same approach used in the previous question. Here is a quick and dirty modification to

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  if isinstance(f, Solver):
    a = f.assertions()
    if len(a) == 0:
      f = BoolVal(True)
    else:
      f = And(*a)
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

这是一个示例(也可在此处在线获取)

s = Solver()
print toSMT2Benchmark(s, logic="QF_LIA")
a, b = Ints('a b')
s.add(a > 1)
s.add(Or(a < 1, b < 2))
print toSMT2Benchmark(s, logic="QF_LIA")

EDIT 我们可以使用以下脚本以 SMTLIB 1.x 格式显示输出(也可在线获得 此处).请注意，SMTLIB 1.x 非常有限，并且不支持一些功能.我们还强烈鼓励所有用户迁移到 SMTLIB 2.x.

EDIT We can use the following script to display the output in SMTLIB 1.x format (also available online here). Note that SMTLIB 1.x is very limited, and several features are not supported. We also strongly encourage all users to move to SMTLIB 2.x.

def toSMTBenchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  if isinstance(f, Solver):
    a = f.assertions()
    if len(a) == 0:
      f = BoolVal(True)
    else:
      f = And(*a)
  Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB_COMPLIANT)  # Set SMTLIB 1.x pretty print mode  
  r = Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())
  Z3_set_ast_print_mode(f.ctx_ref(), Z3_PRINT_SMTLIB2_COMPLIANT) # Restore SMTLIB 2.x pretty print mode
  return r

s = Solver()
print toSMTBenchmark(s, logic="QF_LIA")
a, b = Ints('a b')
s.add(a > 1)
s.add(Or(a < 1, b < 2))
print toSMTBenchmark(s, logic="QF_LIA")

结束编辑

这篇关于Z3:将 Z3py 表达式从 Solver 对象转换为 SMT-LIB2的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！