如何在Z3中通过.net接口使用elim-quantifiers？
如何在Z3中通过.net接口使用elim-quantifiers？
提问于 2012-09-06 22:04:28
我找不到(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))的.net接口，这是策略吗？有没有人可以帮我用Z3的.net接口来实现以下脚本？
(declare-const t1 Int)
(declare-const t2 Int)
(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))回答 1
Stack Overflow用户
回答已采纳
发布于 2012-09-06 23:07:13
是的，你可以使用一种策略。下面是一个使用.NET应用程序接口的示例(我没有运行这个特定的示例，所以它可能需要进行一些小的修改，但我在我的程序中使用了大致相同的内容)。
// (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页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/12301908
复制相关文章
相似问题
腾讯云开发者
