summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
committerGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
commit85a65323bda16d372a9e163dc4225e5d5535d14c (patch)
tree6e4999e040de5a5c7511521939c576957509b538 /Source
parentf369261b5b9953380d8fb8e0f7b020167482a491 (diff)
Implement support for alternative SMT solvers -- CVC3 and CVC4
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/CommandLineOptions.cs6
-rw-r--r--Source/Core/VCExp.cs4
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs41
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs18
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs5
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs35
6 files changed, 84 insertions, 25 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4e134b3c..f45b76ba 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1266,6 +1266,12 @@ namespace Microsoft.Boogie {
ProverName = "SMTLib".ToUpper();
}
+ var proverOpts = TheProverFactory.BlankProverOptions();
+ proverOpts.Parse(ProverOptions);
+ if (!TheProverFactory.SupportsLabels(proverOpts)) {
+ UseLabels = false;
+ }
+
if (vcVariety == VCVariety.Unspecified) {
vcVariety = TheProverFactory.DefaultVCVariety;
}
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 6bc43e14..1e82224c 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -202,6 +202,10 @@ The generic options may or may not be used by the prover plugin.
}
}
+ public virtual bool SupportsLabels(ProverOptions options) {
+ return true;
+ }
+
public virtual void Close() {
}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 8c6ad875..89bd9d6e 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -94,17 +94,33 @@ namespace Microsoft.Boogie.SMTLib
}
}
- void SetupProcess()
+ ProcessStartInfo ComputeProcessStartInfo()
{
- if (!this.options.UseZ3)
- return;
+ var path = this.options.ProverPath;
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (path == null)
+ path = Z3.ExecutablePath();
+ return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
+ case SolverKind.CVC3:
+ if (path == null)
+ path = "cvc3";
+ return SMTLibProcess.ComputerProcessStartInfo(path, "-lang smt2 +interactive -showPrompt");
+ case SolverKind.CVC4:
+ if (path == null)
+ path = "cvc4";
+ return SMTLibProcess.ComputerProcessStartInfo(path, "--smtlib2 --no-strict-parsing");
+ default:
+ Debug.Assert(false);
+ return null;
+ }
+ }
+ void SetupProcess()
+ {
if (Process != null) return;
- var path = this.options.ProverPath;
- if (path == null)
- path = Z3.ExecutablePath();
- var psi = SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
+ var psi = ComputeProcessStartInfo();
Process = new SMTLibProcess(psi, this.options);
Process.ErrorHandler += this.HandleProverError;
}
@@ -197,6 +213,10 @@ namespace Microsoft.Boogie.SMTLib
SendCommon("; done setting options\n");
SendCommon(_backgroundPredicates);
+ if (options.UseTickleBool) {
+ SendCommon("(declare-fun tickleBool (Bool) Bool)");
+ SendCommon("(assert (and (tickleBool true) (tickleBool false)))");
+ }
if (ctx.KnownDatatypeConstructors.Count > 0) {
string datatypeString = "";
@@ -986,7 +1006,7 @@ namespace Microsoft.Boogie.SMTLib
List<string>/*!>!*/ proverCommands = new List<string/*!*/>();
proverCommands.Add("smtlib");
var opts = (SMTLibProverOptions)options ;
- if (opts.UseZ3)
+ if (opts.Solver == SolverKind.Z3)
proverCommands.Add("z3");
else
proverCommands.Add("external");
@@ -1010,5 +1030,10 @@ namespace Microsoft.Boogie.SMTLib
return new SMTLibProcessTheoremProver(options, gen, ctx);
}
+
+ public override bool SupportsLabels(ProverOptions options)
+ {
+ return ((SMTLibProverOptions)options).SupportsLabels;
+ }
}
}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 0a0e37a2..6a2cbb6a 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -416,14 +416,7 @@ namespace Microsoft.Boogie.SMTLib
Contract.Requires(node != null);
Contract.Requires(options != null);
- // not sure if this is needed
- if (node[0].Type.IsBool) {
- Contract.Assert(node[1].Type.IsBool);
- // use equivalence
- WriteApplication("iff", node, options);
- } else {
- WriteApplication("=", node, options);
- }
+ WriteApplication("=", node, options);
return true;
}
@@ -470,7 +463,10 @@ namespace Microsoft.Boogie.SMTLib
public bool VisitCustomOp(VCExprNAry node, LineariserOptions options)
{
VCExprCustomOp op = (VCExprCustomOp)node.Op;
- WriteApplication(op.Name, node, options);
+ if (!ExprLineariser.ProverOptions.UseTickleBool && op.Name == "tickleBool")
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ else
+ WriteApplication(op.Name, node, options);
return true;
}
@@ -517,7 +513,7 @@ namespace Microsoft.Boogie.SMTLib
}
var op = (VCExprLabelOp)node.Op;
- if (ExprLineariser.ProverOptions.UseLabels) {
+ if (CommandLineOptions.Clo.UseLabels) {
// Z3 extension
//wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));
wr.Write("(! ");
@@ -529,7 +525,7 @@ namespace Microsoft.Boogie.SMTLib
wr.Write(")");
- if (ExprLineariser.ProverOptions.UseLabels)
+ if (CommandLineOptions.Clo.UseLabels)
wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));
return true;
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 1dcfdbff..f4fa5e75 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -162,6 +162,11 @@ namespace Microsoft.Boogie.SMTLib
sb.Clear();
}
}
+ } else if (resp.Name == "unsupported") {
+ // Skip -- this may be a benign "unsupported" from a previous command.
+ // Of course, this is suboptimal. We should really be using
+ // print-success to identify the errant command and determine whether
+ // the response is benign.
} else {
return resp;
}
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 8aea84c5..4d002956 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -27,17 +27,20 @@ namespace Microsoft.Boogie.SMTLib
}
}
+ public enum SolverKind { Z3, CVC3, CVC4 };
+
public class SMTLibProverOptions : ProverOptions
{
public bool UseWeights = true;
- public bool UseLabels { get { return UseZ3; } }
+ public bool SupportsLabels { get { return Solver == SolverKind.Z3; } }
+ public bool UseTickleBool { get { return Solver == SolverKind.Z3; } }
+ public SolverKind Solver = SolverKind.Z3;
public List<OptionValue> SmtOptions = new List<OptionValue>();
public List<string> SolverArguments = new List<string>();
public bool MultiTraces = false;
public string Logic = "";
// Z3 specific (at the moment; some of them make sense also for other provers)
- public bool UseZ3 = true;
public string Inspector = null;
public bool OptimizeForBv = false;
@@ -80,6 +83,27 @@ namespace Microsoft.Boogie.SMTLib
protected override bool Parse(string opt)
{
+ string SolverStr = null;
+ if (ParseString(opt, "SOLVER", ref SolverStr)) {
+ switch (SolverStr) {
+ case "z3":
+ Solver = SolverKind.Z3;
+ break;
+ case "cvc3":
+ Solver = SolverKind.CVC3;
+ Logic = "ALL";
+ break;
+ case "cvc4":
+ Solver = SolverKind.CVC4;
+ Logic = "ALL_SUPPORTED";
+ break;
+ default:
+ ReportError("Invalid SOLVER value; must be 'z3', 'cvc3' or 'cvc4'");
+ return false;
+ }
+ return true;
+ }
+
if (opt.StartsWith("O:")) {
AddSmtOption(opt.Substring(2));
return true;
@@ -93,7 +117,6 @@ namespace Microsoft.Boogie.SMTLib
return
ParseBool(opt, "MULTI_TRACES", ref MultiTraces) ||
ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||
- ParseBool(opt, "USE_Z3", ref UseZ3) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
ParseString(opt, "LOGIC", ref Logic) ||
@@ -103,7 +126,7 @@ namespace Microsoft.Boogie.SMTLib
public override void PostParse()
{
base.PostParse();
- if (UseZ3)
+ if (Solver == SolverKind.Z3)
Z3.SetupOptions(this);
}
@@ -115,18 +138,18 @@ namespace Microsoft.Boogie.SMTLib
@"
SMT-specific options:
~~~~~~~~~~~~~~~~~~~~~
+SOLVER=<string> Use the given SMT solver (z3, cvc3, cvc4; default: z3)
USE_WEIGHTS=<bool> Pass :weight annotations on quantified formulas (default: true)
VERBOSITY=<int> 1 - print prover output (default: 0)
O:<name>=<value> Pass (set-option :<name> <value>) to the SMT solver.
C:<string> Pass <string> to the SMT on the command line.
-LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty)
+LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4)
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
MULTI_TRACES=<bool> Report errors with multiple paths leading to the same assertion.
INSPECTOR=<string> Use the specified Z3Inspector binary.
OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
-USE_Z3=<bool> Use z3.exe as the prover, and use Z3 extensions (default: true)
" + base.Help;
}
}