diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-04-28 13:32:38 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-04-28 13:32:38 -0700 |
| commit | dfb4e6c3a65c8bf7cd95bfe27bf5a33ba0c73f3c (patch) | |
| tree | 583b8b855c384c4228ebfaa006276896c8467b02 /Source/Provers | |
| parent | 386085ef362905d564753e8e6d252540ceef0e85 (diff) | |
Use (get-model) Z3 command; quote skolem-ids
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 40 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 2 |
2 files changed, 25 insertions, 17 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 11b6e2db..7b4d170d 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -359,7 +359,7 @@ namespace Microsoft.Boogie.SMTLib {
SendThisVC("(labels)");
if (options.ExpectingModel())
- SendThisVC("(model)");
+ SendThisVC("(get-model)");
Process.Ping();
List<string> labelNums = null;
@@ -375,25 +375,33 @@ namespace Microsoft.Boogie.SMTLib res = labels;
if (labelNums != null) HandleProverError("Got multiple :labels responses");
labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
- } else if (resp.Name == "model" && resp.ArgCount >= 1) {
- var modelStr = resp[0].Name;
- List<Model> models = null;
- try {
- models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
- } catch (ArgumentException exn) {
- HandleProverError("Model parsing error: " + exn.Message);
+ } else {
+ string modelStr = null;
+ if (resp.Name == "model" && resp.ArgCount >= 1) {
+ modelStr = resp[0].Name;
+ } else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
+ modelStr = resp.Name;
}
- if (models != null) {
- if (models.Count == 0) HandleProverError("Could not parse any models");
- else {
- if (models.Count > 1) HandleProverError("Expecting only one model, got multiple");
- if (theModel != null) HandleProverError("Got multiple :model responses");
- theModel = models[0];
+ if (modelStr != null) {
+ List<Model> models = null;
+ try {
+ models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
+ } catch (ArgumentException exn) {
+ HandleProverError("Model parsing error: " + exn.Message);
+ }
+
+ if (models != null) {
+ if (models.Count == 0) HandleProverError("Could not parse any models");
+ else {
+ if (models.Count > 1) HandleProverError("Expecting only one model, got multiple");
+ if (theModel != null) HandleProverError("Got multiple :model responses");
+ theModel = models[0];
+ }
}
+ } else {
+ HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString());
}
- } else {
- HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString());
}
}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index d06cba3b..3e8a3fc8 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -266,7 +266,7 @@ namespace Microsoft.Boogie.SMTLib if (weight != 1)
wr.Write(" :weight {0}\n", weight);
if (infos.uniqueId != -1)
- wr.Write(" :skolemid {0}\n", infos.uniqueId);
+ wr.Write(" :skolemid |{0}|\n", infos.uniqueId);
WriteTriggers(node.Triggers, options);
wr.Write(")");
|