diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 11 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/CVC4.cs | 71 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLib.csproj | 7 |
3 files changed, 88 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 683935b4..cea7d4c4 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -409,6 +409,7 @@ namespace Microsoft.Boogie { public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
public string Z3ExecutablePath = null;
+ public string CVC4ExecutablePath = null;
public enum ProverWarnings {
None,
@@ -1259,6 +1260,12 @@ namespace Microsoft.Boogie { }
return true;
+ case "cvc4exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ CVC4ExecutablePath = args[ps.i];
+ }
+ return true;
+
case "doBitVectorAnalysis":
DoBitVectorAnalysis = true;
if (ps.ConfirmArgumentCount(1)) {
@@ -1806,6 +1813,10 @@ namespace Microsoft.Boogie { 3 - (default) any
/z3exe:<path>
path to Z3 executable
+
+ CVC4 specific options:
+ /cvc4exe:<path>
+ path to CVC4 executable
");
}
}
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/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">
|