diff options
| -rw-r--r-- | Source/Model/Model.cs | 48 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 21 |
3 files changed, 61 insertions, 10 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 355a277f..7dcd3dd8 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -120,6 +120,7 @@ namespace Microsoft.Boogie internal readonly List<FuncTuple> apps = new List<FuncTuple>();
public IEnumerable<FuncTuple> Apps { get { return apps; } }
public int AppCount { get { return apps.Count; } }
+ private Element @else;
internal Func(Model p, string n, int a) { Model = p; Name = n; Arity = a; }
@@ -128,6 +129,20 @@ namespace Microsoft.Boogie return string.Format("{0}/{1}", Name, Arity);
}
+ public Element Else
+ {
+ get
+ {
+ return @else;
+ }
+ set
+ {
+ if (@else != null)
+ throw new ArgumentException();
+ @else = value;
+ }
+ }
+
public void SetConstant(Element res)
{
if (Arity != 0 || apps.Count > 0)
@@ -512,6 +527,8 @@ namespace Microsoft.Boogie wr.Write("{0} ", a);
wr.WriteLine("-> {0}", app.Result);
}
+ if (f.Else != null)
+ wr.WriteLine(" else -> {0}", f.Else);
wr.WriteLine("}");
}
foreach (var s in States) {
@@ -663,19 +680,42 @@ namespace Microsoft.Boogie if (tuple == null) BadModel("EOF in function table");
if (tuple.Length == 0) continue;
if (tuple.Length == 1 && tuple[0] == "}") break;
- if (tuple.Length < 3 || tuple[tuple.Length - 2] != "->") BadModel("invalid function tuple definition");
- if (tuple[0] == "else") {
- if (tuple[tuple.Length - 1].EndsWith("}"))
+
+ var resultName = tuple[tuple.Length - 1];
+ var isElse = false;
+
+ if (tuple.Length == 1 && fn == null)
+ isElse = true;
+
+ if (!isElse && (tuple.Length < 3 || tuple[tuple.Length - 2] != "->")) BadModel("invalid function tuple definition");
+
+ if (isElse || tuple[0] == "else") {
+ var hasBrace = false;
+ if (resultName.EndsWith("}")) {
+ hasBrace = true;
+ resultName = resultName.Substring(0, resultName.Length - 1);
+ }
+ if (!resultName.StartsWith("#unspec")) {
+ if (fn == null)
+ fn = currModel.TryGetFunc(funName);
+ // if it's still null, we don't know the arity, so just skip it
+ if (fn != null) {
+ fn.Else = GetElt(resultName);
+ }
+ }
+
+ if (hasBrace)
break;
else
continue;
}
+
if (fn == null)
fn = currModel.MkFunc(funName, tuple.Length - 2);
var args = new Element[fn.Arity];
for (int i = 0; i < fn.Arity; ++i)
args[i] = GetElt(tuple[i]);
- fn.AddApp(GetElt(tuple[tuple.Length - 1]), args);
+ fn.AddApp(GetElt(resultName), args);
}
} else {
fn = currModel.MkFunc(funName, 0);
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 8b21861e..80a220cb 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -107,7 +107,7 @@ namespace Microsoft.Boogie.SMTLib // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
options.AddWeakSmtOption("AUTO_CONFIG", "false");
- options.AddWeakSmtOption("MODEL_PARTIAL", "true");
+ //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
options.AddWeakSmtOption("MODEL_V2", "true");
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index da68aac0..e0c89603 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -417,7 +417,10 @@ namespace Microsoft.Boogie { tuples.Add(tpl);
}
var elseTpl = new List<int>();
- elseTpl.Add(elseElt.Id);
+ if (f.Else != null)
+ elseTpl.Add(f.Else.Id);
+ else
+ elseTpl.Add(elseElt.Id);
tuples.Add(elseTpl);
}
}
@@ -458,6 +461,11 @@ namespace Microsoft.Boogie { // get the Func ("it doesn't matter if you get the funk, just as long as the funk gets you", from Ulco Bed's "Get The Funk" on Candy Dulfer's 1990 album Saxuality)
var name = t.Key;
var arity = tuples[0].Count - 1;
+
+ // this may happen if the function only has the else clause; the 1 is just the best guess in such case
+ if (arity == 0)
+ arity = 1;
+
Model.Func f;
if (Regex.IsMatch(name, "^MapType[0-9]*Select$")) {
name = string.Format("[{0}]", arity);
@@ -477,10 +485,13 @@ namespace Microsoft.Boogie { var args = new Model.Element[arity];
foreach (var l in tuples) {
- if (l.Count == 1) continue;
- for (int i = 0; i < f.Arity; ++i)
- args[i] = elts[l[i]];
- f.AddApp(elts[l[f.Arity]], args);
+ if (l.Count == 1) {
+ f.Else = elts[l[0]];
+ } else {
+ for (int i = 0; i < f.Arity; ++i)
+ args[i] = elts[l[i]];
+ f.AddApp(elts[l[f.Arity]], args);
+ }
}
}
|