Add configuration options for selecting SAT solver, plus some related

cleanups to how scripts and Makefiles include and invoke each other.
Patch from Peter Collingbourne.

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

diff --git a/clean-install.sh b/clean-install.sh
index 86685dcd03bd80b7a8e3e0bc70ba80adf44daf9d..ad2dcb120414943d9c41d6fef998947d95a1f0ff 100755 (executable)
--- a/clean-install.sh
+++ b/clean-install.sh
@@ -1,23 +1,8 @@
 #!/bin/sh
 PREFIX=$HOME
 
-while [ $# -gt 0 ]; do
-    case "$1" in
-       --with-prefix=*)
-           arg=`expr "x$1" : 'x[^=]*=\(.*\)'`
-           PREFIX=$arg;;
-       *)
-           echo "Usage: ./clean-install [options]"
-           echo "   --with-prefix=/prefix/path   Installs STP at the specified path"
-           echo "configure failed"
-           exit 1;;
-    esac
-
-    shift
-done
-
 make configclean
-./scripts/configure --with-prefix=$PREFIX
+. scripts/configure
 make clean
 make install
 

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index e0b59f0b9ca649048b66ff2795e967cf9140bd34..62282e57cb6da0787dfe44932238e0c7435bf696 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -8,6 +8,8 @@
 # * LICENSE: Please view LICENSE file in the home dir of this Program
 # ********************************************************************/
 
+-include $(TOP)/scripts/config.info
+
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 #OPTIMIZE      = -g                # Debugging
 #OPTIMIZE      = -O3 -fPIC         # Maximum optimization
@@ -18,28 +20,36 @@ OPTIMIZE      = -O3               # Maximum optimization
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
-# CRYPTOMINISAT2 = true
-# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
-# MTL            = ../sat/cryptominisat2/mtl
-# SOLVER_INCLUDE = ../sat/cryptominisat2
+ifeq ($(SAT),cryptominisat2)
+  CRYPTOMINISAT2 = true
+  CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
+  MTL            = $(TOP)/src/sat/cryptominisat2/mtl
+  SOLVER_INCLUDE = $(TOP)/src/sat/cryptominisat2
+endif
 
 # OPTION to compile MiniSAT
-CORE          = true
-CFLAGS_BASE   = $(OPTIMIZE) -DCORE
-MTL            = ../sat/mtl
-SOLVER_INCLUDE = ../sat/core
+ifeq ($(SAT),minisat)
+  CORE           = true
+  CFLAGS_BASE    = $(OPTIMIZE) -DCORE
+  MTL            = $(TOP)/src/sat/mtl
+  SOLVER_INCLUDE = $(TOP)/src/sat/core
+endif
 
 # OPTION to compile UNSOUND MiniSAT
-#UNSOUND       = true
-#CFLAGS_BASE   = $(OPTIMIZE) -DUNSOUND
-#MTL            = ../sat/mtl
-#SOLVER_INCLUDE = ../sat/unsound
+ifeq ($(SAT),unsound)
+  UNSOUND        = true
+  CFLAGS_BASE    = $(OPTIMIZE) -DUNSOUND
+  MTL            = $(TOP)/src/sat/mtl
+  SOLVER_INCLUDE = $(TOP)/src/sat/unsound
+endif
 
 # OPTION to compile Simplifying MiniSAT
-# SIMP          = true
-# CFLAGS_BASE   = $(OPTIMIZE) -DSIMP
-# MTL            = ../sat/mtl
-# SOLVER_INCLUDE = ../sat/simp
+ifeq ($(SAT),simp)
+  SIMP           = true
+  CFLAGS_BASE    = $(OPTIMIZE) -DSIMP
+  MTL            = $(TOP)/src/sat/mtl
+  SOLVER_INCLUDE = $(TOP)/src/sat/simp
+endif
 
 SHELL=/bin/bash
 

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 840087250f36eb74a100963ee4fde2e2753f5616..c12ea947ed3452e33cbebfcbbca37a231293629a 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -7,8 +7,8 @@
  # scripts/Makefile.in. The version at the top level stp directory
  # is automatically copied from there.
 
-include  scripts/Makefile.common
--include scripts/config.info
+TOP=.
+include  $(TOP)/scripts/Makefile.common
 
 BIN_DIR=$(PREFIX)/bin
 LIB_DIR=$(PREFIX)/lib

