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

我找不到.net api for (elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))它是一个战术吗？ 有人可以帮我使用Z3的.net API来实现以下脚本吗？

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

Answer 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