added specific command line options to enable the SMTLIB2 output model parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true

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.