在 Z3 中对多个值的逻辑公式进行评估

Question

我需要使用 Z3 针对各种变量值评估表达式的值。 我知道 Z3 是一个可满足性检查器，但 model.Eval(Args) 会导致对模型生成的变量值的表达式进行评估。

那么我们是否可以迭代各种值来评估表达式。

示例：p 和 q 在所有可能的 p 和 q 值（p,q 为布尔值）

所以在某种意义上，使用某种递归或迭代来创建一个真值表。 Z3有没有办法做到这一点？

对 C# API 的帮助会更好。

谢谢

Answer 1

您可以考虑 C# API 中的方法Substitute。它可用于用值替换 p 和 q 等常量。它还在应用替换后简化/评估公式。

这是一个使用 Substitute 的小型 C# 示例（来自我们的回归套件）：

using Microsoft.Z3;
using System;
using System.Collections.Generic;

class Test
{
    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() { 
            { "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 的所有功能。

最后，另一种可能性是枚举模型。 通过这样做，您基本上生成了满足公式的所有 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);
        }
    }
}