From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 6 Jan 2009 02:31:09 +0000 (+0000)
Subject: Fix compiling of the SMT-LIB Parser, Fix regression test script on bash.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a53510af89ef4a9b9d7951fd641fcc6e03c82322;p=francis%2Fstp.git

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 fb6f649..04f3528 100644
--- 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 0b0d18c..3782cf8 100644
--- 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 5571e65..0680cf5 100755
--- 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 f4bb44c..eb60723 100755
--- 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 caeb2e8..e55aa7e 100644
--- 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