diff options
Diffstat (limited to 'Source/Provers/Z3api')
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 14 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 159 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 8 |
3 files changed, 161 insertions, 20 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 2eb01e24..df40df3d 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -499,7 +499,7 @@ namespace Microsoft.Boogie.Z3 { sw.WriteLine("*** END_MODEL");
var sr = new StringReader(sw.ToString());
var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
boogieErrors.Add(e);
if (boogieErrors.Count < this.counterexamples) {
@@ -570,7 +570,7 @@ namespace Microsoft.Boogie.Z3 { sw.WriteLine("*** END_MODEL");
var sr = new StringReader(sw.ToString());
var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
boogieErrors.Add(e);
labels.Dispose();
@@ -685,16 +685,16 @@ namespace Microsoft.Boogie.Z3 { }
public class Z3ErrorModelAndLabels {
- private ErrorModel _errorModel;
+ private Model _model;
private List<string> _relevantLabels;
- public ErrorModel ErrorModel {
- get { return this._errorModel; }
+ public Model Model {
+ get { return this._model; }
}
public List<string> RelevantLabels {
get { return this._relevantLabels; }
}
- public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {
- this._errorModel = errorModel;
+ public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {
+ this._model = model;
this._relevantLabels = relevantLabels;
}
}
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 947d4eae..d72705f3 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,7 +19,146 @@ using PatternAst = System.IntPtr; namespace Microsoft.Boogie.Z3
{
- public class Z3apiProcessTheoremProver : ApiProverInterface
+ 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 : ProverInterface
{
public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)
{
@@ -91,10 +230,10 @@ namespace Microsoft.Boogie.Z3 outcome = context.Check(out z3LabelModels);
}
- public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+ public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- outcome = context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
+ return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
@@ -146,12 +285,22 @@ namespace Microsoft.Boogie.Z3 foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
{
List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
- handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
+ handler.OnModel(unprefixedLabels, z3LabelModel.Model);
}
}
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.Model);
+ }
+ }
+ return outcome;
+ }
+
private List<string> RemovePrefixes(List<string> labels)
{
List<string> result = new List<string>();
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 0923cb36..f9511dbd 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -161,14 +161,6 @@ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
- <ProjectReference Include="..\Simplify\Simplify.csproj">
- <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
- <Name>Simplify</Name>
- </ProjectReference>
- <ProjectReference Include="..\Z3\Z3.csproj">
- <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
- <Name>Z3</Name>
- </ProjectReference>
</ItemGroup>
<ItemGroup>
<Compile Include="..\..\version.cs">
|