From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/VCExpr/VCExprASTPrinter.cs | 864 +++++++++++++++++++------------------- 1 file changed, 432 insertions(+), 432 deletions(-) (limited to 'Source/VCExpr/VCExprASTPrinter.cs') 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 { - private VCExprOpPrinter OpPrinterVar = null; - private VCExprOpPrinter/*!*/ OpPrinter { - get { - Contract.Ensures(Contract.Result() != 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(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(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 { - 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 { + private VCExprOpPrinter OpPrinterVar = null; + private VCExprOpPrinter/*!*/ OpPrinter { + get { + Contract.Ensures(Contract.Result() != 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(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(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 { + 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); + } + } + + +} -- cgit v1.2.3