【发布时间】：2013-11-29 11:12:15
【问题描述】：
根据simplification in Z3，Z3中有两种简化表达式的方法：simplify和ctx-solver-simplify使用Java api时，我只能在com.microsoft.z3.Expr类上找到simplify()的方法.如何使用ctx-solver-simplify 方法？ Solver 类中似乎不存在它。
【问题讨论】：
标签： z3
【发布时间】：2013-11-29 11:12:15
【问题描述】：
你需要使用一种策略，见this overview。
查看这个答案以获取 Java 中的示例，以及使用策略或主要求解器之间的比较：
How to call Z3 properly from Java program?
要使用 Java 中的 ctx-solver-simplify 策略，请使用以下命令创建对象：
Tactic css = ctx.MkTactic("ctx-solver-simplify")
ctx 是一个 Z3 上下文对象。
【讨论】：
-
那么我该如何简化表达式呢？你能创建一个例子吗？我似乎要构建一个目标，但我不知道要给出什么参数。
-
这是 Z3 .NET API 中使用不同策略（量词消除）的一个最小示例，但 Java API 的对象（可能是模次要重命名）和步骤是相同的，结果简化将在 ApplyResult 对象的 Subgoals 字段中，然后您需要从那里迭代子目标以重新创建表达式；有点乏味：stackoverflow.com/questions/12301908/…