From 0ad93c637c97672fa71c380f9112ea1b7d6572d8 Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Tue, 9 Jul 2013 22:12:51 +0100 Subject: added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true --- Source/Model/Model.cs | 22 ++++++---------------- Source/Model/ModelParser.cs | 4 ++-- Source/Provers/SMTLib/ProverInterface.cs | 11 +++++++++-- Source/Provers/SMTLib/SMTLibProverOptions.cs | 7 +++++-- Source/Provers/SMTLib/Z3.cs | 11 +++++++++-- 5 files changed, 31 insertions(+), 24 deletions(-) (limited to 'Source') 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 ParseModels(System.IO.TextReader rd, string modelType) + public static List 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 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 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= Use the given SMT solver (z3, cvc3, cvc4; default: z3) +SOLVER= Use the given SMT solver (z3 or cvc4; default: z3) USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) VERBOSITY= 1 - print prover output (default: 0) O:= Pass (set-option : ) to the SMT solver. @@ -146,6 +148,7 @@ Z3-specific options: MULTI_TRACES= Report errors with multiple paths leading to the same assertion. INSPECTOR= Use the specified Z3Inspector binary. OPTIMIZE_FOR_BV= Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. +SMTLIB2_MODEL= 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. -- cgit v1.2.3