summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/Inspector.cs1
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs216
-rw-r--r--Source/Provers/SMTLib/SMTLib.csproj4
-rw-r--r--Source/Provers/TPTP/TPTP.csproj4
-rw-r--r--Source/Provers/Z3api/ProverLayer.cs153
-rw-r--r--Source/Provers/Z3api/Z3api.csproj8
6 files changed, 254 insertions, 132 deletions
diff --git a/Source/Provers/SMTLib/Inspector.cs b/Source/Provers/SMTLib/Inspector.cs
index 4126c169..362502f3 100644
--- a/Source/Provers/SMTLib/Inspector.cs
+++ b/Source/Provers/SMTLib/Inspector.cs
@@ -11,7 +11,6 @@ using System.Collections.Generic;
using System.Diagnostics.Contracts;
//using util;
using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 657603d0..6ef3778d 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -17,12 +17,11 @@ using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.Clustering;
using Microsoft.Boogie.TypeErasure;
-using Microsoft.Boogie.Simplify;
using System.Text;
namespace Microsoft.Boogie.SMTLib
{
- public class SMTLibProcessTheoremProver : ApiProverInterface
+ public class SMTLibProcessTheoremProver : ProverInterface
{
private readonly SMTLibProverContext ctx;
private readonly VCExpressionGenerator gen;
@@ -94,7 +93,6 @@ namespace Microsoft.Boogie.SMTLib
PrepareCommon();
}
prevOutcomeAvailable = false;
- pendingPop = false;
}
void SetupProcess()
@@ -285,15 +283,6 @@ namespace Microsoft.Boogie.SMTLib
Process.Close();
}
- string controlFlowVariable;
-
- private VCExpr ArgumentZero(VCExpr vc) {
- VCExprNAry naryExpr = vc as VCExprNAry;
- if (naryExpr == null)
- return null;
- return naryExpr[0];
- }
-
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
//Contract.Requires(descriptiveName != null);
@@ -307,9 +296,6 @@ namespace Microsoft.Boogie.SMTLib
currentLogFile.Write(common.ToString());
}
- if (!CommandLineOptions.Clo.UseLabels)
- controlFlowVariable = VCExpr2String(ArgumentZero(ArgumentZero(ArgumentZero(vc))),1);
-
PrepareCommon();
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -395,7 +381,19 @@ namespace Microsoft.Boogie.SMTLib
[NoDefaultContract]
public override Outcome CheckOutcome(ErrorHandler handler)
- { //Contract.Requires(handler != null);
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
+ var result = CheckOutcomeCore(handler);
+ SendThisVC("(pop 1)");
+ FlushLogFile();
+
+ return result;
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcomeCore(ErrorHandler handler)
+ {
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
var result = Outcome.Undetermined;
@@ -413,40 +411,47 @@ namespace Microsoft.Boogie.SMTLib
var globalResult = Outcome.Undetermined;
- while (errorsLeft-- > 0) {
+ while (true) {
+ errorsLeft--;
string[] labels = null;
result = GetResponse();
if (globalResult == Outcome.Undetermined)
globalResult = result;
- if (result == Outcome.Invalid && options.UseZ3) {
- labels = GetLabelsInfo(handler);
+ if (result == Outcome.Invalid) {
+ IList<string> xlabels;
+ if (CommandLineOptions.Clo.UseLabels) {
+ labels = GetLabelsInfo();
+ xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
+ }
+ else {
+ labels = CalculatePath(0);
+ xlabels = labels;
+ }
+ ErrorModel errorModel = GetErrorModel();
+ handler.OnModel(xlabels, errorModel);
}
- if (labels == null) break;
+ if (labels == null || errorsLeft == 0) break;
- var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();
- var posLabels = labels.Where(l => !l.StartsWith("@"));
- Func<string, string> lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s));
- if (!options.MultiTraces)
- posLabels = Enumerable.Empty<string>();
- var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();
- var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");
- if (errorsLeft > 0) {
+ if (CommandLineOptions.Clo.UseLabels) {
+ var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();
+ var posLabels = labels.Where(l => !l.StartsWith("@"));
+ Func<string, string> lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s));
+ if (!options.MultiTraces)
+ posLabels = Enumerable.Empty<string>();
+ var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();
+ var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");
SendThisVC("(assert " + expr + ")");
SendThisVC("(check-sat)");
}
- }
-
- if (CommandLineOptions.Clo.StratifiedInlining == 0)
- {
- SendThisVC("(pop 1)");
- }
- else if (CommandLineOptions.Clo.StratifiedInlining > 0 && pendingPop)
- {
- pendingPop = false;
- SendThisVC("(pop 1)");
+ else {
+ string source = labels[labels.Length - 2];
+ string target = labels[labels.Length - 1];
+ SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))");
+ SendThisVC("(check-sat)");
+ }
}
FlushLogFile();
@@ -461,100 +466,91 @@ namespace Microsoft.Boogie.SMTLib
}
}
- private string[] CalculatePath() {
- SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " 0)))");
+ public override string[] CalculatePath(int controlFlowConstant) {
+ SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))");
var path = new List<string>();
while (true) {
var resp = Process.GetProverResponse();
- if (resp == null)
- break;
+ if (resp == null) break;
if (!(resp.Name == "" && resp.ArgCount == 1)) break;
resp = resp.Arguments[0];
if (!(resp.Name == "" && resp.ArgCount == 2)) break;
resp = resp.Arguments[1];
var v = resp.Name;
- if (v == "-" && resp.ArgCount == 1)
- v += resp.Arguments[0].Name;
- else if (resp.ArgCount != 0)
+ if (v == "-" && resp.ArgCount == 1) {
+ v = resp.Arguments[0].Name;
+ path.Add(v);
+ break;
+ }
+ else if (resp.ArgCount != 0)
break;
- if (v.StartsWith("-")) {
- path.Add("@" + v.Substring(1));
+ path.Add(v);
+ SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");
+ }
+ return path.ToArray();
+ }
+
+ private ErrorModel GetErrorModel() {
+ if (!options.ExpectingModel())
+ return null;
+ SendThisVC("(get-model)");
+ Process.Ping();
+ Model theModel = null;
+ while (true) {
+ var resp = Process.GetProverResponse();
+ if (resp == null || Process.IsPong(resp))
break;
+ if (theModel != null)
+ HandleProverError("Expecting only one model but got many");
+
+ string modelStr = null;
+ if (resp.Name == "model" && resp.ArgCount >= 1) {
+ modelStr = resp[0].Name;
+ }
+ else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
+ modelStr = resp.Name;
}
else {
- path.Add("+" + v);
+ HandleProverError("Unexpected prover response getting model: " + resp.ToString());
+ }
+ List<Model> models = null;
+ try {
+ models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
}
- SendThisVC("(get-value ((ControlFlow " + controlFlowVariable + " " + v + ")))");
+ catch (ArgumentException exn) {
+ HandleProverError("Model parsing error: " + exn.Message);
+ }
+ if (models == null)
+ HandleProverError("Could not parse any models");
+ else if (models.Count == 0)
+ HandleProverError("Could not parse any models");
+ else if (models.Count > 1)
+ HandleProverError("Expecting only one model but got many");
+ else
+ theModel = models[0];
}
- return path.ToArray();
+ return new ErrorModel(theModel);
}
- private string[] GetLabelsInfo(ErrorHandler handler)
+ private string[] GetLabelsInfo()
{
- if (CommandLineOptions.Clo.UseLabels)
- SendThisVC("(labels)");
- if (options.ExpectingModel())
- SendThisVC("(get-model)");
+ SendThisVC("(labels)");
Process.Ping();
- List<string> labelNums = null;
- Model theModel = null;
string[] res = null;
-
while (true) {
var resp = Process.GetProverResponse();
if (resp == null || Process.IsPong(resp))
break;
+ if (res != null)
+ HandleProverError("Expecting only one sequence of labels but got many");
if (resp.Name == "labels" && resp.ArgCount >= 1) {
- var labels = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray();
- res = labels;
- if (labelNums != null) HandleProverError("Got multiple :labels responses");
- labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
- } else {
- string modelStr = null;
- if (resp.Name == "model" && resp.ArgCount >= 1) {
- modelStr = resp[0].Name;
- } else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
- modelStr = resp.Name;
- }
-
- if (modelStr != null) {
- List<Model> models = null;
- try {
- models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
- } catch (ArgumentException exn) {
- HandleProverError("Model parsing error: " + exn.Message);
- }
-
- if (models != null) {
- if (models.Count == 0) HandleProverError("Could not parse any models");
- else {
- if (models.Count > 1) HandleProverError("Expecting only one model, got multiple");
- if (theModel != null) HandleProverError("Got multiple :model responses");
- theModel = models[0];
- }
- }
- } else {
- HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString());
- }
+ res = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray();
+ }
+ else {
+ HandleProverError("Unexpected prover response getting labels: " + resp.ToString());
}
}
-
- if (!CommandLineOptions.Clo.UseLabels) {
- res = CalculatePath();
- if (res.Length == 0)
- res = null;
- else
- labelNums = res.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
- }
-
- if (labelNums != null) {
- ErrorModel m = null;
- if (theModel != null)
- m = new ErrorModel(theModel);
- handler.OnModel(labelNums, m);
- }
-
return res;
}
@@ -767,7 +763,6 @@ namespace Microsoft.Boogie.SMTLib
throw new NotImplementedException();
}
- // For implementing ApiProverInterface
public override void Assert(VCExpr vc, bool polarity)
{
string a = "";
@@ -790,7 +785,7 @@ namespace Microsoft.Boogie.SMTLib
public override void Check()
{
- Contract.Assert(pendingPop == false && prevOutcomeAvailable == false);
+ Contract.Assert(prevOutcomeAvailable == false);
PrepareCommon();
SendThisVC("(check-sat)");
@@ -806,15 +801,13 @@ namespace Microsoft.Boogie.SMTLib
/// Extra state for ApiChecker (used by stratifiedInlining)
/// </summary>
bool prevOutcomeAvailable;
- bool pendingPop;
Outcome prevOutcome;
static int nameCounter = 0;
public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
- Contract.Assert(pendingPop == false && prevOutcomeAvailable == false);
+ Contract.Assert(prevOutcomeAvailable == false);
- Push();
unsatCore = new List<int>();
// Name the assumptions
@@ -835,7 +828,6 @@ namespace Microsoft.Boogie.SMTLib
prevOutcomeAvailable = true;
if (prevOutcome != Outcome.Valid)
{
- pendingPop = true;
return;
}
Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores");
@@ -845,8 +837,6 @@ namespace Microsoft.Boogie.SMTLib
if(resp.Name != "") unsatCore.Add(nameToAssumption[resp.Name]);
foreach (var s in resp.Arguments) unsatCore.Add(nameToAssumption[s.Name]);
- Pop();
-
FlushLogFile();
}
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index f4cdbb14..3dc042a6 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -191,10 +191,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>
</ItemGroup>
<ItemGroup>
<Folder Include="Properties\" />
diff --git a/Source/Provers/TPTP/TPTP.csproj b/Source/Provers/TPTP/TPTP.csproj
index 564b33f3..882d8009 100644
--- a/Source/Provers/TPTP/TPTP.csproj
+++ b/Source/Provers/TPTP/TPTP.csproj
@@ -116,10 +116,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>
</ItemGroup>
<ItemGroup>
<Folder Include="Properties\" />
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 947d4eae..3b7b8f43 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)
{
@@ -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>();
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 94184957..7c481438 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -162,14 +162,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">