From 0e2b3fea653d867d95dbe8fa328432a144400c07 Mon Sep 17 00:00:00 2001 From: smccam Date: Mon, 12 Apr 2010 19:36:49 +0000 Subject: [PATCH] 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 --- clean-install.sh | 17 +---------- scripts/Makefile.common | 42 +++++++++++++++++---------- scripts/Makefile.in | 4 +-- scripts/configure | 26 +++++++++++++---- src/AST/Makefile | 3 +- src/STPManager/Makefile | 3 +- src/absrefine_counterexample/Makefile | 3 +- src/c_interface/Makefile | 3 +- src/extlib-abc/Makefile | 3 +- src/extlib-abc/aig/cnf/Makefile | 3 +- src/extlib-constbv/Makefile | 3 +- src/main/Makefile | 3 +- src/parser/Makefile | 3 +- src/printer/Makefile | 3 +- src/sat/core/Makefile | 3 +- src/sat/cryptominisat/Makefile | 3 +- src/sat/cryptominisat2/Makefile | 3 +- src/sat/simp/Makefile | 3 +- src/sat/unsound/Makefile | 3 +- src/simplifier/Makefile | 3 +- src/to-sat/Makefile | 3 +- tests/c-api-tests/Makefile | 3 +- 22 files changed, 86 insertions(+), 57 deletions(-) diff --git a/clean-install.sh b/clean-install.sh index 86685dc..ad2dcb1 100755 --- 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 e0b59f0..62282e5 100644 --- 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 8400872..c12ea94 100644 --- 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 13075a6..279b8d0 100755 --- 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 46e8cad..29d485f 100644 --- 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 fd1d690..d60996a 100644 --- 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 6c417b4..bce9db9 100644 --- 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 305c765..649b365 100644 --- 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 254c0e7..ca58bda 100644 --- 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 6a3e0ed..f1b0a68 100644 --- 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 e56c8f4..4c76444 100644 --- 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 e6ccafe..ca818f1 100644 --- 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 c55ee8c..2e17c61 100644 --- 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 c3e0baa..1f54b47 100644 --- 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 a1aa922..ce26507 100644 --- 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 f9c5f4e..416a7a4 100644 --- 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 e986509..954e0e7 100644 --- 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 6a2466c..7158c19 100644 --- 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 b8439de..f1d5ecd 100644 --- 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 1d9d506..cde0dda 100644 --- 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 7d422c4..836869d 100644 --- 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 3a39784..bc17d80 100644 --- 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 -- 2.47.3