diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Source/Provers/SMTLib/CVC4.cs | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Source/Provers/SMTLib/CVC4.cs')
-rw-r--r-- | Source/Provers/SMTLib/CVC4.cs | 142 |
1 files changed, 71 insertions, 71 deletions
diff --git a/Source/Provers/SMTLib/CVC4.cs b/Source/Provers/SMTLib/CVC4.cs index 0ac2ec20..999ac7b5 100644 --- a/Source/Provers/SMTLib/CVC4.cs +++ b/Source/Provers/SMTLib/CVC4.cs @@ -1,71 +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);
- }
- }
- }
- }
-}
+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); + } + } + } + } +} |