在Z3中评估许多值的逻辑公式
我需要使用Z3来评估表达式在各种变量值上的值。 我知道Z3是一个令人满意的检查器，但是model.Eval（Args）会导致对模型生成的变量值的表达式进行求值。
因此，我们可以迭代各种值来评估表达式。
示例：p和q在p和q的所有可能值（p，q为布尔值）
所以在某种意义上使用一些递归或迭代来创建一个真值表。 Z3有可能以任何方式这样做吗？
对C＃API的帮助会更好。
谢谢
您可以考虑在C＃API中Substitute方法。 它可用于通过值替换p和q等常量。 它还在应用替换后简化/评估公式。
这是一个小的C＃示例（来自我们的回归套件）使用Substitute ：
using Microsoft.Z3; using System; using System.Collections.Generic; class Test { public void Run() { Dictionary cfg = new Dictionary() { { "AUTO_CONFIG", "true" } }; using (Context ctx = new Context(cfg)) { IntExpr x = ctx.MkIntConst("x"); IntExpr y = ctx.MkIntConst("y"); FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { ctx.IntSort, ctx.IntSort }, ctx.IntSort); FuncDecl g = ctx.MkFuncDecl("g", new Sort[] { ctx.IntSort }, ctx.IntSort); Expr n = f[f[g[x], g[g[x]]], g[g[y]]]; Console.WriteLine(n); Expr nn = n.Substitute(new Expr[] { g[g[x]], g[y] }, new Expr[] { y, ctx.MkAdd(x, ctx.MkInt(1)) } ); Console.WriteLine(nn); Console.WriteLine(n.Substitute(g[g[x]], y)); } } }
当然，您必须编写一个循环来迭代所有可能的值。 在Python中，您可以使用列表推导： http ： //rise4fun.com/Z3Py/56另一种选择是使用Simplify方法。 此方法可用于评估不包含未解释符号（如p和q公式。 这是Python中的另一个例子： http ： //rise4fun.com/Z3Py/PC我正在使用Python，因为我们不支持在浏览器中运行C＃示例。 请注意，C＃中的Z3 API包含Python的所有function。
最后，另一种可能性是枚举模型。 通过这样做，你基本上产生满足公式的所有p和q值（即，使其成立）。 我们的想法是添加阻止当前模型的新约束，然后再次解决。 这是Python中的一个小脚本： http ： //rise4fun.com/Z3Py/PDJ
约束block用于阻止当前模型。 如果我们取消注释print block ，我们也可以为Z3生成的每个模型打印它。 当然，如果有无限模型满足公式，这种方法不会终止，如下例所示： http ： //rise4fun.com/Z3Py/X0l
这些示例可以用C＃编码。 这是一个C＃示例，演示如何迭代模型中的常量（和函数），并获得它们的解释：
using Microsoft.Z3; using System; class Test { public void Run() { using (Context ctx = new Context()) { Sort U = ctx.MkUninterpretedSort("U"); FuncDecl f = ctx.MkFuncDecl("f", U, U); Expr a = ctx.MkConst("a", U); Expr b = ctx.MkConst("b", U); Expr c = ctx.MkConst("c", U); Solver s = ctx.MkSolver(); s.Assert(ctx.MkEq(f[f[a]], b), ctx.MkNot(ctx.MkEq(f[b], c)), ctx.MkEq(f[c], c)); Console.WriteLine(s.Check()); Model m = s.Model; foreach (FuncDecl d in m.Decls) if (d.DomainSize == 0) Console.WriteLine(d.Name + " -> " + m.ConstInterp(d)); else Console.WriteLine(d.Name + " -> " + m.FuncInterp(d)); Console.WriteLine(m.NumSorts); Console.WriteLine(m.Sorts[0]); foreach(Sort srt in m.Sorts) Console.WriteLine(srt); foreach (Expr v in m.SortUniverse(U)) Console.WriteLine(v); } } }