summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/CommandLineOptions.cs16
-rw-r--r--Source/Core/VCExp.cs28
-rw-r--r--Source/Provers/Isabelle/Prover.cs2
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs34
-rw-r--r--Source/Provers/TPTP/ProverInterface.cs34
-rw-r--r--Source/Provers/Z3/ProverInterface.cs10
-rw-r--r--Source/VCGeneration/Check.cs1
7 files changed, 99 insertions, 26 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5425f6c0..aca58286 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -113,7 +113,6 @@ namespace Microsoft.Boogie {
public bool PrintDesugarings = false;
public string SimplifyLogFilePath = null;
- public string SMTLibOutputPath = "boogie-vc-@PROC@.smt";
public string/*!*/ LogPrefix = "";
public bool PrintInstrumented = false;
public bool InstrumentWithAsserts = false;
@@ -737,13 +736,6 @@ namespace Microsoft.Boogie {
ps.GetNumericArgument(ref ProverShutdownLimit);
break;
- case "-smtOutput":
- case "/smtOutput":
- if (ps.ConfirmArgumentCount(1)) {
- SMTLibOutputPath = args[ps.i];
- }
- break;
-
case "-errorTrace":
case "/errorTrace":
ps.GetNumericArgument(ref ErrorTrace, 3);
@@ -1445,7 +1437,6 @@ namespace Microsoft.Boogie {
ExpandFilename(ref DafnyPrelude);
ExpandFilename(ref DafnyPrintFile);
ExpandFilename(ref SimplifyLogFilePath);
- ExpandFilename(ref SMTLibOutputPath);
ExpandFilename(ref PrintErrorModelFile);
Contract.Assume(XmlSink == null); // XmlSink is to be set here
@@ -2238,7 +2229,7 @@ namespace Microsoft.Boogie {
/proverLog:<file> : Log input for the theorem prover. Like filenames
supplied as arguments to other options, <file> can use the
following macros:
- @TIME@' expands to the current time
+ @TIME@ expands to the current time
@PREFIX@ expands to the concatenation of strings given
by /logPrefix options
@FILE@ expands to the last filename specified on the
@@ -2271,11 +2262,6 @@ namespace Microsoft.Boogie {
/useArrayTheory : use Z3's native theory (as opposed to axioms). Currently
implies /monomorphize.
- SMT-Lib specific options:
- /smtOutput:<file> : Path and basename to which the prover output is
- written (default: boogie-vc-@PROC@.smt). The same
- macros as in /proverLog can be used.
-
/z3types : generate multi-sorted VC that make use of Z3 types
/z3lets:<n> : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
3 - (default) any
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 756f20b6..be6695e8 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -57,6 +57,29 @@ namespace Microsoft.Boogie {
// || base.Parse(opt)
}
+ public virtual string Help
+ {
+ get
+ {
+ return
+@"
+Generic prover options :
+~~~~~~~~~~~~~~~~~~~~~~~
+LOG_FILE=<string> Log input for the theorem prover. The string @PROC@ in the filename
+ causes there to be one prover log file per verification condition,
+ and is expanded to the name of the procedure that the verification
+ condition is for.
+APPEND_LOG_FILE=<bool> Append, rather than overwrite the log file.
+MEMORY_LIMIT=<int> Memory limit of the prover in megabytes.
+VERBOSITY=<int> The higher, the more verbose.
+TIME_LIMIT=<int> Time limit per verification condition in miliseconds.
+
+The generic options may or may not be used by the prover plugin.
+";
+
+ }
+ }
+
public virtual void Parse(List<string/*!*/>/*!*/ opts) {
Contract.Requires(cce.NonNullElements(opts));
StringBuilder sb = new StringBuilder(stringRepr);
@@ -72,7 +95,7 @@ namespace Microsoft.Boogie {
PostParse();
}
- protected virtual void PostParse() {
+ public virtual void PostParse() {
if (LogFilename != null && LogFilename.Contains("@PROC@")) {
SeparateLogFiles = true;
}
@@ -80,7 +103,7 @@ namespace Microsoft.Boogie {
protected void ReportError(string msg) {
Contract.Requires(msg != null);
- throw new OptionException(msg);
+ throw new OptionException(msg + "\n\n" + Help);
}
protected virtual bool ParseString(string opt, string name, ref string field) {
@@ -136,7 +159,6 @@ namespace Microsoft.Boogie {
return false;
}
- static int sequenceNumber = 0;
public virtual TextWriter OpenLog(string/*?*/ descName) {
if (LogFilename != null) {
string filename = LogFilename;
diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 3544458e..60a8de22 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -57,7 +57,7 @@ namespace Microsoft.Boogie.Isabelle {
- protected override void PostParse() {
+ public override void PostParse() {
base.PostParse();
if (filename == null) {
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index a0686adc..f1c4efcd 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -20,6 +20,33 @@ using Microsoft.Boogie.Simplify;
namespace Microsoft.Boogie.SMTLib
{
+ class SMTLibProverOptions : ProverOptions
+ {
+ public string Output = "boogie-vc-@PROC@.smt";
+
+ protected override bool Parse(string opt)
+ {
+ return
+ ParseString(opt, "OUTPUT", ref Output) ||
+ base.Parse(opt);
+ }
+
+ public override string Help
+ {
+ get
+ {
+ return
+@"
+SMT-specific options:
+~~~~~~~~~~~~~~~~~~~~~
+OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.smt.
+
+" + base.Help;
+ // DIST requires non-public binaries
+ }
+ }
+ }
+
public class SMTLibProcessTheoremProver : LogProverInterface
{
private readonly DeclFreeProverContext ctx;
@@ -149,7 +176,7 @@ void ObjectInvariant()
Contract.Requires(descriptiveName != null);
Contract.Ensures(Contract.Result<TextWriter>() != null);
- string filename = CommandLineOptions.Clo.SMTLibOutputPath;
+ string filename = ((SMTLibProverOptions)options).Output;
filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
return new StreamWriter(filename, false);
}
@@ -300,6 +327,11 @@ void ObjectInvariant()
return new DeclFreeProverContext(gen, genOptions);
}
+ public override ProverOptions BlankProverOptions()
+ {
+ return new SMTLibProverOptions();
+ }
+
protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options,
VCExpressionGenerator gen,
DeclFreeProverContext ctx) {
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index 2b2590d1..4b710495 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -20,6 +20,33 @@ using Microsoft.Boogie.Simplify;
namespace Microsoft.Boogie.TPTP
{
+ class TPTPProverOptions : ProverOptions
+ {
+ public string Output = "boogie-vc-@PROC@.tptp";
+
+ protected override bool Parse(string opt)
+ {
+ return
+ ParseString(opt, "OUTPUT", ref Output) ||
+ base.Parse(opt);
+ }
+
+ public override string Help
+ {
+ get
+ {
+ return
+@"
+TPTP-specific options:
+~~~~~~~~~~~~~~~~~~~~~~
+OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.tptp.
+
+" + base.Help;
+ // DIST requires non-public binaries
+ }
+ }
+ }
+
public class TPTPProcessTheoremProver : LogProverInterface
{
private readonly DeclFreeProverContext ctx;
@@ -144,7 +171,7 @@ namespace Microsoft.Boogie.TPTP
Contract.Requires(descriptiveName != null);
Contract.Ensures(Contract.Result<TextWriter>() != null);
- string filename = CommandLineOptions.Clo.SMTLibOutputPath;
+ string filename = ((TPTPProverOptions)options).Output;
filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
return new StreamWriter(filename, false);
}
@@ -301,6 +328,11 @@ namespace Microsoft.Boogie.TPTP
return new DeclFreeProverContext(gen, genOptions);
}
+ public override ProverOptions BlankProverOptions()
+ {
+ return new TPTPProverOptions();
+ }
+
protected virtual TPTPProcessTheoremProver SpawnProver(ProverOptions options,
VCExpressionGenerator gen,
DeclFreeProverContext ctx)
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index af9668d4..9fd87127 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -123,7 +123,7 @@ void ObjectInvariant()
base.Parse(opt);
}
- protected override void PostParse()
+ public override void PostParse()
{
base.PostParse();
@@ -133,12 +133,11 @@ void ObjectInvariant()
}
}
- public string Help
+ public override string Help
{
get
{
- return
- // base.Help +
+ return
@"
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
@@ -149,7 +148,8 @@ Obscure options:
~~~~~~~~~~~~~~~~
DIST=<bool> Use z3-dist.exe binary.
REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
-";
+
+" + base.Help;
// DIST requires non-public binaries
}
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index eeaab21d..5d7e5c97 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -134,6 +134,7 @@ namespace Microsoft.Boogie {
options.LogFilename = logFilePath;
if (appendLogFile)
options.AppendLogFile = appendLogFile;
+ options.PostParse();
}
options.Parse(CommandLineOptions.Clo.ProverOptions);
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 21:44:56 +0000