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

diff --git a/src/AST/Makefile b/src/AST/Makefile
index d976865c541f7676e7e6d256dbee2b1c02345b93..186f0cf8e607378a1b98e5f01e60d31fc71c5987 100644 (file)
--- 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 44b7f3375e00333ad22fa731e30c0a41e8263244..2a063f524726fbabb648e090f27a2b2deb5066b1 100644 (file)
--- 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 212feedef57b31672d0cffed70f69210433577a4..abd66df07a88e9702aad267a9e91db95f8776b32 100644 (file)
--- 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;