diff options
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 6 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 3 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 3 |
3 files changed, 8 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 42cf89ab..c27f6a48 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -152,10 +152,8 @@ namespace Microsoft.Boogie.SMTLib SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
}
- if (CommandLineOptions.Clo.UseArrayTheory) {
- SendCommon("; skipping logic setting (using arrays)");
- } else {
- SendCommon("(set-logic UFNIA)");
+ if (!string.IsNullOrEmpty(options.Logic)) {
+ SendCommon("(set-logic " + options.Logic + ")");
}
SendCommon("; done setting options\n");
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 0793c614..a874c6c5 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -27,6 +27,9 @@ namespace Microsoft.Boogie.SMTLib // Bitvectors
"extract", "concat",
"bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
+ // arrays
+ "store", "select", "const", "default", "map", "union", "intersect", "difference", "complement",
+ "subset", "array-ext", "as-array", "Array",
// Z3 (and not only?) extensions to bitvectors
"bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0",
"bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 44f91cc2..653b2c15 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -34,6 +34,7 @@ namespace Microsoft.Boogie.SMTLib public List<OptionValue> SmtOptions = new List<OptionValue>();
public List<string> SolverArguments = new List<string>();
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;
@@ -92,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib ParseBool(opt, "USE_Z3", ref UseZ3) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+ ParseString(opt, "LOGIC", ref Logic) ||
base.Parse(opt);
}
@@ -114,6 +116,7 @@ USE_WEIGHTS=<bool> Pass :weight annotations on quantified formulas (defau 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)
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
|