summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar akashlal <akashl@AKASHL-LT.fareast.corp.microsoft.com>2015-05-01 11:21:22 +0530
committerGravatar akashlal <akashl@AKASHL-LT.fareast.corp.microsoft.com>2015-05-01 11:21:22 +0530
commitfacbadfc4dc5e17e85f19f4b25ce4473478b9958 (patch)
tree58cd51ddf42cc7c5d43ca009d41b2fb96a659062
parent0f5533a8679a6b0e68cc587582dae8ea49701526 (diff)
AbsHoudini: made disjunct bound a parameter
-rw-r--r--Source/Houdini/AbstractHoudini.cs28
1 files changed, 15 insertions, 13 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 3415ae78..fcd41656 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -1378,7 +1378,6 @@ namespace Microsoft.Boogie.Houdini {
class Disjunct
{
- public static int DisjunctBound = 3;
HashSet<int> pos;
HashSet<int> neg;
bool isTrue;
@@ -1390,7 +1389,7 @@ namespace Microsoft.Boogie.Houdini {
neg = new HashSet<int>();
}
- public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg, int bound)
{
this.isTrue = false;
this.pos = new HashSet<int>(pos);
@@ -1401,7 +1400,7 @@ namespace Microsoft.Boogie.Houdini {
this.pos = new HashSet<int>();
this.neg = new HashSet<int>();
}
- if (this.pos.Count + this.neg.Count > DisjunctBound)
+ if (this.pos.Count + this.neg.Count > bound)
{
// Set to true
this.isTrue = true;
@@ -1411,14 +1410,14 @@ namespace Microsoft.Boogie.Houdini {
}
- public Disjunct OR(Disjunct that)
+ public Disjunct OR(Disjunct that, int bound)
{
if (isTrue)
return this;
if (that.isTrue)
return that;
- return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
+ return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg), bound);
}
public bool Implies(Disjunct that)
@@ -1441,17 +1440,19 @@ namespace Microsoft.Boogie.Houdini {
// Conjunction of Disjuncts
List<Disjunct> conjuncts;
+ int DisjunctBound;
bool isFalse;
- public PredicateAbsElem()
+ public PredicateAbsElem(int bound)
{
this.conjuncts = new List<Disjunct>();
this.isFalse = true;
+ this.DisjunctBound = bound;
}
public IAbstractDomain Bottom()
{
- return new PredicateAbsElem();
+ return new PredicateAbsElem(DisjunctBound);
}
public IAbstractDomain MakeTop(out bool changed)
@@ -1462,7 +1463,7 @@ namespace Microsoft.Boogie.Houdini {
return this;
}
changed = true;
- var ret = new PredicateAbsElem();
+ var ret = new PredicateAbsElem(DisjunctBound);
ret.isFalse = false;
return ret;
}
@@ -1476,21 +1477,21 @@ namespace Microsoft.Boogie.Houdini {
if (!this.isFalse && conjuncts.Count == 0)
return this;
- var ret = new PredicateAbsElem();
+ var ret = new PredicateAbsElem(DisjunctBound);
ret.isFalse = false;
for (int i = 0; i < state.Count; i++)
{
var b = (state[i] as Model.Boolean).Value;
Disjunct d = null;
- if (b) d = new Disjunct(new int[] { i }, new int[] { });
- else d = new Disjunct(new int[] { }, new int[] { i });
+ if (b) d = new Disjunct(new int[] { i }, new int[] { }, DisjunctBound);
+ else d = new Disjunct(new int[] { }, new int[] { i }, DisjunctBound);
if (isFalse)
ret.AddDisjunct(d);
else
{
- conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
+ conjuncts.Iter(c => ret.AddDisjunct(c.OR(d, DisjunctBound)));
}
}
@@ -2213,7 +2214,8 @@ namespace Microsoft.Boogie.Houdini {
System.Tuple.Create("HoudiniConst", HoudiniConst.GetBottom() as IAbstractDomain),
System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),
System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),
- System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),
+ System.Tuple.Create("PredicateAbs", new PredicateAbsElem(3) as IAbstractDomain),
+ System.Tuple.Create("PredicateAbsFull", new PredicateAbsElem(1000) as IAbstractDomain),
System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),
System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),
System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),