From 9bfdd671dcd56f492cab90dd0ad393b96c0bcdb5 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 18 Dec 2008 00:21:59 +0000
Subject: [PATCH] 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
---
 Makefile.in                 |  2 +-
 README                      |  2 +-
 c_interface/c_interface.cpp | 32 ++++++++++++++++++++++++++++++++
 c_interface/c_interface.h   |  6 ++++--
 4 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index 1438bce..e672375 100644
--- 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 7150340..7aa371d 100644
--- 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 96f4e9e..631179c 100644
--- 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 d599b06..b6a1e78 100644
--- 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);
-- 
2.47.3