diff options
| author |  akashlal <unknown> | 2013-06-19 11:53:51 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2013-06-19 11:53:51 +0530 |
| commit | cb5d6e5cd7708e9452953b5c189af85d709f0074 (patch) | |
| tree | 38f803ab1e44c6f1734f01386cc269ace5f48b2e /Source/Houdini | |
| parent | 6fcc7aaf9259e8cff46205b1d409cf09b0007464 (diff) | |
AbsHoudini: Bug fix, with bv constants.
Diffstat (limited to 'Source/Houdini')
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 32 |
1 files changed, 21 insertions, 11 deletions
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index c2ff238f..a9fae923 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -402,12 +402,14 @@ namespace Microsoft.Boogie.Houdini { private Model.Element getValue(VCExpr arg, Model model)
{
-
+
+
if (arg is VCExprLiteral)
{
//return model.GetElement(arg.ToString());
return model.MkElement(arg.ToString());
}
+
else if (arg is VCExprVar)
{
var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
@@ -427,19 +429,27 @@ namespace Microsoft.Boogie.Houdini { return null;
}
}
- else
+ else if (arg is VCExprNAry && (arg as VCExprNAry).Op is VCExprBvOp)
{
- var val = prover.Evaluate(arg);
- if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
+ // support for BV constants
+ var bvc = (arg as VCExprNAry)[0] as VCExprLiteral;
+ if (bvc != null)
{
- return model.MkElement(val.ToString());
+ var ret = model.TryMkElement(bvc.ToString() + arg.Type.ToString());
+ if (ret != null && (ret is Model.BitVector)) return ret;
}
- else
- {
- Debug.Assert(false);
- }
- return null;
}
+
+ var val = prover.Evaluate(arg);
+ if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
+ {
+ return model.MkElement(val.ToString());
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return null;
}
// Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"
@@ -1983,7 +1993,7 @@ namespace Microsoft.Boogie.Houdini { private static void RegisterFunction(Function func)
{
- var attr = QKeyValue.FindStringAttribute(func.Attributes, "builtin");
+ var attr = QKeyValue.FindStringAttribute(func.Attributes, "bvbuiltin");
if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv)
bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func);
}
|