From a6a4e7d318cb43683369d2dd4882318ddabfe0f2 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 6 Sep 2009 20:52:21 +0000
Subject: [PATCH] minor changes to c_interface

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@192 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/Makefile                      |  2 +-
 src/AST/{ => TestAST}/asttest.cpp     |  0
 src/AST/{test => TestAST}/bbtest.cpp  |  0
 src/AST/{test => TestAST}/cnftest.cpp |  0
 src/c_interface/c_interface.cpp       | 55 +++++++++++++++++++++------
 src/main/Globals.h                    |  4 ++
 6 files changed, 48 insertions(+), 13 deletions(-)
 rename src/AST/{ => TestAST}/asttest.cpp (100%)
 rename src/AST/{test => TestAST}/bbtest.cpp (100%)
 rename src/AST/{test => TestAST}/cnftest.cpp (100%)

diff --git a/src/AST/Makefile b/src/AST/Makefile
index d976865..186f0cf 100644
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -6,7 +6,7 @@ OBJS = $(SRCS:.cpp=.o)
 CFLAGS += -I../sat/mtl -I../sat/core
 
 #Make the ast library for use by other modules
-libast.a:	$(OBJS) depend
+libast.a:$(OBJS) depend
 	-rm -rf $@
 	$(AR) rc $@ $(OBJS)
 	$(RANLIB) $@
diff --git a/src/AST/asttest.cpp b/src/AST/TestAST/asttest.cpp
similarity index 100%
rename from src/AST/asttest.cpp
rename to src/AST/TestAST/asttest.cpp
diff --git a/src/AST/test/bbtest.cpp b/src/AST/TestAST/bbtest.cpp
similarity index 100%
rename from src/AST/test/bbtest.cpp
rename to src/AST/TestAST/bbtest.cpp
diff --git a/src/AST/test/cnftest.cpp b/src/AST/TestAST/cnftest.cpp
similarity index 100%
rename from src/AST/test/cnftest.cpp
rename to src/AST/TestAST/cnftest.cpp
diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 44b7f33..2a063f5 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -27,7 +27,7 @@ bool cinterface_exprdelete_on_flag = false;
 
 /* GLOBAL FUNCTION: parser
  */
-extern int cvcparse();
+extern int cvcparse(void*);
 
 void vc_setFlags(char c) {
   std::string helpstring = "Usage: stp [-option] [infile]\n\n";
@@ -1448,6 +1448,40 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) {
 }
 #endif
 
+// Expr vc_parseExpr(VC vc, char* infile) {
+//   bmstar b = (bmstar)vc;
+//   extern FILE* cvcin;
+//   const char * prog = "stp";
+  
+//   cvcin = fopen(infile,"r");
+//   if(cvcin == NULL) {
+//     fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+//     BEEV::FatalError("");
+//   }
+  
+//   BEEV::GlobalBeevMgr = b;
+
+//   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); 
+//   if(0 != c) {
+//     cout << CONSTANTBV::BitVector_Error(c) << endl;
+//     return 0;
+//   }
+
+//   cvcparse();
+//   nodelist aaa = b->GetAsserts();
+
+//   //Don't add the query. It gets added automatically if the input file
+//   //has QUERY in it 
+//   //
+//   //node bbb = b->CreateNode(BEEV::NOT,b->GetQuery());
+//   node o =  b->CreateNode(BEEV::AND,aaa);
+//   //node o = b->CreateNode(BEEV::AND,oo,bbb);
+
+//   nodestar output = new node(o);
+//   return output;
+// } //end of vc_parseExpr()
+
+
 Expr vc_parseExpr(VC vc, char* infile) {
   bmstar b = (bmstar)vc;
   extern FILE* cvcin;
@@ -1460,23 +1494,20 @@ Expr vc_parseExpr(VC vc, char* infile) {
   }
   
   BEEV::GlobalBeevMgr = b;
-
   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); 
   if(0 != c) {
     cout << CONSTANTBV::BitVector_Error(c) << endl;
     return 0;
   }
 
-  cvcparse();
-  nodelist aaa = b->GetAsserts();
-
-  //Don't add the query. It gets added automatically if the input file
-  //has QUERY in it 
-  //
-  //node bbb = b->CreateNode(BEEV::NOT,b->GetQuery());
-  node o =  b->CreateNode(BEEV::AND,aaa);
-  //node o = b->CreateNode(BEEV::AND,oo,bbb);
-
+  BEEV::ASTVec * AssertsQuery = new BEEV::ASTVec;
+  cvcparse((void*)AssertsQuery);
+  BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
+  BEEV::ASTNode query   = (*(BEEV::ASTVec*)AssertsQuery)[1];
+  //b->TopLevelSAT(asserts, query);
+  
+  node oo = b->CreateNode(BEEV::NOT,query);
+  node o = b->CreateNode(BEEV::AND,asserts,oo);
   nodestar output = new node(o);
   return output;
 } //end of vc_parseExpr()
diff --git a/src/main/Globals.h b/src/main/Globals.h
index 212feed..abd66df 100644
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -18,6 +18,7 @@
 #include <signal.h>
 #include <stdio.h>
 #include <unistd.h>
+#include <vector>
 
 namespace MINISAT
 {
@@ -103,6 +104,9 @@ namespace BEEV
   //Useful global variables. There are very few them
   extern BeevMgr * GlobalBeevMgr;
 
+  //Empty vector
+  extern std::vector<BEEV::ASTNode> _empty_ASTVec;
+
   //Some global vars for the Main function.
   extern const char * prog;
   extern int linenum;
-- 
2.47.3