Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 29 insertions, 0 deletions

diff --git a/stp/AST/asttest.cpp b/stp/AST/asttest.cpp
new file mode 100644
index 00000000..57f3d20c
--- /dev/null
+++ b/stp/AST/asttest.cpp
@@ -0,0 +1,29 @@
+#include "AST.h"
+
+using namespace BEEV;
+
+int main()
+{
+
+  BeevMgr * bm = new BeevMgr();
+  ASTNode s1 = bm->CreateSymbol("foo");
+  s1 = bm->CreateSymbol("foo1");
+  s1 = bm->CreateSymbol("foo2");
+  ASTNode s2 = bm->CreateSymbol("bar");
+  cout << "s1" <<  s1 << endl;
+  cout << "s2" <<  s2 << endl;
+
+  ASTNode b1 = bm->CreateBVConst(5,12);
+  ASTNode b2 = bm->CreateBVConst(6,36);
+  cout << "b1: " <<  b1 << endl;
+  cout << "b2: " <<  b2 << endl;
+
+  ASTNode a1 = bm->CreateNode(EQ, s1, s2);
+  ASTNode a2 = bm->CreateNode(AND, s1, s2);
+  a1 = bm->CreateNode(OR, s1, s2);
+  ASTNode a3 = bm->CreateNode(IMPLIES, a1, a2);
+  ASTNode a4 = bm->CreateNode(IMPLIES, s1, a2);
+  cout << "a3" <<  a3 << endl;
+  cout << "a4" <<  a4 << endl;
+  return 0;
+}