added parsing capability in c_interface

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@46 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/Makefile.in b/Makefile.in
index 1438bce893ca0b57e721f6fabb8ef111ea9f33e1..e672375e982a7080f7a2059a9c4a08857b153cfa 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -25,7 +25,7 @@ all:
        $(MAKE) -C c_interface
        $(MAKE) -C constantbv
        $(MAKE) -C parser
-       $(AR) rc libstp.a  AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
+       $(AR) rc libstp.a  AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o parser/let-funcs.o parser/parsePL.o parser/lexPL.o
        $(RANLIB) libstp.a
        @mkdir -p lib
        @mv libstp.a lib/

diff --git a/README b/README
index 7150340b93e93000cbea71c11db1ec85d82dd68a..7aa371dd42880a671a8ce44279b68b2a72f06525 100644 (file)
--- a/README
+++ b/README
@@ -1,7 +1,7 @@
 /********************************************************************
  * PROGRAM NAME: STP (Simple Theorem Prover)   
  *             
- * AUTHORS: Vijay Ganesh, David L. Dill
+ * AUTHORS: Vijay Ganesh
  *     
  * BEGIN DATE: November, 2005
  *

diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp
index 96f4e9e61af40650bfb870b1c1dc372edbc0d9c3..631179c69a856a12ad479443cdfd47789b847547 100644 (file)
--- a/c_interface/c_interface.cpp
+++ b/c_interface/c_interface.cpp
@@ -24,6 +24,10 @@ BEEV::ASTVec *decls = NULL;
 //vector<BEEV::ASTNode *> created_exprs;
 bool cinterface_exprdelete_on = false;
 
+/* GLOBAL FUNCTION: parser
+ */
+extern int yyparse();
+
 void vc_setFlags(char c) {
   std::string helpstring = "Usage: stp [-option] [infile]\n\n";
   helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
@@ -1402,6 +1406,34 @@ 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* yyin;
+  const char * prog = "stp";
+  
+  yyin = fopen(infile,"r");
+  if(yyin == NULL) {
+    fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+    BEEV::FatalError("");
+  }
+  
+  BEEV::globalBeevMgr_for_parser = b;
+
+  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); 
+  if(0 != c) {
+    cout << CONSTANTBV::BitVector_Error(c) << endl;
+    return 0;
+  }
+
+  yyparse();
+  nodelist aaa = b->GetAsserts();
+  node o =  b->CreateNode(BEEV::AND,aaa);
+  
+  nodestar output = new node(o);
+  return output;
+} //end of vc_parseExpr()
+
 char* exprString(Expr e){
   stringstream ss;
   ((nodestar)e)->PL_Print(ss,0);

diff --git a/c_interface/c_interface.h b/c_interface/c_interface.h
index d599b066998731f72bf4ec279c8c472be9c110e1..b6a1e78c3c8818e160f3ff2e049b5c59c5587ee5 100644 (file)
--- a/c_interface/c_interface.h
+++ b/c_interface/c_interface.h
@@ -21,6 +21,8 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+
+#include <stdio.h>
   
 #ifdef STP_STRONG_TYPING
 #else
@@ -109,8 +111,8 @@ extern "C" {
   //! Array update; equivalent to "array WITH [index] := newValue"
   Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue);
   
-  // Expr I/O
-  //! Expr vc_parseExpr(VC vc, char* s);
+  // Expr I/O: Parses directly from file in the c_interface. pretty cool!!
+  Expr vc_parseExpr(VC vc, char* s);
 
   //! Prints 'e' to stdout.
   void vc_printExpr(VC vc, Expr e);