small changes to z3api to make it compile after the z3 project was ripped out

added CheckOutcomeCore to the class that extends ProverInterface; should be checked

1 files changed, 150 insertions, 1 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 947d4eae..bff7773c 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -8,7 +8,7 @@ using Microsoft.Boogie.AbstractInterpretation;
 using Microsoft.Boogie;

 using Microsoft.Boogie.Z3;

 using Microsoft.Boogie.VCExprAST;

-using Microsoft.Boogie.Simplify;

+using System.Diagnostics.Contracts;

 

 using TypeAst = System.IntPtr;

 using TermAst = System.IntPtr;

@@ -19,6 +19,145 @@ using PatternAst = System.IntPtr;
 

 namespace Microsoft.Boogie.Z3

 {

+  public class Z3InstanceOptions : ProverOptions {

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

+    public int Lets {

+      get {

+        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);

+        return CommandLineOptions.Clo.Z3lets;

+      }

+    }

+    public bool DistZ3 = false;

+    public string ExeName = "z3.exe";

+    public bool InverseImplies = false;

+    public string Inspector = null;

+    public bool OptimizeForBv = false;

+

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(ExeName != null);

+    }

+

+    protected override bool Parse(string opt) {

+      //Contract.Requires(opt!=null);

+      return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

+             ParseString(opt, "INSPECTOR", ref Inspector) ||

+             ParseBool(opt, "DIST", ref DistZ3) ||

+             ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

+             base.Parse(opt);

+    }

+

+    public override void PostParse() {

+      base.PostParse();

+

+      if (DistZ3) {

+        ExeName = "z3-dist.exe";

+        CommandLineOptions.Clo.RestartProverPerVC = true;

+      }

+    }

+

+    public override string Help {

+      get {

+        return

+@"

+Z3-specific options:

+~~~~~~~~~~~~~~~~~~~~

+INSPECTOR=<string>        Use the specified Z3Inspector binary.

+OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

+

+Obscure options:

+~~~~~~~~~~~~~~~~

+DIST=<bool>               Use z3-dist.exe binary.

+REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.

+

+" + base.Help;

+        // DIST requires non-public binaries

+      }

+    }

+  }

+

+  public class Z3LineariserOptions : LineariserOptions {

+    private readonly Z3InstanceOptions opts;

+

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(opts != null);

+    }

+

+

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

+      : base(asTerm) {

+      Contract.Requires(opts != null);

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

+

+      this.opts = opts;

+      this.LetVariablesAttr = letVariables;

+    }

+

+    public override bool UseWeights {

+      get {

+        return true;

+      }

+    }

+

+    public override bool UseTypes {

+      get {

+        return true;

+      }

+    }

+

+    public override bool QuantifierIds {

+      get {

+        return true;

+      }

+    }

+

+    public override bool InverseImplies {

+      get {

+        return opts.InverseImplies;

+      }

+    }

+

+    public override LineariserOptions SetAsTerm(bool newVal) {

+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);

+

+      if (newVal == AsTerm)

+        return this;

+      return new Z3LineariserOptions(newVal, opts, LetVariables);

+    }

+

+    // variables representing formulas in let-bindings have to be

+    // printed in a different way than other variables

+    private readonly List<VCExprVar/*!>!*/> LetVariablesAttr;

+    public override List<VCExprVar/*!>!*/> LetVariables {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

+

+        return LetVariablesAttr;

+      }

+    }

+

+    public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {

+      //Contract.Requires(furtherVar != null);

+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);

+

+      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();

+      allVars.AddRange(LetVariables);

+      allVars.Add(furtherVar);

+      return new Z3LineariserOptions(AsTerm, opts, allVars);

+    }

+

+    public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {

+      //Contract.Requires(furtherVars != null);

+      Contract.Ensures(Contract.Result<LineariserOptions>() != null);

+

+      List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();

+      allVars.AddRange(LetVariables);

+      allVars.AddRange(furtherVars);

+      return new Z3LineariserOptions(AsTerm, opts, allVars);

+    }

+  }

+

     public class Z3apiProcessTheoremProver : ApiProverInterface

     {

         public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)

@@ -152,6 +291,16 @@ namespace Microsoft.Boogie.Z3
             return outcome;

         }

 

+        public override Outcome CheckOutcomeCore(ErrorHandler handler) {

+          if (outcome == Outcome.Invalid) {

+            foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {

+              List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

+              handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

+            }

+          }

+          return outcome;

+        }

+

         private List<string> RemovePrefixes(List<string> labels)

         {

             List<string> result = new List<string>();