clean up in z3api

1 files changed, 111 insertions, 80 deletions

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index c2eeb45f..aa47d7e0 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -11,13 +11,14 @@ using System.Collections.Generic;
 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

+using Microsoft.Z3;

 

 namespace Microsoft.Boogie.Z3

 {

-    public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>

+    public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>

     {

         private Z3apiOpLineariser OpLinObject = null;

-        private IVCExprOpVisitor<Z3TermAst, LineariserOptions> OpLineariser

+        private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser

         {

             get

             {

@@ -29,36 +30,36 @@ namespace Microsoft.Boogie.Z3
         }

 

         internal readonly UniqueNamer namer;

-        internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;

+        internal readonly Dictionary<VCExprVar, Term> letBindings;

         protected Z3Context cm;

 

         public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)

         {

             this.cm = cm;

             this.namer = namer;

-            this.letBindings = new Dictionary<VCExprVar, Z3TermAst>();

+            this.letBindings = new Dictionary<VCExprVar, Term>();

         }

 

-        public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)

+        public Term Linearise(VCExpr expr, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(expr != null);

-            return expr.Accept<Z3TermAst, LineariserOptions>(this, options);

+            return expr.Accept<Term, LineariserOptions>(this, options);

         }

 

         /////////////////////////////////////////////////////////////////////////////////////

 

-        public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)

+        public Term Visit(VCExprLiteral node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

 

             if (node == VCExpressionGenerator.True)

-                return cm.MakeTrue();

+                return cm.z3.MkTrue();

             else if (node == VCExpressionGenerator.False)

-                return cm.MakeFalse();

+                return cm.z3.MkFalse();

             else if (node is VCExprIntLit)

-                return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString());

+              return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());

             else

             {

                 Contract.Assert(false);

@@ -66,7 +67,7 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)

+        public Term Visit(VCExprNAry node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -76,7 +77,7 @@ namespace Microsoft.Boogie.Z3
             if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))

             {

                 // handle these operators without recursion

-                List<Z3TermAst> asts = new List<Z3TermAst>();

+                List<Term> asts = new List<Term>();

                 string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";

 

                 IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

@@ -93,10 +94,10 @@ namespace Microsoft.Boogie.Z3
                 return cm.Make(opString, asts);

             }

 

-            return node.Accept<Z3TermAst, LineariserOptions>(OpLineariser, options);

+            return node.Accept<Term, LineariserOptions>(OpLineariser, options);

         }

 

-        public Z3TermAst Visit(VCExprVar node, LineariserOptions options)

+        public Term Visit(VCExprVar node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -111,7 +112,7 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)

+        public Term Visit(VCExprQuantifier node, LineariserOptions options)

         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

@@ -123,11 +124,11 @@ namespace Microsoft.Boogie.Z3
                 List<string> varNames;

                 List<Type> varTypes;

                 VisitBounds(node.BoundVars, out varNames, out varTypes);

-                List<Z3PatternAst> patterns;

-                List<Z3TermAst> no_patterns;

+                List<Pattern> patterns;

+                List<Term> no_patterns;

                 VisitTriggers(node.Triggers, options, out patterns, out no_patterns);

-                Z3TermAst body = Linearise(node.Body, options);

-                Z3TermAst result;

+                Term body = Linearise(node.Body, options);

+                Term result;

                 uint weight = 1;

                 string qid = "";

                 int skolemid = 0;

@@ -153,9 +154,9 @@ namespace Microsoft.Boogie.Z3
 

                 switch (node.Quan)

                 {

-                    case Quantifier.ALL:

+                    case Microsoft.Boogie.VCExprAST.Quantifier.ALL:

                         result = cm.MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

-                    case Quantifier.EX:

+                    case Microsoft.Boogie.VCExprAST.Quantifier.EX:

                         result = cm.MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

                     default:

                         throw new Exception("unknown quantifier kind " + node.Quan);

@@ -180,44 +181,44 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

-        private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Z3PatternAst> patterns, out List<Z3TermAst> no_patterns)

