added ability to parse SMT files from the c_interface

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

diff --git a/Makefile b/Makefile
index c0d5cd146a9fc99099837ed3d7b8dce99ff89426..ebb724ca46e972b9f090033ed9693c2f832555dd 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -44,6 +44,8 @@ endif
                           $(SRC)/parser/let-funcs.o  \
                           $(SRC)/parser/parseCVC.o  \
                           $(SRC)/parser/lexCVC.o \
+                          $(SRC)/parser/parseSMT.o \
+                          $(SRC)/parser/lexSMT.o \
                           $(SRC)/main/*.o
        $(RANLIB) libstp.a
        @mkdir -p lib
@@ -52,7 +54,6 @@ endif
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
 
-#
 # During the build of AST some classes are built that most of the other
 # classes depend upon. So in a parallel make, AST should be made first.
 

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index c0d5cd146a9fc99099837ed3d7b8dce99ff89426..ebb724ca46e972b9f090033ed9693c2f832555dd 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -44,6 +44,8 @@ endif
                           $(SRC)/parser/let-funcs.o  \
                           $(SRC)/parser/parseCVC.o  \
                           $(SRC)/parser/lexCVC.o \
+                          $(SRC)/parser/parseSMT.o \
+                          $(SRC)/parser/lexSMT.o \
                           $(SRC)/main/*.o
        $(RANLIB) libstp.a
        @mkdir -p lib
@@ -52,7 +54,6 @@ endif
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
 
-#
 # During the build of AST some classes are built that most of the other
 # classes depend upon. So in a parallel make, AST should be made first.
 

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 24075fcfd71527b75e17542bff578847b63ea350..49be558ab2cc64d33a5f823869f0180e8ec290ee 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -28,9 +28,9 @@ BEEV::ASTVec *decls = NULL;
 //vector<BEEV::ASTNode *> created_exprs;
 bool cinterface_exprdelete_on_flag = false;
 
-/* GLOBAL FUNCTION: parser
- */
+// GLOBAL FUNCTION: parser
 extern int cvcparse(void*);
+extern int smtparse(void*);
 
 void vc_setFlags(VC vc, char c) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
@@ -958,8 +958,8 @@ Expr vc_bvConstExprFromInt(VC vc,
   unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits;
   //printf("%ull", max_n_bits);
   if(v > max_n_bits) {
-    printf("CInterface: vc_bvConstExprFromInt: "                        \
-           "Cannot construct a constant %llu >= %d,\n", v, max_n_bits);
+    printf("CInterface: vc_bvConstExprFromInt: "\
+           "Cannot construct a constant %llu >= %llu,\n", v, max_n_bits);
     BEEV::FatalError("FatalError");
   }
   node n = b->CreateBVConst(n_bits, v);
@@ -1709,7 +1709,7 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) {
 
 Expr vc_parseExpr(VC vc, const char* infile) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
-  extern FILE* cvcin;
+  extern FILE *cvcin, *smtin;
   const char * prog = "stp";
 
   cvcin = fopen(infile,"r");
@@ -1726,7 +1726,17 @@ Expr vc_parseExpr(VC vc, const char* infile) {
   }
 
   BEEV::ASTVec * AssertsQuery = new BEEV::ASTVec;
-  cvcparse((void*)AssertsQuery);
+  if (b->UserFlags.smtlib_parser_flag) 
+    {
+      smtin = cvcin;
+      cvcin = NULL;
+      smtparse((void*)AssertsQuery);
+    } 
+  else
+    {
+      cvcparse((void*)AssertsQuery);
+    }
+
   BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
   BEEV::ASTNode query   = (*(BEEV::ASTVec*)AssertsQuery)[1];
   //BEEV::GlobalSTP->TopLevelSTP(asserts, query);

diff --git a/src/sat/cryptominisat/clause.h b/src/sat/cryptominisat/clause.h
index c7abb7baab4d3c42e16ea9e19a236c7965d455a3..3674b145f1a2d541138493c8c96fbdeca90e0076 100644 (file)
--- a/src/sat/cryptominisat/clause.h
+++ b/src/sat/cryptominisat/clause.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdint.h>
 #include <cstdio>
 #include <vector>
-#include <sys/types.h>
+//#include <sys/types.h>
 #include "mtl/Vec.h"
 #include "SolverTypes.h"
 

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 68a5ddb90f67e96cbe4badaac3284d59c992e9f1..39453ec506b38d41f7f853d7e6b1effd0035e492 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -43,7 +43,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
        ./a10.out
 11:
        g++  $(CXXFLAGS)  squares-leak.c -lstp -o a11.out
-       ulimit -v 30000 && ./a11.out
+       #ulimit -v 30000 && ./a11.out
 12:
        g++  $(CXXFLAGS)  stp-counterex.c -lstp -o a12.out
        ./a12.out
@@ -72,7 +72,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
 
 20:
        g++  -g $(CXXFLAGS)  leak.c  -lstp -o a20.out
-       ulimit -v 13000 && ./a20.out
+       #ulimit -v 13000 && ./a20.out
 
 
 clean: