diff options
| author |  Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2012-02-23 13:52:02 -0800 |
|---|---|---|
| committer | Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2012-02-23 13:52:02 -0800 |
| commit | dc8e43c41b46e8d2ae9bc93caa97f7b7d891b5df (patch) | |
| tree | be54b512a45481d6164f7127664be66a0ce1652d /Source/Provers | |
| parent | 51e9ec1d1b9fd9d707a7eb5b9c903e266efbdad1 (diff) | |
using model instead of labels
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 41 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 5 |
2 files changed, 44 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 40492ce4..7ffe8323 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -187,7 +187,7 @@ namespace Microsoft.Boogie.SMTLib if (common.Length == 0) {
SendCommon("(set-option :print-success false)");
SendCommon("(set-info :smt-lib-version 2.0)");
- if (options.ExpectingModel())
+ if (options.ProduceModel())
SendCommon("(set-option :produce-models true)");
foreach (var opt in options.SmtOptions) {
SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
@@ -449,9 +449,38 @@ namespace Microsoft.Boogie.SMTLib }
}
+ private string[] CalculatePath() {
+ SendThisVC("(get-value ((ControlFlow @cfc 0)))");
+ var path = new List<string>();
+ while (true) {
+ var resp = Process.GetProverResponse();
+ if (resp == null)
+ break;
+ if (!(resp.Name == "" && resp.ArgCount == 1)) break;
+ resp = resp.Arguments[0];
+ if (!(resp.Name == "" && resp.ArgCount == 2)) break;
+ resp = resp.Arguments[1];
+ var v = resp.Name;
+ if (v == "-" && resp.ArgCount == 1)
+ v += resp.Arguments[0].Name;
+ else if (resp.ArgCount != 0)
+ break;
+ if (v.StartsWith("-")) {
+ path.Add("@" + v.Substring(1));
+ break;
+ }
+ else {
+ path.Add("+" + v);
+ }
+ SendThisVC("(get-value ((ControlFlow @cfc " + v + ")))");
+ }
+ return path.ToArray();
+ }
+
private string[] GetLabelsInfo(ErrorHandler handler)
{
- SendThisVC("(labels)");
+ if (CommandLineOptions.Clo.UseLabels)
+ SendThisVC("(labels)");
if (options.ExpectingModel())
SendThisVC("(get-model)");
Process.Ping();
@@ -499,6 +528,14 @@ namespace Microsoft.Boogie.SMTLib }
}
+ if (!CommandLineOptions.Clo.UseLabels) {
+ res = CalculatePath();
+ if (res.Length == 0)
+ res = null;
+ else
+ labelNums = res.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
+ }
+
if (labelNums != null) {
ErrorModel m = null;
if (theModel != null)
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index b7b7f24d..6fe025c0 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -41,6 +41,11 @@ namespace Microsoft.Boogie.SMTLib public string Inspector = null;
public bool OptimizeForBv = false;
+ public bool ProduceModel() {
+ return !CommandLineOptions.Clo.UseLabels ||
+ ExpectingModel();
+ }
+
public bool ExpectingModel()
{
return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
|