Fix compiling of the SMT-LIB Parser, Fix regression test script on bash.

The make files for the smtlib parser referred to to old locations of the SAT solver. The regression tests used
lots to many arguments to ulimit, it didn't run in my bash shell.

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

diff --git a/AST/AST.h b/AST/AST.h
index fb6f6491510c71653a9e171a6afea849810c49f9..04f3528912a1e1fece868f4154e39e2d14249f4b 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -103,9 +103,6 @@ namespace BEEV {
     // Usual constructor.  
     ASTNode(ASTInternal *in);
 
-    //Check if it points to a null node
-    bool IsNull () const { return _int_node_ptr == NULL; }
-
     //Equal iff ASTIntNode pointers are the same.
     friend bool operator==(const ASTNode node1, const ASTNode node2){
       return ((size_t) node1._int_node_ptr) == ((size_t) node2._int_node_ptr);
@@ -127,6 +124,9 @@ namespace BEEV {
     }
 
   public:
+    //Check if it points to a null node
+    bool IsNull () const { return _int_node_ptr == NULL; }
+
     // This is for sorting by expression number (used in Boolean
     //optimization).
     // With any ordering operation, the properties of the order

diff --git a/Makefile.smt b/Makefile.smt
index 0b0d18c7b41d5c9fd85c7eb20049d676f0f388e1..3782cf8d9888a8155c3c3e5124965c0f03f32f04 100644 (file)
--- a/Makefile.smt
+++ b/Makefile.smt
@@ -18,17 +18,17 @@ HEADERS=c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C AST
-       $(MAKE) -C sat
+       $(MAKE) -C sat/core lib
        $(MAKE) -C simplifier
        $(MAKE) -C bitvec
        $(MAKE) -C c_interface
        $(MAKE) -C constantbv
        $(MAKE) -C parser -f Makefile.smt
-       $(AR) rc libstp.a  AST/*.o sat/*.o simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
-       ranlib libstp.a
+       $(AR) rc libstp.a  AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
+       $(RANLIB) libstp.a
        @mkdir -p lib
        @mv libstp.a lib/
-       $(MAKE) TAGS
+#      $(MAKE) TAGS
        @echo ""
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
@@ -53,7 +53,7 @@ clean:
        rm -rf config.info
        rm -f TAGS
        $(MAKE) clean -C AST
-       $(MAKE) clean -C sat
+       $(MAKE) clean -C sat/core
        $(MAKE) clean -C simplifier
        $(MAKE) clean -C bitvec
        $(MAKE) clean -C parser

diff --git a/bin/run_tests b/bin/run_tests
index 5571e658c657b1a26524d3a312b7e5d70040db29..0680cf5109a5af41bfd668a09262b00d6a833f2d 100755 (executable)
--- a/bin/run_tests
+++ b/bin/run_tests
@@ -372,7 +372,7 @@ foreach my $testcase (@testcases) {
        # Now, run the sucker
        my $timeMax = getOpt('time');
        my $timeLimit = ($timeMax > 0)? "-t $timeMax" : "";
-       my $limits = "ulimit -c 0 -d 2000000 -m 2000000 -v 2000000 $timeLimit";
+       my $limits = "ulimit -c 0; ulimit -d 2000000; ulimit -m 2000000; ulimit -v 2000000; ulimit $timeLimit";
        #   "-s 10240 -v 2000000 $timeLimit";   
        my $logging = ($verbose)? " 2>&1 | tee output" : "> output 2>&1";
        my $timing = ($verbose)? "time " : "";

diff --git a/bin/run_tests.smt b/bin/run_tests.smt
index f4bb44c8b1816a687a02099660881e65b420264d..eb607231bbf569fb54ee3b0c15ca47dc6518c1c9 100755 (executable)
--- a/bin/run_tests.smt
+++ b/bin/run_tests.smt
@@ -375,7 +375,7 @@ foreach my $testcase (@testcases) {
        # Now, run the sucker
        my $timeMax = getOpt('time');
        my $timeLimit = ($timeMax > 0)? "-t $timeMax" : "";
-       my $limits = "ulimit -c 0 -d 2000000 -m 2000000 -s 2000000 -v 2000000 $timeLimit";
+       my $limits = "ulimit -c 0; ulimit -d 2000000;ulimit -m 2000000; ulimit -s 2000000; ulimit -v 2000000; ulimit -t $timeLimit";
        #    "-s 10240 -v 2000000 $timeLimit";  
        my $logging = ($verbose)? " 2>&1 | tee output" : "> output 2>&1";
        my $timing = ($verbose)? "time " : "";

diff --git a/parser/Makefile.smt b/parser/Makefile.smt
index caeb2e8898b4d7dcbab89611ee551591e101d56c..e55aa7ef8f3e1ff699b89a6c89b50dc09fb44636 100644 (file)
--- a/parser/Makefile.smt
+++ b/parser/Makefile.smt
@@ -5,7 +5,7 @@ YACC=bison -d -y --debug -v
 
 SRCS = lexPL.cpp parsePL.cpp let-funcs.cpp main.cpp
 OBJS = $(SRCS:.cpp=.o)
-LIBS = -L../AST -last -L../sat/core -L../sat/simp -lminisatp -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
+LIBS = -L../AST -last -L../sat/core -L../sat/simp -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
 CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp
 
 all: parsePL.cpp lexPL.cpp let-funcs.cpp parser parsePL.o lexPL.o let-funcs.o