diff options
| -rw-r--r-- | Source/Core/AbsyQuant.ssc | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.ssc | 22 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 27 |
3 files changed, 46 insertions, 9 deletions
diff --git a/Source/Core/AbsyQuant.ssc b/Source/Core/AbsyQuant.ssc index 401492a3..ec98a85c 100644 --- a/Source/Core/AbsyQuant.ssc +++ b/Source/Core/AbsyQuant.ssc @@ -610,6 +610,12 @@ namespace Microsoft.Boogie public Trigger Triggers;
static int SkolemIds = 0;
+ public static int GetNextSkolemId()
+ {
+ SkolemIds++;
+ return SkolemIds;
+ }
+
public readonly int SkolemId;
public QuantifierExpr(IToken! tok, TypeVariableSeq! typeParameters,
diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc index c77c3dc8..0ccbd843 100644 --- a/Source/VCGeneration/Check.ssc +++ b/Source/VCGeneration/Check.ssc @@ -333,6 +333,17 @@ namespace Microsoft.Boogie return 0;
}
+ private string! LookupSkolemConstant(string! name) {
+ foreach (string! functionName in identifierToPartition.Keys)
+ {
+ int index = functionName.LastIndexOf("!");
+ if (index == -1) continue;
+ string! newFunctionName = (!)functionName.Remove(index);
+ if (newFunctionName.Equals(name))
+ return functionName;
+ }
+ return "";
+ }
private string! LookupSkolemFunction(string! name) {
foreach (string! functionName in definedFunctions.Keys)
{
@@ -342,12 +353,19 @@ namespace Microsoft.Boogie if (newFunctionName.Equals(name))
return functionName;
}
- assert false;
return "";
}
public int LookupSkolemFunctionAt(string! functionName, List<int>! values)
{
- List<List<int>>! tuples = this.definedFunctions[LookupSkolemFunction(functionName)];
+ string! actualFunctionName = LookupSkolemFunction(functionName);
+ if (actualFunctionName.Equals(""))
+ {
+ // The skolem function is actually a skolem constant
+ actualFunctionName = LookupSkolemConstant(functionName);
+ assert !actualFunctionName.Equals("");
+ return identifierToPartition[actualFunctionName];
+ }
+ List<List<int>>! tuples = this.definedFunctions[actualFunctionName];
assert tuples.Count > 0;
// the last tuple is a dummy tuple
for (int n = 0; n < tuples.Count - 1; n++)
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index c0144b24..f7afc6cf 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -119,7 +119,7 @@ namespace VC if (impl == null) continue;
Procedure! proc = (!)impl.Proc;
if (proc.FindExprAttribute("inline") != null) {
- LazyInliningInfo info = new LazyInliningInfo(impl, program, implName2LazyInliningInfo.Count);
+ LazyInliningInfo info = new LazyInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId());
implName2LazyInliningInfo[impl.Name] = info;
impl.LocVars.Add(info.controlFlowVariable);
ExprSeq! exprs = new ExprSeq();
@@ -226,7 +226,8 @@ namespace VC }
if (privateVars.Count > 0)
{
- vcexpr = gen.Exists(new List<TypeVariable!>(), privateVars, new List<VCTrigger!>(), new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr);
+ vcexpr = gen.Exists(new List<TypeVariable!>(), privateVars, new List<VCTrigger!>(),
+ new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr);
}
List<VCExpr!> interfaceExprs = new List<VCExpr!>();
@@ -246,7 +247,10 @@ namespace VC triggers.Add(trigger);
interfaceExprVars.Reverse();
- vcexpr = gen.Forall(interfaceExprVars, triggers, vcexpr);
+ Expr e = new LiteralExpr(Token.NoToken, BigNum.FromInt(1));
+ QKeyValue q = new QKeyValue(Token.NoToken, "weight", new List<object!>(new object![] { e }), null);
+ vcexpr = gen.Forall(new List<TypeVariable!>(), interfaceExprVars, triggers,
+ new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);
checker.TheoremProver.PushVCExpression(vcexpr);
info.vcexpr = vcexpr;
@@ -2071,6 +2075,8 @@ namespace VC List<int>! args = new List<int>();
foreach (Expr! expr in naryExpr.Args)
{
+ VCExprVar exprVar;
+ string name;
LiteralExpr litExpr = expr as LiteralExpr;
if (litExpr != null)
{
@@ -2082,6 +2088,14 @@ namespace VC assert idExpr != null;
Variable! var = (!)idExpr.Decl;
+ if (var is Constant)
+ {
+ exprVar = boogieExprTranslator.LookupVariable(var);
+ name = vcExprTranslator.Lookup(exprVar);
+ args.Add(errModel.identifierToPartition[name]);
+ continue;
+ }
+
int index = 0;
List<GlobalVariable!> globalVars = program.GlobalVariables();
foreach (Variable! global in globalVars)
@@ -2117,10 +2131,9 @@ namespace VC continue;
}
- VCExprVar! exprVar = boogieExprTranslator.LookupVariable(var);
- string! name = vcExprTranslator.Lookup(exprVar);
- int partition = errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values);
- args.Add(partition);
+ exprVar = boogieExprTranslator.LookupVariable(var);
+ name = vcExprTranslator.Lookup(exprVar);
+ args.Add(errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values));
}
calleeCounterexamples[assumeCmd] =
new CalleeCounterexampleInfo(
|