如何在 Z3 中使用 .net API 使用 elim-quantifiers？

【问题标题】：how to use elim-quantifiers using .net API in Z3?如何在 Z3 中使用 .net API 使用 elim-quantifiers？
【发布时间】：2012-08-31 09:08:59
【问题描述】：

我找不到(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2)))) 的 .net api，这是一种策略吗？有人可以帮我使用 Z3 的 .net API 来实现以下脚本吗？

(declare-const t1 Int)
(declare-const t2 Int)

(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))

【问题讨论】：

标签： c# .net z3 smt

【解决方案1】：

是的，您可以使用策略。这是一个使用 .NET API 的示例（我没有运行这个特定的示例，因此可能需要进行一些小的修改，但我在我的程序中使用大致相同）。

// (exists ((x Int)) (and (< t1 x) (< x t2))))
Context z3 = new Context();
Expr t1 = z3.MkIntConst("t1");
Expr t2 = z3.MkIntConst("t2");
Expr x = z3.MkIntConst("x");

Expr p = z3.MkAnd(z3.MkLt((ArithExpr)t1, (ArithExpr)x), z3.MkLt((ArithExpr)x, (ArithExpr)t2));
Expr ex = z3.MkExists(new Expr[] { x }, p);

Goal g = z3.MkGoal(true, true, false);
g.Assert((BoolExpr)ex);
Tactic tac = Instance.Z3.MkTactic("qe"); // quantifier elimination
ApplyResult a = tac.Apply(g); // look at a.Subgoals

【讨论】：