+        private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)

         {

-            patterns = new List<Z3PatternAst>();

-            no_patterns = new List<Z3TermAst>();

+            patterns = new List<Pattern>();

+            no_patterns = new List<Term>();

             foreach (VCTrigger trigger in triggers)

             {

-                List<Z3TermAst> exprs = new List<Z3TermAst>();

+                List<Term> exprs = new List<Term>();

                 foreach (VCExpr expr in trigger.Exprs)

                 {

                     System.Diagnostics.Debug.Assert(expr != null);

-                    Z3TermAst termAst = Linearise(expr, options);

+                    Term termAst = Linearise(expr, options);

                     exprs.Add(termAst);

                 }

                 if (exprs.Count > 0)

                 {

                     if (trigger.Pos)

                     {

-                        Z3PatternAst pattern = cm.MakePattern(exprs);

+                        Pattern pattern = cm.MakePattern(exprs);

                         patterns.Add(pattern);

                     }

                     else

                     {

                         System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");

-                        foreach (Z3TermAst expr in exprs)

+                        foreach (Term expr in exprs)

                             no_patterns.Add(expr);

                     }

                 }

             }

         }

 

-        public Z3TermAst Visit(VCExprLet node, LineariserOptions options)

+        public Term Visit(VCExprLet node, LineariserOptions options)

         {

             foreach (VCExprLetBinding b in node)

             {

-                Z3TermAst defAst = Linearise(b.E, options);

+                Term defAst = Linearise(b.E, options);

                 letBindings.Add(b.V, defAst);

             }

-            Z3TermAst letAst = Linearise(node.Body, options);

+            Term letAst = Linearise(node.Body, options);

             foreach (VCExprLetBinding b in node)

             {

                 letBindings.Remove(b.V);

@@ -227,7 +228,7 @@ namespace Microsoft.Boogie.Z3
 

         /////////////////////////////////////////////////////////////////////////////////////

 

-        internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions>

+        internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>

         {

             [ContractInvariantMethod]

             void ObjectInvariant()

@@ -245,13 +246,13 @@ namespace Microsoft.Boogie.Z3
 

             ///////////////////////////////////////////////////////////////////////////////////

 

-            private Z3TermAst WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)

+            private Term WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(op != null);

                 Contract.Requires(cce.NonNullElements(terms));

 

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 foreach (VCExpr e in terms)

                 {

                     Contract.Assert(e != null);

@@ -262,51 +263,51 @@ namespace Microsoft.Boogie.Z3
 

             ///////////////////////////////////////////////////////////////////////////////////

 

-            public Z3TermAst VisitNotOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitNotOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("NOT", node, options);

             }

 

-            public Z3TermAst VisitEqOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitEqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("EQ", node, options);

             }

 

-            public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("NEQ", node, options);

             }

 

-            public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitAndOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("AND", node, options);  

             }

 

-            public Z3TermAst VisitOrOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitOrOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("OR", node, options); 

             }

 

-            public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 if (options.InverseImplies)

                 {

-                    List<Z3TermAst> args = new List<Z3TermAst>();

+                    List<Term> args = new List<Term>();

 

                     args.Add(ExprLineariser.Linearise(node[1], options));

-                    List<Z3TermAst> t = new List<Z3TermAst>();

+                    List<Term> t = new List<Term>();

                     t.Add(ExprLineariser.Linearise(node[0], options));

                     args.Add(ExprLineariser.cm.Make("NOT", t));

                     return ExprLineariser.cm.Make("OR", args);

@@ -317,7 +318,7 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -328,7 +329,7 @@ namespace Microsoft.Boogie.Z3
                 }

                 else

                 {

-                    List<Z3TermAst> args = new List<Z3TermAst>();

+                    List<Term> args = new List<Term>();

                     foreach (VCExpr e in node)

                     {

                         Contract.Assert(e != null);

@@ -338,7 +339,7 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -347,73 +348,103 @@ namespace Microsoft.Boogie.Z3
                 return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); 

             }

 

