From 6f290d8f9e9d7faac295cb51fc96884a18f4ded4 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Thu, 21 May 2009 04:36:41 +0000
Subject: 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
---
 stp/AST/cnftest.cpp | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 stp/AST/cnftest.cpp

(limited to 'stp/AST/cnftest.cpp')

diff --git a/stp/AST/cnftest.cpp b/stp/AST/cnftest.cpp
new file mode 100644
index 00000000..7ce270c8
--- /dev/null
+++ b/stp/AST/cnftest.cpp
@@ -0,0 +1,47 @@
+// -*- c++ -*-
+
+// Test program for CNF conversion.
+
+#include "AST.h"
+
+using namespace BEEV;
+
+int main()
+{
+  const int size = 1;
+  
+  BeevMgr *bm = new BeevMgr();
+  ASTNode s1 = bm->CreateSymbol("x");
+  s1.SetValueWidth(size);
+  
+  cout << "s1" <<  s1 << endl;
+  ASTNode s2 = bm->CreateSymbol("y");
+  s2.SetValueWidth(size);
+
+  cout << "s2" <<  s2 << endl;
+  ASTNode s3 = bm->CreateSymbol("z");
+  s3.SetValueWidth(size);
+  
+  cout << "s3" <<  s3 << endl;
+
+  ASTNode bbs1 = bm->BBForm(s1);
+  cout << "bitblasted s1" << endl << bbs1 << endl;
+  bm->PrintClauseList(cout, bm->ToCNF(bbs1));
+
+  ASTNode a2 = bm->CreateNode(AND, s1, s2);
+  ASTNode bba2 = bm->BBForm(a2);
+  cout << "bitblasted a2" << endl << bba2 << endl;
+  bm->PrintClauseList(cout, bm->ToCNF(bba2));
+
+  ASTNode a3 = bm->CreateNode(OR, s1, s2);
+  ASTNode bba3 = bm->BBForm(a3);
+  cout << "bitblasted a3" << endl << bba3 << endl;
+  bm->PrintClauseList(cout, bm->ToCNF(bba3));
+
+  ASTNode a4 = bm->CreateNode(EQ, s1, s2);
+  ASTNode bba4 = bm->BBForm(a4);
+  cout << "bitblasted a4 " << endl << bba4 << endl;
+
+  bm->PrintClauseList(cout, bm->ToCNF(bba4));
+
+}
-- 
cgit 1.4.1