diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-09-02 21:38:42 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-09-02 21:38:42 -0700 |
| commit | 7e7c58ddc206933cf23a28acd17dce18f0ce0cd4 (patch) | |
| tree | 77ce77ee2ef4e96d15f85dbe437dc847b0bd43e4 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | b9a6a826992356259535597838204c8bfc2d9d1e (diff) | |
adding support for accessing Z3's generalized array theory
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 70 |
1 files changed, 68 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index ed7beabf..7eafbdfb 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -656,8 +656,7 @@ namespace Microsoft.Boogie.SMTLib return true;
}
- public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
- {
+ public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
Contract.Assert(op != null);
string printedName;
@@ -669,11 +668,78 @@ namespace Microsoft.Boogie.SMTLib printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
Contract.Assert(printedName != null);
+ printedName = CheckMapApply(printedName, node);
+
WriteApplication(printedName, node, options);
return true;
}
+ private static string CheckMapApply(string name, VCExprNAry node) {
+ MapType mapType = node.Type as MapType;
+ Contract.Assume(mapType != null);
+ if (name == "MapConst") {
+ StringBuilder sb = new StringBuilder();
+ TypeToStringHelper(node.Type, sb);
+ return "(as const " + sb.ToString() + ")";
+ }
+ else if (name == "MapAdd") {
+ return "(_ map (+ (Int Int) Int))";
+ }
+ else if (name == "MapSub") {
+ return "(_ map (- (Int Int) Int))";
+ }
+ else if (name == "MapMul") {
+ return "(_ map (* (Int Int) Int))";
+ }
+ else if (name == "MapDiv") {
+ return "(_ map (div (Int Int) Int))";
+ }
+ else if (name == "MapMod") {
+ return "(_ map (mod (Int Int) Int))";
+ }
+ else if (name == "MapEq" || name == "MapIff") {
+ MapType argType = node[0].Type as MapType;
+ Contract.Assume(argType != null);
+ StringBuilder sb = new StringBuilder();
+ TypeToStringHelper(argType.Result, sb);
+ string s = sb.ToString();
+ return "(_ map (= (" + s + " " + s + ") Bool))";
+ }
+ else if (name == "MapGt") {
+ return "(_ map (> (Int Int) Int))";
+ }
+ else if (name == "MapGe") {
+ return "(_ map (>= (Int Int) Int))";
+ }
+ else if (name == "MapLt") {
+ return "(_ map (< (Int Int) Int))";
+ }
+ else if (name == "MapLe") {
+ return "(_ map (<= (Int Int) Int))";
+ }
+ else if (name == "MapOr") {
+ return "(_ map or)";
+ }
+ else if (name == "MapAnd") {
+ return "(_ map and)";
+ }
+ else if (name == "MapNot") {
+ return "(_ map not)";
+ }
+ else if (name == "MapImp") {
+ return "(_ map =>)";
+ }
+ else if (name == "MapIte") {
+ StringBuilder sb = new StringBuilder();
+ TypeToStringHelper(mapType.Result, sb);
+ string s = sb.ToString();
+ return "(_ map (ite (Bool " + s + " " + s + ") " + s + "))";
+ }
+ else {
+ return name;
+ }
+ }
}
}
|