Boogie: internal clean-up, removed BvHandling type, everything now behaves as if the old /bv:z were used

2 files changed, 9 insertions, 31 deletions

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 8929e732..6a066f1f 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -156,11 +156,8 @@ namespace Microsoft.Boogie.Z3
       if (opts.Inspector != null)

         AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");

 

-      if (opts.Typed) {

-        AddOption(result, "TYPE_CHECK", "true");

-        if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)

-            AddOption(result, "BV_REFLECT", "true");

-      }

+      AddOption(result, "TYPE_CHECK", "true");

+      AddOption(result, "BV_REFLECT", "true");

 

       foreach (string opt in CommandLineOptions.Clo.Z3Options) {

         Contract.Assert(opt != null);

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 19097f8c..3194fa63 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -35,7 +35,7 @@ void ObjectInvariant()
 

     [NotDelayed]

     public Z3ProcessTheoremProver(VCExpressionGenerator gen,

-                                  DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName,opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx")

+                                  DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName, "TypedUnivBackPred2.sx")

     {

       Contract.Requires(gen != null);

       Contract.Requires(ctx != null);

@@ -88,11 +88,6 @@ void ObjectInvariant()
   public class Z3InstanceOptions : ProverOptions

   {

     public int Timeout { get { return TimeLimit / 1000; } }

-    public bool Typed {

-      get { 

-        return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;

-      } 

-    }

     public int Lets {

       get

         {

@@ -164,10 +159,6 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }

 

 

-    public override CommandLineOptions.BvHandling Bitvectors { get {

-      return opts.BitVectors;

-    } }

- 

     public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {

     Contract.Requires(opts != null);

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

@@ -181,7 +172,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     } }

 

     public override bool UseTypes { get {

-      return opts.Typed;

+      return true;

     } }

 

     public override bool QuantifierIds { get {

@@ -254,7 +245,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       UniqueNamer namer = new UniqueNamer ();

       Namer = namer;

       this.DeclCollector =

-        new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);

+        new TypeDeclCollector (namer, true);

     }

 

     private Z3VCExprTranslator(Z3VCExprTranslator tl) :base(tl){

@@ -332,16 +323,9 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);

       Contract.Assert(sortedAxioms!=null);

 

-      if (Opts.Typed) {

-        DeclCollector.Collect(sortedAxioms);

-        DeclCollector.Collect(sortedExpr);

-        FeedTypeDeclsToProver();

-      } else {

-        TermFormulaFlattener flattener = new TermFormulaFlattener (Gen);

-        Contract.Assert(flattener!=null);

-        sortedExpr = flattener.Flatten(sortedExpr);

-        sortedAxioms = flattener.Flatten(sortedAxioms);

-      }

+      DeclCollector.Collect(sortedAxioms);

+      DeclCollector.Collect(sortedExpr);

+      FeedTypeDeclsToProver();

       if (Opts.Lets != 3) {

         // replace let expressions with implies

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

@@ -412,10 +396,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       proverCommands.Add("all");

       proverCommands.Add("z3");

       proverCommands.Add("simplifyLike");

-      if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)

-        proverCommands.Add("bvDefSem");

-      if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)

-        proverCommands.Add("bvInt");

+      proverCommands.Add("bvDefSem");

       VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

       

       return NewProverContext(gen, genOptions, opts);