From f0df4f110687974508a4c96e4ebb58a9cd7270c8 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sun, 4 Oct 2009 07:01:06 +0000
Subject: 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.

---
 Source/Provers/Z3/ProverInterface.ssc | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'Source/Provers/Z3')

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);
-- 
cgit v1.2.3