diff --git a/scripts/configure b/scripts/configure
index 13075a61b5d8fc2c99c9d2854a98664a5f8518ab..279b8d099c9bd3f5fe4dbb740ddd7dd1ba2a5981 100755 (executable)
--- a/scripts/configure
+++ b/scripts/configure
@@ -8,9 +8,7 @@
 # LICENSE: Please view LICENSE file in the home dir of this Program
 #********************************************************************
 
-# check for an option --with-prefix=/path/to/prefix and use that as the 
-# prefix, otherwise use /usr/local
-PREFIX=/usr/local
+SAT=minisat
 
 while [ $# -gt 0 ]; do
     case "$1" in
@@ -21,16 +19,32 @@ while [ $# -gt 0 ]; do
            arg=`expr "x$1" : 'x[^=]*=\(.*\)'`    
            CXX=$arg
            echo "Using g++ instead of gcc";;
+       --with-minisat-core)
+           SAT=minisat;;
+       --with-minisat-unsound)
+           SAT=unsound;;
+       --with-minisat-simp)
+           SAT=simp;;
+       --with-cryptominisat2)
+           SAT=cryptominisat2;;
        *)
-           echo "Usage: configure [options]"
+           echo "Usage: $0 [options]"
            echo "   --with-prefix=/prefix/path   Install STP at the specified path"
-           echo "configure failed"
+           echo "   --with-g++=/path/to/g++      Use g++ at the specified path"
+           echo "   --with-minisat-core          Use core MiniSAT solver (default)"
+           echo "   --with-minisat-unsound       Use unsound MiniSAT solver"
+           echo "   --with-minisat-simp          Use simplifying MiniSAT solver"
+           echo "   --with-cryptominisat2        Use CRYPTOMiniSAT 2.x solver"
+           echo "$0 failed"
            exit 1;;
     esac
 
     shift
 done
 
+# check for an option --with-prefix=/path/to/prefix and use that as the 
+# prefix, otherwise use /usr/local
+PREFIX=${PREFIX:-/usr/local}
 
 echo "PREFIX=$PREFIX" > scripts/config.info
 echo "Setting prefix to... $PREFIX"
@@ -39,6 +53,8 @@ then echo "CXX=$CXX" >> scripts/config.info
 export CXX="$CXX"
 echo "Setting CXX to... $CXX"
 fi
+echo "SAT=$SAT" >> scripts/config.info
+echo "Using SAT solver: $SAT"
 
 if [ ! -d $PREFIX/include ]
 then mkdir -p $PREFIX/include

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 46e8cad2c37b072a6444720bd3d8c25a3ef486c0..29d485fbf0ed0738c4db467a58cac64a70ee4591 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS=$(wildcard  *.cpp)
 SRCS+=$(wildcard  NodeFactory/*.cpp)

diff --git a/src/STPManager/Makefile b/src/STPManager/Makefile
index fd1d690d09193e020e20c339b5e5dfbcf46abe21..d60996a03949995c3590992488b6f0f743b69872 100644 (file)
--- a/src/STPManager/Makefile
+++ b/src/STPManager/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/absrefine_counterexample/Makefile b/src/absrefine_counterexample/Makefile
index 6c417b4903186b7e97a49c9871f3aebb22bc5533..bce9db9a3385af5ccd6fdf94ae2dd8b589f9caf3 100644 (file)
--- a/src/absrefine_counterexample/Makefile
+++ b/src/absrefine_counterexample/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile
index 305c765dba680d123e2aea84f943e8fcbf2088c3..649b365da8aa3fb9741e995b6948805d649ea58d 100644 (file)
--- a/src/c_interface/Makefile
+++ b/src/c_interface/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/extlib-abc/Makefile b/src/extlib-abc/Makefile
index 254c0e746fab9beebaafdc14818e2db07f3dd77e..ca58bdad2908cdc8184ae21eed9a4dfb24e54b46 100644 (file)
--- a/src/extlib-abc/Makefile
+++ b/src/extlib-abc/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard aig/*/*.c)
 #SRCS += $(wildcard aig/cnf/*.c)

diff --git a/src/extlib-abc/aig/cnf/Makefile b/src/extlib-abc/aig/cnf/Makefile
index 6a3e0edbdf115648a543628daf81eab3fda58506..f1b0a682adafd3fd2a8584175ceb70c31ecc9f23 100644 (file)
--- a/src/extlib-abc/aig/cnf/Makefile
+++ b/src/extlib-abc/aig/cnf/Makefile
@@ -1,4 +1,5 @@
-include ../../../../scripts/Makefile.common
+TOP = ../../../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.c)
 OBJS = $(SRCS:.c=.o)

