From 85a65323bda16d372a9e163dc4225e5d5535d14c Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Thu, 6 Sep 2012 20:33:21 +0100 Subject: Implement support for alternative SMT solvers -- CVC3 and CVC4 --- Binaries/UnivBackPred2.smt2 | 2 -- Source/Core/CommandLineOptions.cs | 6 ++++ Source/Core/VCExp.cs | 4 +++ Source/Provers/SMTLib/ProverInterface.cs | 41 ++++++++++++++++++++++------ Source/Provers/SMTLib/SMTLibLineariser.cs | 18 +++++------- Source/Provers/SMTLib/SMTLibProcess.cs | 5 ++++ Source/Provers/SMTLib/SMTLibProverOptions.cs | 35 ++++++++++++++++++++---- 7 files changed, 84 insertions(+), 27 deletions(-) diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index 97c052c9..d3e3777f 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -7,5 +7,3 @@ (declare-fun int_mod (Int Int) Int) (declare-fun UOrdering2 (|T@U| |T@U|) Bool) (declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) -(declare-fun tickleBool (Bool) Bool) -(assert (and (tickleBool true) (tickleBool false))) 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/*!>!*/ proverCommands = new List(); 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 SmtOptions = new List(); public List SolverArguments = new List(); 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= Use the given SMT solver (z3, cvc3, cvc4; default: z3) USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) VERBOSITY= 1 - print prover output (default: 0) O:= Pass (set-option : ) to the SMT solver. C: Pass to the SMT on the command line. -LOGIC= Pass (set-logic ) to the prover (default: empty) +LOGIC= Pass (set-logic ) to the prover (default: empty, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4) Z3-specific options: ~~~~~~~~~~~~~~~~~~~~ MULTI_TRACES= Report errors with multiple paths leading to the same assertion. INSPECTOR= Use the specified Z3Inspector binary. OPTIMIZE_FOR_BV= Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. -USE_Z3= Use z3.exe as the prover, and use Z3 extensions (default: true) " + base.Help; } } -- cgit v1.2.3