1

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

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

示例： p 和 q 在 p 和 q 的所有可能值（p，q 是 Boolean ）

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

C# API 的帮助会更好。

谢谢

4

1 回答 1

1

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

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

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);
        }
    }
}
于 2012-05-19T14:52:20.697 回答