Added the port of Z3api. It is simply a port to the latest version of Microsoft.Z3.dll and to C#. It does not work yet.

1 files changed, 74 insertions, 0 deletions

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
new file mode 100644
index 00000000..80f1776e
--- /dev/null
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -0,0 +1,74 @@
+using System;

+using System.Collections;

+using System.Collections.Generic;

+using System.Threading;

+using System.IO;

+using System.Diagnostics;

+using Microsoft.Contracts;

+using Microsoft.Boogie.AbstractInterpretation;

+using Microsoft.Boogie;

+using Microsoft.Boogie.Z3;

+using Microsoft.Z3;

+using Microsoft.Boogie.VCExprAST;

+

+namespace Microsoft.Boogie.Z3 {

+  public class Z3StubContext:Z3Context {

+    class Z3StubPatternAst: Z3PatternAst {}

+    class Z3StubTermAst: Z3TermAst {}

+    class Z3StubLabeledLiterals: Z3LabeledLiterals {}

+  

+    public void CreateBacktrackPoint(){}

+    public void Backtrack(){}

+    public void AddAxiom(VCExpr vc) {}

+    public void AddConjecture(VCExpr vc){}

+    public void AddSmtlibString(string smtlibString) {}

+    public string GetDeclName(Z3ConstDeclAst constDeclAst) {

+      return "";

+    }

+    public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {

+      return new Z3StubPatternAst();

+    }

+    public Z3TermAst MakeForall(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

+      return new Z3StubTermAst();

+    }

+    public Z3TermAst MakeExists(List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

+      return new Z3StubTermAst();

+    }

+    public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {

+      return new List<string>();

+    }

+    public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {

+      boogieErrors = new List<Z3ErrorModelAndLabels>();

+      return ProverInterface.Outcome.Undetermined;

+    }

+    public void TypeCheckBool(Z3TermAst t){}

+    public void TypeCheckInt(Z3TermAst t){}

+    public void DeclareType(string typeName) {}

+    public void DeclareConstant(string constantName, Type boogieType) {}

+    public Z3TermAst MakeBoundVariable(uint deBruijnIndex,Type boogieType) {

+      return new Z3StubTermAst();

+    }

+    public void DeclareFunction(string functionName, List<Type> domain, Type range) {}

+    public Z3TermAst GetConstant(string constantName, Type constantType) {

+      return new Z3StubTermAst();

+    }    

+    public Z3TermAst MakeIntLiteral(string numeral) {

+      return new Z3StubTermAst();

+    }

+    public Z3TermAst MakeTrue() {

+      return new Z3StubTermAst();

+    }

+    public Z3TermAst MakeFalse() {

+      return new Z3StubTermAst();

+    }

+    public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) {

+      return new Z3StubTermAst();

+    }

+    public Z3LabeledLiterals GetRelevantLabels() {

+      return new Z3StubLabeledLiterals();

+    }

+    public Z3TermAst Make(string op, List<Z3TermAst> children) {

+      return new Z3StubTermAst();

+    }

+  }

+}
\ No newline at end of file