Applying a patch provided by Hume to parse cvc and smtlib format constraints from...

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 78f7d9d8ad4d7a4c4f7d33aca01ff34dd4e20a02..ed189870c480934c8d6bc9ab2df9a45fd407f55d 100644 (file)
--- 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\r
+struct yy_buffer_state;\r
+#define YY_TYPEDEF_YY_BUFFER_STATE\r
+typedef struct yy_buffer_state *YY_BUFFER_STATE;\r
+
+
+extern YY_BUFFER_STATE cvc_scan_string (const char *yy_str  );\r
+extern void cvc_delete_buffer (YY_BUFFER_STATE  b );
+extern YY_BUFFER_STATE smt_scan_string (const char *yy_str  );\r
+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 8e280e5da4d4c6aeccfd429d9ccc6eee41a3493b..6cbdf90c16742184db9249760207fe61c0056a10 100644 (file)
--- 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 bc17d803c2c8f6ad103907d140f1ce6d70e4ecf1..e885164f125fe982918d220d6c3c4514ff5fe667 100644 (file)
--- 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