Added /z3lets switch, which governs which kinds of LET expressions are sent to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.

6 files changed, 76 insertions, 46 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 952bad92..d3eb2eba 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -197,6 +197,8 @@ namespace Microsoft.Boogie
     public int Z3mam = 0;

     [Peer] public List<string!>! Z3Options = new List<string!>();

     public bool Z3types = false;

+    public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any

+    invariant 0 <= Z3lets && Z3lets < 4;

 

     // Maximum amount of virtual memory (in bytes) for the prover to use

     //

@@ -219,8 +221,8 @@ namespace Microsoft.Boogie
     public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };

     public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;

 

-	public bool Monomorphize = false;

-	

+    public bool Monomorphize = false;

+    

     public bool ReflectAdd = false;

 

     // Static constructor

@@ -421,8 +423,8 @@ namespace Microsoft.Boogie
             

             case "-launch":

             case "/launch":

-			  System.Diagnostics.Debugger.Launch();

-			  break;

+              System.Diagnostics.Debugger.Launch();

+              break;

             

           case "-proc":

           case "/proc":

@@ -550,8 +552,8 @@ namespace Microsoft.Boogie
           

           case "-proverShutdownLimit":

           case "/proverShutdownLimit":

-			ps.GetNumericArgument(ref ProverShutdownLimit);

-			break;

+            ps.GetNumericArgument(ref ProverShutdownLimit);

+            break;

           

           case "-smtOutput":

           case "/smtOutput":

@@ -931,11 +933,6 @@ namespace Microsoft.Boogie
             }

             break;

             

-          case "-monomorphize":

-          case "/monomorphize":

-			Monomorphize = true;

-			break;

-		  

           case "-vcBrackets":

           case "/vcBrackets":

             ps.GetNumericArgument(ref BracketIdsInVC, 2);

@@ -1021,11 +1018,6 @@ namespace Microsoft.Boogie
             ps.GetNumericArgument(ref ProverCCLimit);

             break;

             

-          case "-z3multipleErrors":

-          case "/z3multipleErrors":

-            z3AtFlag = false;

-            break;

-            

           case "-z3mam":

           case "/z3mam":

           {

@@ -1047,11 +1039,11 @@ namespace Microsoft.Boogie
             }

             break;

 

-          case "-z3types":

-          case "/z3types":

-            Z3types = true;

+          case "-z3lets":

+          case "/z3lets":

+            ps.GetNumericArgument(ref Z3lets, 4);

             break;

-            

+

           case "-platform":

           case "/platform":

             if (ps.ConfirmArgumentCount(1))

@@ -1137,7 +1129,10 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) ||

               ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) ||

               ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||

-              ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd)

+              ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||

+              ps.CheckBooleanFlag("z3types", ref Z3types) ||

+              ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

+              ps.CheckBooleanFlag("monomorphize", ref Monomorphize)

               )

             {

               // one of the boolean flags matched

@@ -1958,6 +1953,8 @@ namespace Microsoft.Boogie
                           macros as in /proverLog can be used.

   

   /z3types       : generate multi-sorted VC that make use of Z3 types

+  /z3lets:<n>    : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

+                   3 - (default) any

 ");

     }

   }

diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc
index 8443d950..0dc52516 100644
--- a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc
+++ b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc
@@ -22,8 +22,16 @@ namespace Microsoft.Boogie.Simplify
   public class Let2ImpliesMutator : SubstitutingVCExprVisitor {

 

     public Let2ImpliesMutator(VCExpressionGenerator! gen) {

+      this(gen, false, false);

+    }

+    public Let2ImpliesMutator(VCExpressionGenerator! gen, bool keepLetTerm, bool keepLetFormula) {

       base(gen);

+      this.keepLetTerm = keepLetTerm;

+      this.keepLetFormula = keepLetFormula;

     }

+    

+    readonly bool keepLetTerm;

+    readonly bool keepLetFormula;

 

     public VCExpr! Mutate(VCExpr! expr) {

       return Mutate(expr, new VCExprSubstitution ());

@@ -138,7 +146,8 @@ namespace Microsoft.Boogie.Simplify
       substitution.PushScope(); try {

 

       // the bindings that remain and that are later handled using an implication

-      List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!> ();

+      List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!> ();

+      List<VCExprLetBinding!> keepBindings = new List<VCExprLetBinding!> ();

 

       foreach (VCExprLetBinding! binding in node) {

         // in all cases we apply the substitution up to this point

@@ -149,18 +158,30 @@ namespace Microsoft.Boogie.Simplify
           // a bound formula is handled using an implication; we introduce

           // a fresh variable to avoid clashes

           assert polarity > 0;

-

-          VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);

-          substitution[binding.V] = newVar;

-

-          bindings.Add(Gen.LetBinding(newVar, newE));

+          

+          if (keepLetFormula) {

+            keepBindings.Add(Gen.LetBinding(binding.V, newE));

+            

+          } else {

+            VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);

+            substitution[binding.V] = newVar;

+

+            bindings.Add(Gen.LetBinding(newVar, newE));

+          }

         } else {

-          // a bound term is substituted

-          substitution[binding.V] = newE;

+          if (keepLetTerm) {

+            keepBindings.Add(Gen.LetBinding(binding.V, newE));

+          } else {

+            // a bound term is substituted

+            substitution[binding.V] = newE;

+          }

         }

       }

 

       VCExpr! newBody = Mutate(node.Body, substitution);

