Tag: z3

关于Z3 for Java的性能问题

我在使用Z3 for Java的当前项目中遇到了一些性能问题：基本上我当前的大多数约束非常简单：例如： (f(x) = 2 && f(y) <= 3) || f(x) <=5 (f(x) = 2 && f(y) <= 3) || f(x) <=5 我正在使用整个项目共享的静态上下文和解算器实例： public class ConstraintManager { static Context ctx; static Solver solver; … } 如果我通过相同的ctx实例生成expr数十亿次，那是否会出现问题？ 何时是调用ctx.Dispose()的最佳时机，或者，管理c​​tx的最佳方法是什么？ 我调用了expr.Simplify()来简化一些约束，例如： f(x)=3 && f(x)<=2 。 但是这个API结果非常慢。 特别是约束的长度增加了。 这是一个已知问题还是因为我错误地使用了它？ 我正在使用expr.substitute(expr1, expr2) ，但我注意到z3会在替换后将expr转换为let-bindingforms。 这是为了使配方更紧凑吗？

显示从SMT-LIB2文件解析的声明

我正在使用Z3和Java API。 在我的SMT-LIB2文件中，有几个变量： (declare-fun x0 () Int) (declare-fun x1 () Bool) ; alot more 我想得到所有这些变量，并将它们存储在Expr数组中。 从z3 SMTLIBDecls的示例中，我找到了API SMTLIBDecls ，它们从SMT-LIB1文件中解析出声明，但SMT-LIB2没有类似的API。 我怎样才能得到声明？ 谢谢。

Z3 Java API文档或教程

我已经安装了Z3 API for Java的Z3 API for Java ，我正在尝试使用它，但我找不到任何解释如何使用此API的教程或文档。 到目前为止我找到的唯一资源是源代码和示例程序 ，所以我想知道是否有人知道Z3 Java API的任何其他文档/教程。