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/Model | |
| 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/Model')
| -rw-r--r-- | Source/Model/Model.cs | 22 | ||||
| -rw-r--r-- | Source/Model/ModelParser.cs | 4 |
2 files changed, 8 insertions, 18 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) { |