diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 22:12:51 +0100 |
commit | 0ad93c637c97672fa71c380f9112ea1b7d6572d8 (patch) | |
tree | 81796eee129a7763e3930c3da31c5b4c4aaac5b0 /Source | |
parent | e8e4c58f700242eab9e951e01c8a2ee3cafd89de (diff) |
added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Model/Model.cs | 22 | ||||
-rw-r--r-- | Source/Model/ModelParser.cs | 4 | ||||
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 11 | ||||
-rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 7 | ||||
-rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 11 |
5 files changed, 31 insertions, 24 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 34d39863..7668b370 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -695,20 +695,20 @@ namespace Microsoft.Boogie foreach (var f in functions) f.Substitute(mapping);
}
- public static List<Model> ParseModels(System.IO.TextReader rd, string modelType)
+ public static List<Model> ParseModels(System.IO.TextReader rd, string prover)
{
ModelParser p;
-
- switch (modelType)
+
+ switch (prover)
{
- case "Z3":
- p = new ParserZ3();
+ case "Z3_SMTLIB2":
+ p = new ParserZ3_SMTLIB2();
break;
case "CVC4":
p = new ParserCVC4();
break;
default:
- p = new ParserZ3_2();
+ p = new ParserZ3();
break;
}
@@ -717,15 +717,5 @@ namespace Microsoft.Boogie return p.resModels;
}
-
- public static List<Model> ParseModels(System.IO.TextReader rd)
- {
- ModelParser p = new ParserZ3_2();
-
- p.rd = rd;
- p.Run();
-
- return p.resModels;
- }
}
}
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index bd3be773..9a455662 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -89,7 +89,7 @@ namespace Microsoft.Boogie abstract internal void Run(); } - class ParserZ3_2 : ModelParser + class ParserZ3 : ModelParser { List<object> GetFunctionTokens(string newLine) { @@ -597,7 +597,7 @@ namespace Microsoft.Boogie } } - internal class ParserZ3 : ParserSMT + internal class ParserZ3_SMTLIB2 : ParserSMT { protected override void ParseArray(ref int i) { diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c00545df..68976183 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -542,7 +542,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());
@@ -929,7 +929,14 @@ namespace Microsoft.Boogie.SMTLib try {
switch (options.Solver) {
case SolverKind.Z3:
- models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "Z3");
+ if (options.SMTLib2Model)
+ {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "Z3_SMTLIB2");
+ }
+ else
+ {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
+ }
break;
case SolverKind.CVC4:
models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "CVC4");
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 6b1ffb34..3252dd57 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -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 ||
@@ -94,7 +95,7 @@ namespace Microsoft.Boogie.SMTLib 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;
@@ -115,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);
}
@@ -134,7 +136,7 @@ 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.
@@ -146,6 +148,7 @@ 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 66b1809a..5865a333 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -283,10 +283,17 @@ 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("pp-bv-literals", "false");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+ if (options.SMTLib2Model)
+ {
+ 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.
|