diff options
author | 2010-04-17 19:14:43 +0000 | |
---|---|---|
committer | 2010-04-17 19:14:43 +0000 | |
commit | d03242f9efa515d848f9166244bfaaa9fefd22b0 (patch) | |
tree | 67c010e1d67394aff7c66d652e4a17e7efddd99a /Source/Provers | |
parent | 584e66329027e1ea3faff5253a0b5554d455df49 (diff) |
First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/Simplify/ProverInterface.ssc | 5 | ||||
-rw-r--r-- | Source/Provers/Z3/Prover.ssc | 34 | ||||
-rw-r--r-- | Source/Provers/Z3/ProverInterface.ssc | 5 | ||||
-rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.ssc | 34 |
4 files changed, 77 insertions, 1 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc index 5e5d8558..74efceb4 100644 --- a/Source/Provers/Simplify/ProverInterface.ssc +++ b/Source/Provers/Simplify/ProverInterface.ssc @@ -567,6 +567,11 @@ namespace Microsoft.Boogie.Simplify private readonly UniqueNamer! Namer;
private readonly BigLiteralAbstracter! LitAbstracter;
+ public override string! Lookup(VCExprVar! var)
+ {
+ return Namer.Lookup(var);
+ }
+
public override string! translate(VCExpr! expr, int polarity) {
Let2ImpliesMutator! letImplier = new Let2ImpliesMutator(Gen);
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc index 44d450c0..eb09576b 100644 --- a/Source/Provers/Z3/Prover.ssc +++ b/Source/Provers/Z3/Prover.ssc @@ -441,6 +441,34 @@ namespace Microsoft.Boogie.Z3 } else if (s[j] == 'v') {
// -> val!..., i.e. no value
partitionToValue.Add(null);
+ } else if (s[j] == '{') {
+ // array
+ List<List<int>!> arrayModel = new List<List<int>!>();
+ string array = s.Substring(j);
+ int index1, index2;
+ string from, to;
+ List<int> tuple = new List<int>();
+ while (0 <= array.IndexOf(';')) {
+ index1 = array.IndexOf('*') + 1;
+ index2 = array.IndexOf(' ');
+ from = array.Substring(index1, index2-index1);
+ tuple.Add(int.Parse(from));
+ array = array.Substring(index2);
+ index1 = array.IndexOf('*') + 1;
+ index2 = array.IndexOf(';');
+ to = array.Substring(index1, index2-index1);
+ array = array.Substring(index2+2);
+ tuple.Add(int.Parse(to));
+ arrayModel.Add(tuple);
+ tuple = new List<int>();
+ }
+ assert array.StartsWith("else ->");
+ index1 = array.IndexOf('*') + 1;
+ index2 = array.IndexOf('}');
+ to = array.Substring(index1, index2-index1);
+ tuple.Add(int.Parse(to));
+ arrayModel.Add(tuple);
+ partitionToValue.Add(arrayModel);
} else {
string numberOrBv = s.Substring(j);
// make number an int, then store it:
@@ -494,8 +522,10 @@ namespace Microsoft.Boogie.Z3 ensures 0 <= result && result <= s.Length;
{
List<string!> identifiers = new List<string!>();
+ int arrowIndex = s.IndexOf('>');
+ assert 0 < arrowIndex;
int j = s.IndexOf('{', 0) + 1; // skip the '{', if present, and set j to 0 otherwise
- if (1 <= j) {
+ if (1 <= j && j < arrowIndex) {
// There is a list of ID's.
assume j < s.Length; // there should be more characters; the ending '}', for one
//ID*
@@ -516,6 +546,8 @@ namespace Microsoft.Boogie.Z3 }
assume j < s.Length; // there should be more characters; the ending '}', for one
}//end ID*
+ } else {
+ j = 0;
}
Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
partitionToIdentifiers.Add(identifiers);
diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc index 9a28eb42..cc788033 100644 --- a/Source/Provers/Z3/ProverInterface.ssc +++ b/Source/Provers/Z3/ProverInterface.ssc @@ -223,6 +223,11 @@ namespace Microsoft.Boogie.Z3 private readonly UniqueNamer! Namer;
private readonly TypeDeclCollector! DeclCollector;
+ public override string! Lookup(VCExprVar! var)
+ {
+ return Namer.Lookup(var);
+ }
+
public override string! translate(VCExpr! expr, int polarity) {
DateTime start = DateTime.Now;
if (CommandLineOptions.Clo.Trace)
diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc index 21aebabe..a45ca206 100644 --- a/Source/Provers/Z3/TypeDeclCollector.ssc +++ b/Source/Provers/Z3/TypeDeclCollector.ssc @@ -35,6 +35,9 @@ namespace Microsoft.Boogie.Z3 KnownVariables = new Dictionary<VCExprVar!, bool> ();
KnownTypes = new Dictionary<Type!, bool> ();
KnownBvOps = new Dictionary<string!, bool> ();
+
+ KnownStoreFunctions = new Dictionary<string!, bool> ();
+ KnownSelectFunctions = new Dictionary<string!, bool> ();
}
internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {
@@ -46,6 +49,9 @@ namespace Microsoft.Boogie.Z3 KnownVariables = new Dictionary<VCExprVar!, bool> (coll.KnownVariables);
KnownTypes = new Dictionary<Type!, bool> (coll.KnownTypes);
KnownBvOps = new Dictionary<string!, bool> (coll.KnownBvOps);
+
+ KnownStoreFunctions = new Dictionary<string!, bool> (coll.KnownStoreFunctions);
+ KnownSelectFunctions = new Dictionary<string!, bool> (coll.KnownSelectFunctions);
}
// not used
@@ -65,6 +71,9 @@ namespace Microsoft.Boogie.Z3 // the names of registered BvConcatOps and BvExtractOps
private readonly IDictionary<string!, bool>! KnownBvOps;
+ private readonly IDictionary<string!, bool>! KnownStoreFunctions;
+ private readonly IDictionary<string!, bool>! KnownSelectFunctions;
+
public List<string!>! AllDeclarations { get {
List<string!>! res = new List<string!> ();
res.AddRange(AllDecls);
@@ -171,6 +180,31 @@ namespace Microsoft.Boogie.Z3 }
}
//
+ } else if (node.Op is VCExprStoreOp) {
+ //
+ string name = SimplifyLikeExprLineariser.StoreOpName(node);
+ if (!KnownStoreFunctions.ContainsKey(name)) {
+ AddDeclaration("(DEFOP " + name +
+ " " + TypeToString(node[0].Type) +
+ " " + TypeToString(node[1].Type) +
+ " " + TypeToString(node[2].Type) +
+ " " + TypeToString(node.Type) +
+ " :BUILTIN store)");
+ KnownStoreFunctions.Add(name, true);
+ }
+ //
+ } else if (node.Op is VCExprSelectOp) {
+ //
+ string name = SimplifyLikeExprLineariser.SelectOpName(node);
+ if (!KnownSelectFunctions.ContainsKey(name)) {
+ AddDeclaration("(DEFOP " + name +
+ " " + TypeToString(node[0].Type) +
+ " " + TypeToString(node[1].Type) +
+ " " + TypeToString(node.Type) +
+ " :BUILTIN select)");
+ KnownSelectFunctions.Add(name, true);
+ }
+ //
} else {
//
VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
|