-            public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

                     args.Add(ExprLineariser.Linearise(e, options));

                 }

-                return ExprLineariser.cm.MakeArraySelect(args);

+

+                Term[] unwrapChildren = args.ToArray();

+                return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]);

                 // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);

             }

 

-            public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);

                     args.Add(ExprLineariser.Linearise(e, options));

                 }

-                return ExprLineariser.cm.MakeArrayStore(args);

+

+                Term[] unwrapChildren = args.ToArray();

+                return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);

                 // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);

             }

 

-            public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitBvOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("$make_bv" + node.Type.BvBits, node, options);

+                List<int> args = new List<int>();

+                foreach (VCExpr e in node) {

+                  VCExprIntLit literal = e as VCExprIntLit;

+                  System.Diagnostics.Debug.Assert(literal != null);

+                  args.Add(literal.Val.ToInt);

+                }

+                System.Diagnostics.Debug.Assert(args.Count == 1);

+                return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits));

             }

 

-            public Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options);

+            public Term VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+

+              VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

+              Contract.Assert(op != null);

+              System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End);

+

+              List<Term> args = new List<Term>();

+              foreach (VCExpr e in node) {

+                Contract.Assert(e != null);

+                args.Add(ExprLineariser.Linearise(e, options));

+              }

+              System.Diagnostics.Debug.Assert(args.Count == 1);

+              return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]);

             }

 

-            public Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options)

-            {

-                Contract.Requires(options != null);

-                Contract.Requires(node != null);

-                return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options);

+            public Term VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {

+              Contract.Requires(options != null);

+              Contract.Requires(node != null);

+

+              VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op;

+              Contract.Assert(op != null);

+

+              List<Term> args = new List<Term>();

+              foreach (VCExpr e in node) {

+                Contract.Assert(e != null);

+                args.Add(ExprLineariser.Linearise(e, options));

+              }

+              System.Diagnostics.Debug.Assert(args.Count == 2);

+              return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]);

             }

 

-            public Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

 

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 args.Add(ExprLineariser.Linearise(node[0], options));

                 args.Add(ExprLineariser.Linearise(node[1], options));

                 args.Add(ExprLineariser.Linearise(node[2], options));

                 return ExprLineariser.cm.Make("ITE", args);

             }

 

-            public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(node != null);

                 Contract.Requires(options != null);

                 VCExprCustomOp op = (VCExprCustomOp)node.Op;

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 foreach (VCExpr arg in node)

                 {

                     args.Add(ExprLineariser.Linearise(arg, options));

@@ -421,7 +452,7 @@ namespace Microsoft.Boogie.Z3
                 return ExprLineariser.cm.Make(op.Name, args);

             }

 

-            public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitAddOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -435,77 +466,77 @@ namespace Microsoft.Boogie.Z3
                 }

             }

 

-            public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("-", node, options);

             }

 

-            public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitMulOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("*", node, options);

             }

 

-            public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitDivOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("/", node, options);

             }

 

-            public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitModOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("%", node, options);

             }

 

-            public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<", node, options);

             }

 

-            public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitLeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<=", node, options);

             }

 

-            public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitGtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication(">", node, options);

             }

 

-            public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitGeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication(">=", node, options);

             }

 

-            public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<:", node, options);

             }

 

-            public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

+            public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

                 return WriteApplication("<::", node, options);

             }

 

-            public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

+            public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

@@ -516,7 +547,7 @@ namespace Microsoft.Boogie.Z3
                 string bvzName = op.Func.FindStringAttribute("external");

                 if (bvzName != null) funcName = bvzName;

 

-                List<Z3TermAst> args = new List<Z3TermAst>();

+                List<Term> args = new List<Term>();

                 foreach (VCExpr e in node)

                 {

                     Contract.Assert(e != null);