Boogie: Added boolean code expressions (sans well-formedness checks on the input).

1 files changed, 25 insertions, 0 deletions

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 5fb9404d..dedfbc09 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -961,6 +961,31 @@ namespace Microsoft.Boogie.Isabelle {
       return Write(b2i, B2I.Kind.IfThenElse, node);

     }

 

+    public bool VisitCustomOp(VCExprNAry node, B2I b2i) {

+      Contract.Requires(node != null);

+      Contract.Requires(b2i != null);

+      VCExprCustomOp op = (VCExprCustomOp)node.Op;

+

+      Contract.Assert(op.Arity == node.Length);

+      b2i.Write(B2I.Kind.Function, op.Name + " " + node.Length);

+      if (b2i.Context.AllTypes) {

+        b2i.Indent(2);

+

+        // pick the types from the actual arguments

+        foreach (VCExpr arg in node) {

+          Contract.Assert(arg != null);

+          b2i.Write(arg.Type);

+        }

+        b2i.Unindent();

+      }

+      if (b2i.Context.AllTypes) {

+        b2i.Indent(2);

+        b2i.Write(op.Type);

+        b2i.Unindent();

+      }

+      WriteArguments(b2i, node);

+      return true;

+    }

 

     public bool VisitHeapSuccessionOp(VCExprNAry node, B2I b2i) {

       Contract.Requires(node != null);