From a53510af89ef4a9b9d7951fd641fcc6e03c82322 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 6 Jan 2009 02:31:09 +0000 Subject: [PATCH] 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 --- AST/AST.h | 6 +++--- Makefile.smt | 10 +++++----- bin/run_tests | 2 +- bin/run_tests.smt | 2 +- parser/Makefile.smt | 2 +- 5 files changed, 11 insertions(+), 11 deletions(-) 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 -- 2.47.3