From cfdcb3e47a026b1cab1ed51dd5a13651155ef871 Mon Sep 17 00:00:00 2001
From: Unknown <akashl@akash-desk.fareast.corp.microsoft.com>
Date: Wed, 29 Feb 2012 14:36:46 +0530
Subject: Cleaned up code by getting rid of ApiProverInterface.

---
 Source/VCGeneration/Check.cs | 51 +++++++++++++++++++++++++++++++++-----------
 1 file changed, 39 insertions(+), 12 deletions(-)

(limited to 'Source/VCGeneration/Check.cs')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index f0e6b384..d74497c0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -805,6 +805,44 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();
     }
 
+    // (assert vc)
+    public virtual void Assert(VCExpr vc, bool polarity)
+    {
+        throw new NotImplementedException();
+    }
+
+    // (assert implicit-axioms)
+    public virtual void AssertAxioms()
+    {
+        throw new NotImplementedException();
+    }
+
+    // (check-sat)
+    public virtual void Check()
+    {
+        throw new NotImplementedException();
+    }
+
+    // (check-sat + get-unsat-core)
+    public virtual void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+    {
+        throw new NotImplementedException();
+    }
+
+    public virtual Outcome CheckOutcomeCore(ErrorHandler handler)
+    {
+        throw new NotImplementedException();
+    }
+
+    // (push 1)
+    public virtual void Push()
+    {
+        throw new NotImplementedException();
+    }
+
+    // Set theorem prover timeout for the next "check-sat"
+    public virtual void SetTimeOut(int ms)
+    { }
 
     public abstract ProverContext Context {
       get;
@@ -813,6 +851,7 @@ namespace Microsoft.Boogie {
       get;
     }
   }
+
   public class ProverInterfaceContracts : ProverInterface {
     public override ProverContext Context {
       get {
@@ -841,18 +880,6 @@ namespace Microsoft.Boogie {
     }
   }
 
-  // Exposes an api in line with z3's api
-  public abstract class ApiProverInterface : ProverInterface
-  {
-      public abstract void Assert(VCExpr vc, bool polarity);
-      public abstract void AssertAxioms();
-      public abstract void Check();
-      public abstract void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore);
-      public abstract Outcome CheckOutcomeCore(ErrorHandler handler);
-      public abstract void Push();
-      public virtual void SetTimeOut(int ms) { }
-  }
-
   public class ProverException : Exception {
     public ProverException(string s)
       : base(s) {
-- 
cgit v1.2.3