Some changes to support expanded use of z3api.

Should not affect function
of other provers. There is an option added in Check.cs to  allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).

1 files changed, 246 insertions, 3 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index f0aa3906..2eb01e24 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -20,6 +20,8 @@ namespace Microsoft.Boogie.Z3 {
     internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();

     internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();

     internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();

+    internal BacktrackDictionary<Term, VCExpr> constants_inv = null;

+    internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;

 

     public Config config;

     public Context z3;

@@ -56,7 +58,13 @@ namespace Microsoft.Boogie.Z3 {
       z3 = new Context(config);

       z3.SetPrintMode(PrintMode.Smtlib2Compliant);

       if (logFilename != null)

-        z3.OpenLog(logFilename);

+      {

+#if true

+          Z3Log.Open(logFilename);

+#else

+          z3.OpenLog(logFilename);

+#endif

+      }

       foreach (string tag in debugTraces)

         z3.EnableDebugTrace(tag);

 

@@ -65,6 +73,227 @@ namespace Microsoft.Boogie.Z3 {
       this.namer = new UniqueNamer();

     }

 

+    public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)

+        : base(gen, new VCGenerationOptions(new List<string>()))

+    {

+        z3 = ctx;

+

+        this.z3log = null;

+        this.tm = new Z3TypeCachedBuilder(this);

+        this.namer = new UniqueNamer();

+

+        // For external 

+

+        constants_inv = new BacktrackDictionary<Term, VCExpr>();

+        functions_inv = new BacktrackDictionary<FuncDecl, Function>();

+    }

+

+    public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {

+        Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

+        return (Term)expr.Accept(visitor, linOptions);

+    }

+

+

+    private class fromZ3

+    {

+        private VCExpressionGenerator gen;

+        private Dictionary<Term, VCExpr> memo;

+        private BacktrackDictionary<Term, VCExpr> constants_inv;

+        private BacktrackDictionary<FuncDecl, Function> functions_inv;

+        private List<VCExprLetBinding> lets;

+        private int let_ctr = 0;

+

+        private VCExpr create_let(Term t, VCExpr u)

+        {

+            var name = "$x" + let_ctr.ToString();

+            let_ctr++;

+            var sym = gen.Variable(name, u.Type);

+            memo.Remove(t);

+            memo.Add(t, sym);

+            lets.Add(gen.LetBinding(sym, u));

+            return sym;

+        }

+

+        public fromZ3(VCExpressionGenerator _gen,

+                      BacktrackDictionary<Term, VCExpr> _constants_inv,

+                      BacktrackDictionary<FuncDecl, Function> _functions_inv)

+        {

+            gen = _gen;

+            constants_inv = _constants_inv;

+            functions_inv = _functions_inv;

+            memo = new Dictionary<Term, VCExpr>();

+            lets = new List<VCExprLetBinding>();

+        }

+

+        public void clear()

+        {

+            memo.Clear();

+            lets.Clear();

+        }

+        public VCExpr get(Term arg)

+        {

+            if (memo.ContainsKey(arg))

+                return memo[arg];

+            VCExpr res = null;

+            switch (arg.GetKind())

+            {

+                case TermKind.Numeral:

+                    var numstr = arg.GetNumeralString();

+                    var bignum = Basetypes.BigNum.FromString(numstr);

+                    res = gen.Integer(bignum);

+                    break;

+                case TermKind.App:

+                    var args = arg.GetAppArgs();

+                    var vcargs = new VCExpr[args.Length];

+                    for (int i = 0; i < args.Length; i++)

+                        vcargs[i] = get(args[i]);

+

+                    switch (arg.GetAppDecl().GetKind())

+                    {

+                        case DeclKind.Add:

+                            if (vcargs.Length == 0)

+                                res = gen.Integer(Basetypes.BigNum.FromInt(0));

+                            else

+                            {

+                                res = vcargs[0];

+                                for (int k = 1; k < vcargs.Length; k++)

+                                    res = gen.Add(res, vcargs[k]);

+                            }

+                            break;

+                        case DeclKind.And:

+                            res = VCExpressionGenerator.True;

+                            for (int i = 0; i < vcargs.Length; i++)

+                                res = gen.AndSimp(res, vcargs[i]);

+                            break;

+                        case DeclKind.Div:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Eq:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Eq(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.False:

+                            res = VCExpressionGenerator.False;

+                            break;

+                        case DeclKind.Ge:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Gt:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Gt(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.IDiv:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Iff:

+                            Debug.Assert(vcargs.Length == 2);

+                            var l = create_let(args[0], vcargs[0]);

+                            var r = create_let(args[1], vcargs[1]);

+                            return gen.And(gen.Implies(l, r), gen.Implies(r, l));

+                        case DeclKind.Implies:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Implies(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Ite:

+                            Debug.Assert(vcargs.Length == 3);

+                            res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);

+                            break;

+                        case DeclKind.Le:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Lt:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Mod:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Mul:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Not:

+                            Debug.Assert(vcargs.Length == 1);

+                            res = gen.Not(vcargs[0]);

+                            break;

+                        case DeclKind.Or:

+                            res = VCExpressionGenerator.False;

+                            for (int i = 0; i < vcargs.Length; i++)

+                                res = gen.OrSimp(res, vcargs[i]);

+                            break;

+                        case DeclKind.Select:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Select(vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.Store:

+                            Debug.Assert(vcargs.Length == 3);

+                            res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);

+                            break;

+                        case DeclKind.Sub:

+                            Debug.Assert(vcargs.Length == 2);

+                            res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);

+                            break;

+                        case DeclKind.True:

+                            res = VCExpressionGenerator.True;

+                            break;

+                        case DeclKind.Uminus:

+                            Debug.Assert(vcargs.Length == 1);

+                            var bigzero = Basetypes.BigNum.FromInt(0);

+                            res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]);

+                            break;

+                        case DeclKind.Uninterpreted:

+                            var name = arg.GetAppDecl().GetDeclName();

+                            if (args.Length == 0)

+                            { // a 0-ary constant is a VCExprVar

+                                if (!constants_inv.TryGetValue(arg, out res))

+                                    throw new Exception("Z3 returned unknown constant: " + name);

+                            }

+                            else

+                            {

+                                Function f;

+                                if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))

+                                    throw new Exception("Z3 returned unknown function: " + name);

+                                List<VCExpr> vcargsList = new List<VCExpr>(vcargs);

+                                res = gen.Function(f, vcargsList);

+                            }   

+                            break;

+                        default:

+                            throw new Exception("Unknown Z3 operator");

+                    }

+                    break;

+                default:

+                    Debug.Assert(false);

+                    throw new Exception("Unknown Z3 AST kind");

+            }

