diff options
| -rw-r--r-- | Source/Core/LinearSets.cs | 41 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 10 |
2 files changed, 31 insertions, 20 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 6ceacdf7..5769cbdf 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -425,7 +425,10 @@ namespace Microsoft.Boogie foreach (var domainName in linearDomains.Keys)
{
var domain = linearDomains[domainName];
- callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }));
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ callCmd.Ins.Add(expr);
}
}
else if (callCmd.InParallelWith != null)
@@ -435,7 +438,10 @@ namespace Microsoft.Boogie foreach (var domainName in linearDomains.Keys)
{
var domain = linearDomains[domainName];
- callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }));
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ callCmd.Ins.Add(expr);
}
callCmd = callCmd.InParallelWith;
}
@@ -445,17 +451,17 @@ namespace Microsoft.Boogie Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
foreach (var domainName in linearDomains.Keys)
{
- var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
- expr.Type = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { linearDomains[domainName].elementType }, Type.Bool);
- domainNameToExpr[domainName] = expr;
+ domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
}
foreach (Variable v in availableLocalLinearVars[callCmd])
{
var domainName = FindDomainName(v);
var domain = linearDomains[domainName];
IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] });
- expr.Type = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { linearDomains[domainName].elementType }, Type.Bool);
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool),
+ new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
domainNameToExpr[domainName] = expr;
}
foreach (var domainName in linearDomains.Keys)
@@ -559,16 +565,6 @@ namespace Microsoft.Boogie return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }), e, Expr.True);
}
- List<AssignLhs> MkAssignLhss(params Variable[] args)
- {
- List<AssignLhs> lhss = new List<AssignLhs>();
- foreach (Variable arg in args)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, arg)));
- }
- return lhss;
- }
-
List<Expr> MkExprs(params Expr[] args)
{
return new List<Expr>(args);
@@ -589,7 +585,10 @@ namespace Microsoft.Boogie e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));
disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);
}
- return new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);
+ var expr = new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ return expr;
}
}
@@ -735,6 +734,12 @@ namespace Microsoft.Boogie axiomExpr.Typecheck(new TypecheckingContext(null));
axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
+
+ foreach (var axiom in axioms)
+ {
+ axiom.Expr.Resolve(new ResolutionContext(null));
+ axiom.Expr.Typecheck(new TypecheckingContext(null));
+ }
}
}
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index eaafafc5..aaee1ff0 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -201,14 +201,20 @@ namespace Microsoft.Boogie Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
foreach (var domainName in linearTypechecker.linearDomains.Keys)
{
- domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ domainNameToExpr[domainName] = expr;
}
foreach (Variable v in availableLocalLinearVars)
{
var domainName = linearTypechecker.FindDomainName(v);
var domain = linearTypechecker.linearDomains[domainName];
IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ domainNameToExpr[domainName] = expr;
}
return domainNameToExpr;
}
|