diff --git a/src/extlib-constbv/Makefile b/src/extlib-constbv/Makefile
index e56c8f445f52c8ab5e569671228b0b80335a6a88..4c764447167d640578b0a506c0e3d85a7244085d 100644 (file)
--- a/src/extlib-constbv/Makefile
+++ b/src/extlib-constbv/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/main/Makefile b/src/main/Makefile
index e6ccafe6b68e759d1af9c05a25279fddf4d706f6..ca818f1794086fcce3a5dee74e4552484cabdc22 100644 (file)
--- a/src/main/Makefile
+++ b/src/main/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS=main.cpp versionString.cpp Globals.cpp
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/parser/Makefile b/src/parser/Makefile
index c55ee8cbbdd2072b19a9ec922da312bf5c6cd5b9..2e17c61db3826d4883f4fe09fa617d6626d363e7 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 LEX=flex
 YACC=bison -d -y --debug -v

diff --git a/src/printer/Makefile b/src/printer/Makefile
index c3e0baaab8cca939414461857577b9b0decacd20..1f54b47f3cb0afebd0bd8983d20f5098a16b4cf7 100644 (file)
--- a/src/printer/Makefile
+++ b/src/printer/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS=$(wildcard  *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index a1aa922fadad8844c2bd0048ea5c3e5dd8ad1fe5..ce26507315e285bb0e9ef0582c37f6e3ab871900 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -1,4 +1,5 @@
-include   ../../../scripts/Makefile.common
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
 
 MTL       = ../mtl
 SOURCES   = Solver.C

diff --git a/src/sat/cryptominisat/Makefile b/src/sat/cryptominisat/Makefile
index f9c5f4eb5a2a626b7e9b68a79ddc4d64c9dcfb38..416a7a4a2f0407478c6dcb4817d771b9631e5f88 100644 (file)
--- a/src/sat/cryptominisat/Makefile
+++ b/src/sat/cryptominisat/Makefile
@@ -1,4 +1,5 @@
-include   ../../../scripts/Makefile.common
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
 
 MTL       = mtl
 MTRAND    = MTRand

diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile
index e9865097d38c00fda6788f76fa81350745f9fe31..954e0e74f3c6cd893e13202fa5fa25a57b7a80a6 100644 (file)
--- a/src/sat/cryptominisat2/Makefile
+++ b/src/sat/cryptominisat2/Makefile
@@ -1,4 +1,5 @@
-include   ../../../scripts/Makefile.common
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
 
 MTL       = mtl
 MTRAND    = MTRand

diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile
index 6a2466c867cb4911e026e2fd855780b5e5760041..7158c19eda653f5b9d992087e76e9f436dbb9791 100644 (file)
--- a/src/sat/simp/Makefile
+++ b/src/sat/simp/Makefile
@@ -1,4 +1,5 @@
-include   ../../../scripts/Makefile.common
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
 
 MTL       = ../mtl
 SOURCES   = SimpSolver.C ../core/Solver.C

diff --git a/src/sat/unsound/Makefile b/src/sat/unsound/Makefile
index b8439de5de1aee18211848995d9a43ce23976838..f1d5ecdf33ebc618b705228d07f85b99f746f2b9 100644 (file)
--- a/src/sat/unsound/Makefile
+++ b/src/sat/unsound/Makefile
@@ -1,4 +1,5 @@
-include   ../../../scripts/Makefile.common
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
 
 MTL       = ../mtl
 SOURCES   = UnsoundSimpSolver.C ../core/Solver.C

diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile
index 1d9d506edf4240efe960e85e2aec374b56d04b69..cde0dda2bf6a5cadb5934b004fe9e6d89a60bd81 100644 (file)
--- a/src/simplifier/Makefile
+++ b/src/simplifier/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
index 7d422c44693791b6121823d319c0344f71a292cf..836869df9df3165b3be5b78d1f30c342fe9069dd 100644 (file)
--- a/src/to-sat/Makefile
+++ b/src/to-sat/Makefile
@@ -1,4 +1,5 @@
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 3a3978424ae3ffc89dfb3b4d911ffcd45d41167f..bc17d803c2c8f6ad103907d140f1ce6d70e4ecf1 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -1,6 +1,7 @@
 # Tests that run under valgrind will return a non-zero error code on
 # either leak, or use of unitialised values.
-include ../../scripts/Makefile.common
+TOP = ../..
+include $(TOP)/scripts/Makefile.common
 CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib 
 LIBS= -lstp