+

+            memo.Add(arg, res);

+            return res;

+        }

+        public VCExpr add_lets(VCExpr e)

+        {

+            foreach (var let in lets)

+            {

+                e = gen.Let(e, let);

+            }

+            return e;

+        }

+    }

+

+    public VCExpr TermToVCExpr(Term t)

+    {

+      var fZ = new fromZ3(gen, constants_inv, functions_inv);

+      return fZ.add_lets(fZ.get(t));

+    }

+

+

+    

+

+

     public override void DeclareType(TypeCtorDecl t, string attributes) {

       base.DeclareType(t, attributes);

       log("(declare-sort {0})", t.Name);

@@ -97,6 +326,7 @@ namespace Microsoft.Boogie.Z3 {
       Sort rangeAst = tm.GetType(range);

       FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);

       functions.Add(functionName, constDeclAst);

+      if(functions_inv != null)functions_inv.Add(constDeclAst, f);

       log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);

     }

 

@@ -122,7 +352,11 @@ namespace Microsoft.Boogie.Z3 {
     }

 

     public void CloseLog() {

-      z3.CloseLog();

+#if true

+        Z3Log.Close();

+#else

+        z3.CloseLog();

+#endif

       if (z3log != null) {

         z3log.Close();

       }

@@ -134,6 +368,8 @@ namespace Microsoft.Boogie.Z3 {
       constants.CreateBacktrackPoint();

       functions.CreateBacktrackPoint();

       labels.CreateBacktrackPoint();

+      if(constants_inv != null)constants_inv.CreateBacktrackPoint();

+      if(functions_inv != null)functions_inv.CreateBacktrackPoint();

       z3.Push();

       log("(push)");

     }

@@ -144,6 +380,8 @@ namespace Microsoft.Boogie.Z3 {
       functions.Backtrack();

       constants.Backtrack();

       symbols.Backtrack();

+      if (constants_inv != null) constants_inv.Backtrack();

+      if (functions_inv != null) functions_inv.Backtrack();

       log("(pop)");

     }

 

@@ -368,13 +606,18 @@ namespace Microsoft.Boogie.Z3 {
       return result;

     }

 

-    public Term GetConstant(string constantName, Type constantType) {

+    public Term GetConstant(string constantName, Type constantType, VCExpr node)

+    {

       Term typeSafeTerm;

       if (!constants.ContainsKey(constantName))

         this.DeclareConstant(constantName, constantType);

 

       if (!constants.TryGetValue(constantName, out typeSafeTerm))

         throw new Exception("constant " + constantName + " is not defined");

+

+      if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))

+          constants_inv.Add(typeSafeTerm, node);

+

       return typeSafeTerm;

     }