diff options
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) { |