我找不到.NET API为(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
文章来源: how to use elim-quantifiers using .net API in Z3?
