Evaluation of a logical formula at many values in

问题:

I needed to evaluate the value of an expression over various values of variables using Z3. I know Z3 is a satisfiabilty checker but model.Eval(Args) causes evaluations of an expression at values of variables generated by model.

So is it possible for us to iterate over various values to evaluate an expression.

Example : p and q at all possible values of p and q (p,q being Boolean )

So in some sense creating a truth table out of it using some recursion or iteration. Is it possible any way for Z3 to do so?

Help with the C# API will be even better.

Thanks

回答1:

You may consider the method Substitute in the C# API. It can be used to substitute constants such as p and q by values. It also simplifies/evaluates the formula after applying the substitution.

Here is a small C# example (from our regression suite) using 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));
        }
    }
}

Of course, you will have to write a loop to iterate over all possible values. In Python, you can use list comprehensions: http://rise4fun.com/Z3Py/56 Another option is to use the method Simplify. This method can be used to evaluate formulas that do not contains uninterpreted symbols such as p and q. Here is another example in Python: http://rise4fun.com/Z3Py/PC I'm using Python because we don't have support for running C# examples in the browser. Note that, the Z3 API in C# contains all the functionality of the Python one.

Finally, another possibility is to enumerate models. By doing it, you are essentially producing all values of p and q that satisfy the formula (i.e., make it true). The idea is to add new constraints that block the current model, and solve again. Here is a small script in Python for doing it: http://rise4fun.com/Z3Py/PDJ

The constraint block is used to block the current model. If we uncomment print block, we can also print it for each model produced by Z3. Of course, this approach does not terminate if there are infinite models that satisfy the formula like in this example: http://rise4fun.com/Z3Py/X0l

These examples can be encoded in C#. Here is a C# example demonstrating how to iterate over the constants (and functions) in a model, and obtaining their interpretation:

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);
        }
    }
}