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.

1 files changed, 30 insertions, 9 deletions

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