diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 3 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 108 | ||||
| -rw-r--r-- | Source/Model/Model.cs | 83 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 14 |
4 files changed, 186 insertions, 22 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index e62a98cb..dca9b066 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1816,6 +1816,9 @@ namespace Microsoft.Boogie { if (IsFree) {
stream.Write("free ");
}
+ if (IsAsync) {
+ stream.Write("async ");
+ }
stream.Write("call ");
EmitAttributes(stream, Attributes);
string sep = "";
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index c092139d..63a76eb2 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -414,6 +414,10 @@ namespace Microsoft.Boogie foreach (LinearDomain domain in linearDomains.Values)
{
program.TopLevelDeclarations.Add(domain.allocator);
+ foreach (Axiom axiom in domain.axioms)
+ {
+ program.TopLevelDeclarations.Add(axiom);
+ }
}
}
@@ -596,6 +600,7 @@ namespace Microsoft.Boogie public Function mapOrBool;
public Function mapImpBool;
public Function mapConstBool;
+ public List<Axiom> axioms;
public LinearDomain(Program program, Variable var, string domainName)
{
@@ -606,6 +611,7 @@ namespace Microsoft.Boogie this.elementType = mapType.Arguments[0];
}
this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool)));
+ this.axioms = new List<Axiom>();
MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);
MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);
@@ -613,29 +619,121 @@ namespace Microsoft.Boogie new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapOrBool.AddAttribute("builtin", "MapOr");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapOrBool.AddAttribute("builtin", "MapOr");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapImpBool = new Function(Token.NoToken, "linear@MapImp",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapImpBool.AddAttribute("builtin", "MapImp");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapImpBool.AddAttribute("builtin", "MapImp");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstBool = new Function(Token.NoToken, "linear@MapConstBool",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapConstBool.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstBool.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie));
+ var trueAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), trueTerm);
+ trueAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));
+ var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie));
+ var falseAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));
+ falseAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
+ }
this.mapEqInt = new Function(Token.NoToken, "linear@MapEq",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapEqInt.AddAttribute("builtin", "MapEq");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapEqInt.AddAttribute("builtin", "MapEq");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstInt = new Function(Token.NoToken, "linear@MapConstInt",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
- this.mapConstInt.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstInt.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
}
}
}
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 23bbb1f9..b2bc0410 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -748,27 +748,25 @@ namespace Microsoft.Boogie line = line.Replace("(", " ( ");
line = line.Replace(")", " ) ");
+ line = line.Replace(",", " ");
var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
List<object> newTuple = new List<object>();
- Stack<List<object>> wordStack = new Stack<List<object>>();
+ Stack<int> wordStack = new Stack<int>();
for (int i = 0; i < tuple.Length; i++) {
string elem = tuple[i];
if (elem == "(") {
- List<object> ls = new List<object>();
- wordStack.Push(ls);
+ wordStack.Push(newTuple.Count - 1);
}
else if (elem == ")") {
- List<object> ls = wordStack.Pop();
- if (wordStack.Count > 0) {
- wordStack.Peek().Add(ls);
- }
- else {
- newTuple.Add(ls);
+ int openParenIndex = wordStack.Pop();
+ List<object> ls = new List<object>();
+ for (int j = openParenIndex; j < newTuple.Count; j++)
+ {
+ ls.Add(newTuple[j]);
}
- }
- else if (wordStack.Count > 0) {
- wordStack.Peek().Add(elem);
+ newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex);
+ newTuple.Add(ls);
}
else {
newTuple.Add(elem);
@@ -777,6 +775,67 @@ namespace Microsoft.Boogie return newTuple;
}
+ /*
+ List<object> GetFunctionTuple(string newLine)
+ {
+ if (newLine == null)
+ return null;
+ newLine = bv.Replace(newLine, "bv${1}");
+ string line = newLine;
+ int openParenCounter = CountOpenParentheses(newLine, 0);
+ if (!newLine.Contains("}"))
+ {
+ while (openParenCounter > 0)
+ {
+ newLine = ReadLine();
+ if (newLine == null)
+ {
+ return null;
+ }
+ line += newLine;
+ openParenCounter = CountOpenParentheses(newLine, openParenCounter);
+ }
+ }
+
+ line = line.Replace("(", " ( ");
+ line = line.Replace(")", " ) ");
+ var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
+
+ List<object> newTuple = new List<object>();
+ Stack<List<object>> wordStack = new Stack<List<object>>();
+ for (int i = 0; i < tuple.Length; i++)
+ {
+ string elem = tuple[i];
+ if (elem == "(")
+ {
+ List<object> ls = new List<object>();
+ wordStack.Push(ls);
+ }
+ else if (elem == ")")
+ {
+ List<object> ls = wordStack.Pop();
+ if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(ls);
+ }
+ else
+ {
+ newTuple.Add(ls);
+ }
+ }
+ else if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(elem);
+ }
+ else
+ {
+ newTuple.Add(elem);
+ }
+ }
+ return newTuple;
+ }
+ */
+
string[] GetWords(string line)
{
if (line == null)
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index cf125c76..da73dea1 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -709,15 +709,19 @@ namespace Microsoft.Boogie.SMTLib var builtin = ExtractBuiltin(op.Func);
var datatype = ExtractDatatype(op.Func);
if (builtin != null)
- printedName = builtin;
+ {
+ printedName = CheckMapApply(builtin, node);
+ }
else if (datatype != null)
- printedName = datatype;
+ {
+ printedName = datatype;
+ }
else
- printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ {
+ printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ }
Contract.Assert(printedName != null);
- printedName = CheckMapApply(printedName, node);
-
WriteApplication(printedName, node, options);
return true;
|