+      if (keepBindings.Count > 0) {

+        newBody = Gen.Let(keepBindings, newBody);

+      }

 

       // Depending on the places where the variable occurs, we would

       // have to introduce implications or equations to define the

@@ -172,7 +193,7 @@ namespace Microsoft.Boogie.Simplify
           assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;

       }

 

-      return Gen.Implies(Gen.AsImplications(bindings), newBody);

+      return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);

 

       } finally {

         substitution.PopScope();

diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
index df7f86d6..09873d7e 100644
--- a/Source/Provers/Simplify/ProverInterface.ssc
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -562,21 +562,24 @@ namespace Microsoft.Boogie.Simplify
     private readonly BigLiteralAbstracter! LitAbstracter;

 

     public override string! translate(VCExpr! expr, int polarity) {

-      Let2ImpliesMutator! letImplier = new Let2ImpliesMutator (Gen);

+      Let2ImpliesMutator! letImplier = new Let2ImpliesMutator(Gen);

 

       // handle the types in the VCExpr

-      TypeEraser! eraser;

+      TypeEraser eraser;

       switch (CommandLineOptions.Clo.TypeEncodingMethod) {

         case CommandLineOptions.TypeEncoding.Arguments:

           eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);

           break;

+        case CommandLineOptions.TypeEncoding.Monomorphic:

+          eraser = null;

+          break;

         default:

           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);

           break;

       }

-      VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);

+      VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;

 

-      TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);

+      TermFormulaFlattener! flattener = new TermFormulaFlattener(Gen);

       VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);

       VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);

 

diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc
index 02b4f505..c3a61fe3 100644
--- a/Source/Provers/Z3/ProverInterface.ssc
+++ b/Source/Provers/Z3/ProverInterface.ssc
@@ -75,6 +75,13 @@ namespace Microsoft.Boogie.Z3
         return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native; 

       } 

     }

+    public int Lets {

+      get

+        ensures 0 <= result && result < 4;

+      {

+        return CommandLineOptions.Clo.Z3lets;

+      }

+    }

     public bool V1 = false;

     public bool V2 = false; // default set in PostParse

     public bool DistZ3 = false;

@@ -107,8 +114,8 @@ namespace Microsoft.Boogie.Z3
         ExeName = "z3-v1.3.exe";

       }

       if (DistZ3) {

-		ExeName = "z3-dist.exe";

-		CommandLineOptions.Clo.RestartProverPerVC = true;

+        ExeName = "z3-dist.exe";

+        CommandLineOptions.Clo.RestartProverPerVC = true;

       }

       

     }

@@ -227,7 +234,6 @@ namespace Microsoft.Boogie.Z3
           eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);

           break;

       }

-      

       VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;

       

       LetBindingSorter! letSorter = new LetBindingSorter(Gen);

@@ -243,6 +249,12 @@ namespace Microsoft.Boogie.Z3
         sortedExpr = flattener.Flatten(sortedExpr);

         sortedAxioms = flattener.Flatten(sortedAxioms);

       }

+      if (Opts.Lets != 3) {

+        // replace let expressions with implies

+        Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);

+        sortedExpr = letImplier.Mutate(sortedExpr);

+        sortedAxioms = letImplier.Mutate(sortedAxioms);

+      }

 

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

       //SubtermCollector! coll = new SubtermCollector (gen);

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 7b6bb5c8..289dff87 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -93,18 +93,15 @@ namespace Microsoft.Boogie.VCExprAST
   public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {

 

     public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {

-      StringWriter sw = new StringWriter();

-      SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);

-      lin.Linearise(e, LineariserOptions.SimplifyDefault);

-      return (!)sw.ToString();

+      return ToString(e, LineariserOptions.SimplifyDefault, namer);

     }

 

     public static string! ToString(VCExpr! e, LineariserOptions! options,

                                    UniqueNamer! namer) {

       StringWriter sw = new StringWriter();

-      SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);

+      SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);

       lin.Linearise(e, options);

-      return (!)sw.ToString();

+      return sw.ToString();

     }

 

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

diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index 8347d124..f282b342 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -708,9 +708,9 @@ namespace Microsoft.Boogie.TypeErasure
                               // "AbstractionVariable(int)" delivers variables

                               TypeSeq! instantiations) {

 

-	  if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))

-		return rawType;

-		

+      if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))

+        return rawType;

+

       if (forall{TypeVariable! var in rawType.FreeVariables;

           !boundTypeParams.Has(var)}) {

         // Bingo!