summaryrefslogtreecommitdiff
path: root/Source/VCExpr/VCExprASTPrinter.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/VCExprASTPrinter.cs')
-rw-r--r--Source/VCExpr/VCExprASTPrinter.cs864
1 files changed, 432 insertions, 432 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 8e2f5d12..dac9604c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -1,432 +1,432 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-
-// A simple visitor for turning a VCExpr into a human-readable string
-// (S-expr syntax)
-
-namespace Microsoft.Boogie.VCExprAST {
-
- public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {
- private VCExprOpPrinter OpPrinterVar = null;
- private VCExprOpPrinter/*!*/ OpPrinter {
- get {
- Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
-
- if (OpPrinterVar == null)
- OpPrinterVar = new VCExprOpPrinter(this);
- return OpPrinterVar;
- }
- }
-
- public void Print(VCExpr expr, TextWriter wr) {
- Contract.Requires(wr != null);
- Contract.Requires(expr != null);
- expr.Accept<bool, TextWriter/*!*/>(this, wr);
- }
-
- public bool Visit(VCExprLiteral node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- if (node == VCExpressionGenerator.True) {
- wr.Write("true");
- } else if (node == VCExpressionGenerator.False) {
- wr.Write("false");
- } else if (node is VCExprIntLit) {
- wr.Write(((VCExprIntLit)node).Val);
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- return true;
- }
- public bool Visit(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- VCExprOp/*!*/ op = node.Op;
- Contract.Assert(op != null);
-
- if (op.Equals(VCExpressionGenerator.AndOp) ||
- op.Equals(VCExpressionGenerator.OrOp)) {
- // handle these operators without recursion
-
- wr.Write("({0}",
- op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
- IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);
- Contract.Assert(enumerator != null);
- while (enumerator.MoveNext()) {
- VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
- wr.Write(" ");
- Print(cce.NonNull((VCExpr/*!*/)enumerator.Current), wr);
- }
- }
-
- wr.Write(")");
-
- return true;
- }
-
- return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);
- }
- public bool Visit(VCExprVar node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- wr.Write(node.Name);
- return true;
- }
- public bool Visit(VCExprQuantifier node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
- Contract.Assert(quan != null);
-
- wr.Write("({0} ", quan);
-
- if (node.TypeParameters.Count > 0) {
- wr.Write("<");
- string/*!*/ sep = "";
- foreach (TypeVariable/*!*/ v in node.TypeParameters) {
- Contract.Assert(v != null);
- wr.Write(sep);
- sep = ", ";
- wr.Write("{0}", v.Name);
- }
- wr.Write("> ");
- }
-
- if (node.BoundVars.Count > 0) {
- string/*!*/ sep = "";
- foreach (VCExprVar/*!*/ v in node.BoundVars) {
- Contract.Assert(v != null);
- wr.Write(sep);
- sep = ", ";
- Print(v, wr);
- }
- wr.Write(" ");
- }
-
- wr.Write(":: ");
-
- if (node.Triggers.Count > 0) {
- wr.Write("{0} ", "{");
- string/*!*/ sep = "";
- foreach (VCTrigger/*!*/ t in node.Triggers) {
- Contract.Assert(t != null);
- wr.Write(sep);
- sep = ", ";
- string/*!*/ sep2 = "";
- foreach (VCExpr/*!*/ e in t.Exprs) {
- Contract.Assert(e != null);
- wr.Write(sep2);
- sep2 = "+";
- Print(e, wr);
- }
- }
- wr.Write(" {0} ", "}");
- }
-
- Print(node.Body, wr);
- wr.Write(")");
- return true;
- }
- public bool Visit(VCExprLet node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- wr.Write("(Let ");
-
- string/*!*/ sep = "";
- foreach (VCExprLetBinding/*!*/ b in node) {
- Contract.Assert(b != null);
- wr.Write(sep);
- sep = ", ";
- Print(b.V, wr);
- wr.Write(" = ");
- Print(b.E, wr);
- }
- wr.Write(" ");
-
- Print(node.Body, wr);
- wr.Write(")");
- return true;
- }
- }
-
- public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter/*!*/> {
- private VCExprPrinter/*!*/ ExprPrinter;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(ExprPrinter != null);
- }
-
-
- public VCExprOpPrinter(VCExprPrinter exprPrinter) {
- Contract.Requires(exprPrinter != null);
- this.ExprPrinter = exprPrinter;
- }
-
- private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {
- Contract.Requires(wr != null);
- Contract.Requires(node != null);
- Contract.Requires(op != null);
- wr.Write("({0}", op);
- foreach (VCExpr/*!*/ arg in node) {
- Contract.Assert(arg != null);
- wr.Write(" ");
- ExprPrinter.Print(arg, wr);
- }
- wr.Write(")");
- return true;
- }
-
- public bool VisitNotOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("!", node, wr);
- }
- public bool VisitEqOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("==", node, wr);
- }
- public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("!=", node, wr);
- }
- public bool VisitAndOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- public bool VisitOrOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("Implies", node, wr);
- }
- public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("Distinct", node, wr);
- }
- public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
- Contract.Assert(op != null);
- return PrintNAry("Label " + op.label, node, wr);
- }
- public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("Select", node, wr);
- }
- public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("Store", node, wr);
- }
- public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.add", node, wr);
- }
- public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.sub", node, wr);
- }
- public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.mul", node, wr);
- }
- public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.div", node, wr);
- }
- public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.rem", node, wr);
- }
- public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.min", node, wr);
- }
- public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.max", node, wr);
- }
- public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.leq", node, wr);
- }
- public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.lt", node, wr);
- }
- public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.geq", node, wr);
- }
- public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.gt", node, wr);
- }
- public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("fp.eq", node, wr);
- }
- public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("Bv", node, wr);
- }
- public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("BvExtract", node, wr);
- }
- public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("BvConcat", node, wr);
- }
- public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("if-then-else", node, wr);
- }
- public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) {
- //Contract.Requires(node!=null);
- //Contract.Requires(wr != null);
- VCExprCustomOp op = (VCExprCustomOp)node.Op;
- return PrintNAry(op.Name, node, wr);
- }
- public bool VisitAddOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- if (CommandLineOptions.Clo.ReflectAdd) {
- return PrintNAry("Reflect$Add", node, wr);
- } else {
- return PrintNAry("+", node, wr);
- }
- }
- public bool VisitSubOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("-", node, wr);
- }
- public bool VisitMulOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("*", node, wr);
- }
- public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("div", node, wr);
- }
- public bool VisitModOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("mod", node, wr);
- }
- public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("/", node, wr);
- }
- public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("**", node, wr);
- }
- public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("<", node, wr);
- }
- public bool VisitLeOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("<=", node, wr);
- }
- public bool VisitGtOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry(">", node, wr);
- }
- public bool VisitGeOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry(">=", node, wr);
- }
- public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("<:", node, wr);
- }
- public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("<::", node, wr);
- }
- public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("int", node, wr);
- }
- public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("real", node, wr);
- }
- public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
- Contract.Assert(op != null);
- return PrintNAry(op.Func.Name, node, wr);
- }
- }
-
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+
+// A simple visitor for turning a VCExpr into a human-readable string
+// (S-expr syntax)
+
+namespace Microsoft.Boogie.VCExprAST {
+
+ public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {
+ private VCExprOpPrinter OpPrinterVar = null;
+ private VCExprOpPrinter/*!*/ OpPrinter {
+ get {
+ Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
+
+ if (OpPrinterVar == null)
+ OpPrinterVar = new VCExprOpPrinter(this);
+ return OpPrinterVar;
+ }
+ }
+
+ public void Print(VCExpr expr, TextWriter wr) {
+ Contract.Requires(wr != null);
+ Contract.Requires(expr != null);
+ expr.Accept<bool, TextWriter/*!*/>(this, wr);
+ }
+
+ public bool Visit(VCExprLiteral node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ if (node == VCExpressionGenerator.True) {
+ wr.Write("true");
+ } else if (node == VCExpressionGenerator.False) {
+ wr.Write("false");
+ } else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ return true;
+ }
+ public bool Visit(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ VCExprOp/*!*/ op = node.Op;
+ Contract.Assert(op != null);
+
+ if (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp)) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
+ IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);
+ Contract.Assert(enumerator != null);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Print(cce.NonNull((VCExpr/*!*/)enumerator.Current), wr);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);
+ }
+ public bool Visit(VCExprVar node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ wr.Write(node.Name);
+ return true;
+ }
+ public bool Visit(VCExprQuantifier node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
+ Contract.Assert(quan != null);
+
+ wr.Write("({0} ", quan);
+
+ if (node.TypeParameters.Count > 0) {
+ wr.Write("<");
+ string/*!*/ sep = "";
+ foreach (TypeVariable/*!*/ v in node.TypeParameters) {
+ Contract.Assert(v != null);
+ wr.Write(sep);
+ sep = ", ";
+ wr.Write("{0}", v.Name);
+ }
+ wr.Write("> ");
+ }
+
+ if (node.BoundVars.Count > 0) {
+ string/*!*/ sep = "";
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
+ wr.Write(sep);
+ sep = ", ";
+ Print(v, wr);
+ }
+ wr.Write(" ");
+ }
+
+ wr.Write(":: ");
+
+ if (node.Triggers.Count > 0) {
+ wr.Write("{0} ", "{");
+ string/*!*/ sep = "";
+ foreach (VCTrigger/*!*/ t in node.Triggers) {
+ Contract.Assert(t != null);
+ wr.Write(sep);
+ sep = ", ";
+ string/*!*/ sep2 = "";
+ foreach (VCExpr/*!*/ e in t.Exprs) {
+ Contract.Assert(e != null);
+ wr.Write(sep2);
+ sep2 = "+";
+ Print(e, wr);
+ }
+ }
+ wr.Write(" {0} ", "}");
+ }
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ public bool Visit(VCExprLet node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ wr.Write("(Let ");
+
+ string/*!*/ sep = "";
+ foreach (VCExprLetBinding/*!*/ b in node) {
+ Contract.Assert(b != null);
+ wr.Write(sep);
+ sep = ", ";
+ Print(b.V, wr);
+ wr.Write(" = ");
+ Print(b.E, wr);
+ }
+ wr.Write(" ");
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ }
+
+ public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter/*!*/> {
+ private VCExprPrinter/*!*/ ExprPrinter;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(ExprPrinter != null);
+ }
+
+
+ public VCExprOpPrinter(VCExprPrinter exprPrinter) {
+ Contract.Requires(exprPrinter != null);
+ this.ExprPrinter = exprPrinter;
+ }
+
+ private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {
+ Contract.Requires(wr != null);
+ Contract.Requires(node != null);
+ Contract.Requires(op != null);
+ wr.Write("({0}", op);
+ foreach (VCExpr/*!*/ arg in node) {
+ Contract.Assert(arg != null);
+ wr.Write(" ");
+ ExprPrinter.Print(arg, wr);
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitNotOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("!", node, wr);
+ }
+ public bool VisitEqOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("==", node, wr);
+ }
+ public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("!=", node, wr);
+ }
+ public bool VisitAndOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ public bool VisitOrOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("Implies", node, wr);
+ }
+ public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("Distinct", node, wr);
+ }
+ public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
+ Contract.Assert(op != null);
+ return PrintNAry("Label " + op.label, node, wr);
+ }
+ public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("Select", node, wr);
+ }
+ public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("Store", node, wr);
+ }
+ public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.add", node, wr);
+ }
+ public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.sub", node, wr);
+ }
+ public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.mul", node, wr);
+ }
+ public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.div", node, wr);
+ }
+ public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.rem", node, wr);
+ }
+ public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.min", node, wr);
+ }
+ public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.max", node, wr);
+ }
+ public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.leq", node, wr);
+ }
+ public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.lt", node, wr);
+ }
+ public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.geq", node, wr);
+ }
+ public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.gt", node, wr);
+ }
+ public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.eq", node, wr);
+ }
+ public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("Bv", node, wr);
+ }
+ public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("BvExtract", node, wr);
+ }
+ public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("BvConcat", node, wr);
+ }
+ public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("if-then-else", node, wr);
+ }
+ public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) {
+ //Contract.Requires(node!=null);
+ //Contract.Requires(wr != null);
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ return PrintNAry(op.Name, node, wr);
+ }
+ public bool VisitAddOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ return PrintNAry("Reflect$Add", node, wr);
+ } else {
+ return PrintNAry("+", node, wr);
+ }
+ }
+ public bool VisitSubOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("-", node, wr);
+ }
+ public bool VisitMulOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("*", node, wr);
+ }
+ public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("div", node, wr);
+ }
+ public bool VisitModOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("mod", node, wr);
+ }
+ public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("/", node, wr);
+ }
+ public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("**", node, wr);
+ }
+ public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("<", node, wr);
+ }
+ public bool VisitLeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("<=", node, wr);
+ }
+ public bool VisitGtOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry(">", node, wr);
+ }
+ public bool VisitGeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry(">=", node, wr);
+ }
+ public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("<:", node, wr);
+ }
+ public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("<::", node, wr);
+ }
+ public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("int", node, wr);
+ }
+ public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("real", node, wr);
+ }
+ public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
+ Contract.Assert(op != null);
+ return PrintNAry(op.Func.Name, node, wr);
+ }
+ }
+
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 00:46:22 +0000