1 files changed, 0 insertions, 136 deletions
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
deleted file mode 100644
index fa1b844e..00000000
--- a/Source/Provers/Z3/Inspector.cs
+++ /dev/null
@@ -1,136 +0,0 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using util;
-using Microsoft.Contracts;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
-  internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
-    public Dictionary<string!,bool>! Labels = new Dictionary<string!,bool>();
-
-    public static Dictionary<string!,bool>! FindLabels(VCExpr! expr) {
-      FindLabelsVisitor! visitor = new FindLabelsVisitor();
-      visitor.Traverse(expr, true);
-      return visitor.Labels;
-    }
-    
-    protected override bool StandardResult(VCExpr! node, bool arg) {
-      VCExprNAry nary = node as VCExprNAry;
-      if (nary != null) {
-        VCExprLabelOp lab = nary.Op as VCExprLabelOp;
-        if (lab != null) {
-          Labels[lab.label] = lab.pos;
-        }
-      }
-      return true;      
-    }
-  }
-
-  internal class Inspector {
-    [Rep] protected readonly Process! inspector;
-    [Rep] readonly TextReader! fromInspector;
-    [Rep] readonly TextWriter! toInspector;
-
-    public Inspector(Z3InstanceOptions! opts)
-    {
-      ProcessStartInfo! psi = new ProcessStartInfo(opts.Inspector);
-      psi.CreateNoWindow = true;
-      psi.UseShellExecute = false;
-      psi.RedirectStandardInput = true;
-      psi.RedirectStandardOutput = true;
-      psi.RedirectStandardError = false;
-
-      try 
-      {
-        Process inspector = Process.Start(psi);
-        this.inspector = inspector;
-        fromInspector = inspector.StandardOutput;
-        toInspector = inspector.StandardInput;
-      } 
-      catch (System.ComponentModel.Win32Exception e)
-      {
-        throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
-      }
-    }
-
-    public void NewProver()
-    {
-    }
-
-    public void NewProblem(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
-    {
-      Dictionary<string!,bool>! labels = FindLabelsVisitor.FindLabels(vc);
-      toInspector.WriteLine("PROBLEM " + descriptiveName);
-      toInspector.WriteLine("TOKEN BEGIN");
-      foreach (string! lab in labels.Keys) {
-        string! no = lab.Substring(1);
-        Absy! absy = handler.Label2Absy(no);
-        IToken tok = absy.tok;
-        AssertCmd assrt = absy as AssertCmd;
-        Block blk = absy as Block;
-        string val = tok.val; // might require computation, so cache it
-        if (val == "foo" || tok.filename == null) continue; // no token
-
-        toInspector.Write("TOKEN ");
-        toInspector.Write(lab);
-        toInspector.Write(" ");
-
-        if (assrt != null) {
-          toInspector.Write("ASSERT");
-          string errData = assrt.ErrorData as string;
-          if (errData != null) {
-            val = errData;
-          } else if (assrt.ErrorMessage != null) {
-            val = assrt.ErrorMessage;
-          }
-        } else if (blk != null) {
-          toInspector.Write("BLOCK ");
-          toInspector.Write(blk.Label);
-        } else {
-          assume false;
-        }
-        if (val == null || val == "assert" || val == "ensures") { val = ""; }
-
-        if (absy is LoopInitAssertCmd) {
-          val += " (loop entry)";
-        } else if (absy is LoopInvMaintainedAssertCmd) {
-          val += " (loop body)";
-        } else if (val.IndexOf("#VCCERR") >= 0) { 
-          // skip further transformations
-        } else if (absy is AssertRequiresCmd) {
-          AssertRequiresCmd req = (AssertRequiresCmd)absy;
-          IToken t2 = req.Requires.tok;
-          string tval = t2.val;
-          if (tval == "requires")
-            tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);
-          string call = "";
-          if (val != "call") call = " in call to " + val;
-          val = string.Format("precondition {0}{1}", tval, call);
-        }
-
-        val = val.Replace("\r", "").Replace("\n", " ");
-
-        toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
-      }
-      toInspector.WriteLine("TOKEN END");
-    }
-
-    public void StatsLine(string! line)
-    {
-      toInspector.WriteLine(line);
-      toInspector.Flush();
-    }
-  }
-}