diff options
| author |  Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2012-02-29 14:36:46 +0530 |
|---|---|---|
| committer | Unknown <akashl@akash-desk.fareast.corp.microsoft.com> | 2012-02-29 14:36:46 +0530 |
| commit | cfdcb3e47a026b1cab1ed51dd5a13651155ef871 (patch) | |
| tree | c0b08f9faf6b6de47a5d93647322655bbbf0fa40 /Source/VCGeneration/Check.cs | |
| parent | 8d265ad351152a075e39d07b63148a746ef103f3 (diff) | |
Cleaned up code by getting rid of ApiProverInterface.
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 51 |
1 files changed, 39 insertions, 12 deletions
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) {
|