summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/CVC4.cs71
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs98
-rw-r--r--Source/Provers/SMTLib/SMTLib.csproj7
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs17
-rw-r--r--Source/Provers/SMTLib/Z3.cs7
5 files changed, 151 insertions, 49 deletions
diff --git a/Source/Provers/SMTLib/CVC4.cs b/Source/Provers/SMTLib/CVC4.cs
new file mode 100644
index 00000000..0ac2ec20
--- /dev/null
+++ b/Source/Provers/SMTLib/CVC4.cs
@@ -0,0 +1,71 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie.SMTLib
+{
+ class CVC4
+ {
+ static string _proverPath;
+
+ static string CodebaseString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
+ }
+
+ public static string ExecutablePath()
+ {
+ if (_proverPath == null)
+ FindExecutable();
+ return _proverPath;
+ }
+
+ static void FindExecutable()
+ // throws ProverException, System.IO.FileNotFoundException;
+ {
+ Contract.Ensures(_proverPath != null);
+
+ // Command line option 'cvc4exe' always has priority if set
+ if (CommandLineOptions.Clo.CVC4ExecutablePath != null)
+ {
+ _proverPath = CommandLineOptions.Clo.CVC4ExecutablePath;
+ if (!File.Exists(_proverPath))
+ {
+ throw new ProverException("Cannot find prover specified with cvc4exe: " + _proverPath);
+ }
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
+ var proverExe = "cvc4.exe";
+
+ if (_proverPath == null)
+ {
+ // Initialize '_proverPath'
+ _proverPath = Path.Combine(CodebaseString(), proverExe);
+ string firstTry = _proverPath;
+
+ if (File.Exists(firstTry))
+ {
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+ else
+ {
+ throw new ProverException("Cannot find executable: " + firstTry);
+ }
+ }
+ }
+ }
+}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ee955def..36e45fbc 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -109,14 +109,10 @@ namespace Microsoft.Boogie.SMTLib
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");
+ return SMTLibProcess.ComputerProcessStartInfo(path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
default:
Debug.Assert(false);
return null;
@@ -400,34 +396,38 @@ namespace Microsoft.Boogie.SMTLib
FlushLogFile();
}
- public override void Reset()
+ public override void Reset ()
{
- SendThisVC("(reset)");
-
- if (0 < common.Length)
- {
- var c = common.ToString();
- Process.Send(c);
- if (currentLogFile != null)
- {
- currentLogFile.WriteLine(c);
+ if (options.Solver == SolverKind.Z3) {
+ SendThisVC ("(reset)");
+
+ if (0 < common.Length)
+ {
+ var c = common.ToString ();
+ Process.Send (c);
+ if (currentLogFile != null)
+ {
+ currentLogFile.WriteLine (c);
+ }
}
}
}
-
- public override void FullReset()
+
+ public override void FullReset ()
{
- Namer.Reset();
- common.Clear();
- SetupAxiomBuilder(gen);
- Axioms.Clear();
- TypeDecls.Clear();
- AxiomsAreSetup = false;
- ctx.Reset();
- ctx.KnownDatatypeConstructors.Clear();
- ctx.parent = this;
- DeclCollector.Reset();
- SendThisVC("; doing a full reset...");
+ if (options.Solver == SolverKind.Z3) {
+ Namer.Reset ();
+ common.Clear ();
+ SetupAxiomBuilder (gen);
+ Axioms.Clear ();
+ TypeDecls.Clear ();
+ AxiomsAreSetup = false;
+ ctx.Reset ();
+ ctx.KnownDatatypeConstructors.Clear ();
+ ctx.parent = this;
+ DeclCollector.Reset ();
+ SendThisVC ("; doing a full reset...");
+ }
}
private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
@@ -556,7 +556,7 @@ namespace Microsoft.Boogie.SMTLib
// Concatenate all the arguments
string modelString = resp[0].Name;
// modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
- var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString));
+ var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString), "");
if (models == null || models.Count == 0)
{
HandleProverError("no model from prover: " + resp.ToString());
@@ -923,9 +923,14 @@ namespace Microsoft.Boogie.SMTLib
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;
+ modelStr = resp.Arguments[0] + "\n";
+ for (int i = 1; i < resp.ArgCount; i++) {
+ if (resp.Arguments[i].ToString().Contains("define-fun") &&!resp.Arguments[i].ToString().Contains("not"))
+ modelStr += resp.Arguments[i] + "\n";
+ }
}
else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
modelStr = resp.Name;
@@ -933,9 +938,24 @@ namespace Microsoft.Boogie.SMTLib
else {
HandleProverError("Unexpected prover response getting model: " + resp.ToString());
}
+
List<Model> models = null;
try {
- models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (CommandLineOptions.Clo.UseSmtOutputFormat) {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");
+ } else {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
+ }
+ break;
+ case SolverKind.CVC4:
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");
+ break;
+ default:
+ Debug.Assert(false);
+ return null;
+ }
}
catch (ArgumentException exn) {
HandleProverError("Model parsing error: " + exn.Message);
@@ -1211,15 +1231,17 @@ namespace Microsoft.Boogie.SMTLib
SendThisVC("(check-sat)");
FlushLogFile();
}
-
+
public override void SetTimeOut(int ms)
{
- var name = Z3.SetTimeoutOption();
- var value = ms.ToString();
- options.TimeLimit = ms;
- options.SmtOptions.RemoveAll(ov => ov.Option == name);
- options.AddSmtOption(name, value);
- SendThisVC(string.Format("(set-option :{0} {1})", name, value));
+ if (options.Solver == SolverKind.Z3) {
+ var name = Z3.SetTimeoutOption();
+ var value = ms.ToString();
+ options.TimeLimit = ms;
+ options.SmtOptions.RemoveAll(ov => ov.Option == name);
+ options.AddSmtOption(name, value);
+ SendThisVC(string.Format("(set-option :{0} {1})", name, value));
+ }
}
public override object Evaluate(VCExpr expr)
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index c58d3349..bc1b7e02 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for SMTLib.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -157,6 +161,7 @@
<Compile Include="TypeDeclCollector.cs" />
<Compile Include="..\..\version.cs" />
<Compile Include="Z3.cs" />
+ <Compile Include="CVC4.cs" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
@@ -172,7 +177,7 @@
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\..\Model\Model.csproj">
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index d336252e..3f4ef5ac 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -27,7 +27,7 @@ namespace Microsoft.Boogie.SMTLib
}
}
- public enum SolverKind { Z3, CVC3, CVC4 };
+ public enum SolverKind { Z3, CVC4 };
public class SMTLibProverOptions : ProverOptions
{
@@ -43,6 +43,7 @@ namespace Microsoft.Boogie.SMTLib
// Z3 specific (at the moment; some of them make sense also for other provers)
public string Inspector = null;
public bool OptimizeForBv = false;
+ public bool SMTLib2Model = false;
public bool ProduceModel() {
return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||
@@ -89,16 +90,12 @@ namespace Microsoft.Boogie.SMTLib
case "z3":
Solver = SolverKind.Z3;
break;
- case "cvc3":
- Solver = SolverKind.CVC3;
- Logic = "ALL";
- break;
case "cvc4":
Solver = SolverKind.CVC4;
- Logic = "ALL_SUPPORTED";
+ if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
break;
default:
- ReportError("Invalid SOLVER value; must be 'z3', 'cvc3' or 'cvc4'");
+ ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");
return false;
}
return true;
@@ -119,6 +116,7 @@ namespace Microsoft.Boogie.SMTLib
ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+ ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) ||
ParseString(opt, "LOGIC", ref Logic) ||
base.Parse(opt);
}
@@ -138,18 +136,19 @@ namespace Microsoft.Boogie.SMTLib
@"
SMT-specific options:
~~~~~~~~~~~~~~~~~~~~~
-SOLVER=<string> Use the given SMT solver (z3, cvc3, cvc4; default: z3)
+SOLVER=<string> Use the given SMT solver (z3 or 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, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4)
+LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty, '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.
+SMTLIB2_MODEL=<bool> Use the SMTLIB2 output model. Defaults to false.
" + base.Help;
}
}
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 24071457..d2e06168 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -283,9 +283,14 @@ namespace Microsoft.Boogie.SMTLib
//options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
- options.AddWeakSmtOption("MODEL_V2", "true");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+ if (CommandLineOptions.Clo.UseSmtOutputFormat) {
+ options.AddWeakSmtOption("pp-bv-literals", "false");;
+ } else {
+ options.AddWeakSmtOption("MODEL_V2", "true");
+ }
+
if (!options.OptimizeForBv)
{
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 20:59:17 +0000