From e6536c2deedee1ec77a34126245f04404397c124 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 29 Apr 2010 13:27:44 +0000
Subject: [PATCH] Applying a patch provided by Hume to parse cvc and smtlib
 format constraints from c-strings.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@738 e59a4935-1847-0410-ae03-e826735625c1
---
 src/c_interface/c_interface.cpp | 64 +++++++++++++++++++++++++++++++++
 src/c_interface/c_interface.h   |  2 ++
 tests/c-api-tests/Makefile      |  5 ++-
 3 files changed, 70 insertions(+), 1 deletion(-)

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 78f7d9d..ed18987 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1960,3 +1960,67 @@ int getExprID (Expr ex) {
   BEEV::ASTNode q = (*(nodestar)ex);  
   return q.GetNodeNum();
 }
+
+//////////////////////////////////////////////////////////////////////////
+// extended version
+
+
+#if 0
+/#ifndef YY_TYPEDEF_YY_BUFFER_STATE
+struct yy_buffer_state;
+#define YY_TYPEDEF_YY_BUFFER_STATE
+typedef struct yy_buffer_state *YY_BUFFER_STATE;
+
+
+extern YY_BUFFER_STATE cvc_scan_string (const char *yy_str  );
+extern void cvc_delete_buffer (YY_BUFFER_STATE  b );
+extern YY_BUFFER_STATE smt_scan_string (const char *yy_str  );
+extern void smt_delete_buffer (YY_BUFFER_STATE  b );
+extern void cvc_switch_to_buffer (YY_BUFFER_STATE new_buffer  );
+extern void smt_switch_to_buffer (YY_BUFFER_STATE new_buffer  );
+#endif
+
+int smt_scan_string(const char *yy_str);
+
+int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ) {
+  bmstar b = (bmstar)(((stpstar)vc)->bm);
+
+#if 0
+ BEEV::GlobalSTP = (stpstar)vc;
+  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
+  if(0 != c) {
+    cout << CONSTANTBV::BitVector_Error(c) << endl;
+    return 0;
+  }
+#endif
+  
+  BEEV::ParserInterface pi(*b, b->defaultNodeFactory);
+  BEEV::parserInterface = &pi;
+
+  BEEV::ASTVec AssertsQuery;
+  if (b->UserFlags.smtlib_parser_flag) 
+    {
+      //YY_BUFFER_STATE bstat = smt_scan_string(s);
+      //smt_switch_to_buffer(bstat);
+      smt_scan_string(s);
+      smtparse((void*)&AssertsQuery);
+      //smt_delete_buffer(bstat);
+    } 
+  else
+    {
+      //YY_BUFFER_STATE bstat = cvc_scan_string(s);
+      //cvc_switch_to_buffer(bstat);
+      smt_scan_string(s);
+      cvcparse((void*)&AssertsQuery);
+      //cvc_delete_buffer(bstat);
+    }
+
+  if ( oquery ) {
+    *(nodestar*) oquery = new node(AssertsQuery[1]);
+  }
+  if ( oasserts ) {
+    *(nodestar*) oasserts = new node(AssertsQuery[0]);
+  }
+  return 1;
+} //end of vc_parseMemExpr()
+
diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 8e280e5..6cbdf90 100644
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -429,6 +429,8 @@ extern "C" {
   // get the node ID of an Expr.
   int getExprID (Expr ex);
 
+  // parse the expr from memory string!
+  int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts );
 #ifdef __cplusplus
 }
 #endif
diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index bc17d80..e885164 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -13,7 +13,7 @@ else
 endif
 
 
-all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21
+all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22
 	rm -rf *.out
 
 0:	
@@ -86,6 +86,9 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21
 21:	
 	g++ $(CXXFLAGS) interface-check.c -o a21.out $(LIBS)
 	./a21.out
+22:
+	g++ $(CXXFLAGS) parsestring-using-cinterface.c -o a22.out $(LIBS)
+	$(VALGRIND) ./a22.out
 
 clean:
 	rm -rf *~ *.out
-- 
2.47.3