From: trevor_hansen Date: Wed, 11 May 2011 01:53:42 +0000 (+0000) Subject: Remove the comment that 32-bit is best for arrays. No longer the case because we... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4ef67bbd0f911fe03da075c4a87934dd78d81d36;p=francis%2Fstp.git Remove the comment that 32-bit is best for arrays. No longer the case because we use ABC's AIG CNF conversion by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1320 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index f5b0930..5973ce2 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -1,7 +1,7 @@ # This is a -*- makefile -*-, Emacs # #/******************************************************************** -# * AUTHORS: Vijay Ganesh +# * AUTHORS: Vijay Ganesh, Trevor Hansen # * # * BEGIN DATE: November, 2005 # * @@ -17,18 +17,10 @@ #OPTIMIZE = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE OPTIMIZE = -O3 -g # Maximum optimization - -#When solving array problems STP creates lots of objects during the conversion to CNF. If STP is compiled -#as a 32-bit executable, then these objects are about half the size than they are if STP is compiled as a 64-bit -#program. That's because lots of the data in the objects are pointers to other objects. So, if you meet the -#following criteria you may want to enable -m32 on your 64-bit machine: -#1) You are solving array problems. Problems without arrays use another CNF conversion scheme. -#2) You need STP to use about half the memory. #CFLAGS_M32 = -m32 CFLAGS_BASE = $(OPTIMIZE) - ifeq ($(WITHCBITP),yes) CFLAGS_BASE += -DWITHCBITP endif diff --git a/scripts/run_tests.pl b/scripts/run_tests.pl index 91981ee..25368d8 100755 --- a/scripts/run_tests.pl +++ b/scripts/run_tests.pl @@ -74,7 +74,7 @@ my %optionsDefault = ("level" => 4, "proofs" => 0, "lang" => "all", "stppath" => "stp/bin", - "vc" => $pwd . "/bin/stp -t -d", # Program names + "vc" => $pwd . "/bin/stp -r -t -d", # Program names #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names "pfc" => "true", "stptestpath" => "stp/test", @@ -85,7 +85,7 @@ my %optionsDefault = ("level" => 4, # Runtime limit; 0 = no limit "time" => 180, # Additional command line options to stp - "stpOptions" => "-d"); + "stpOptions" => "-r -d"); # Database of command line options. Initially, they are undefined