all: propsolve.o

include ../config.inc
ifneq ($(CHAFF),)
CHAFF_SRC=satcheck_zchaff.cpp
CHAFF_INCLUDE=-I ../$(CHAFF)
CHAFF_LIB=../$(CHAFF)/libsat.a
endif

ifneq ($(BOOLEFORCE),)
BOOLEFORCE_SRC=satcheck_booleforce.cpp
BOOLEFORCE_INCLUDE=-I ../$(BOOLEFORCE)
BOOLEFORCE_LIB=../$(BOOLEFORCE)/libbooleforce.a
endif

ifneq ($(MINISAT),)
MINISAT_SRC=satcheck_minisat.cpp satcheck_minisat_interpolation.cpp
MINISAT_INCLUDE=-I ../$(MINISAT)
MINISAT_LIB=../$(MINISAT)/Solver.o ../$(MINISAT)/Proof.o ../$(MINISAT)/File.o
#MINISAT_LIB=../$(MINISAT)/Solver.o 
endif

ifneq ($(SMVSAT),)
SMVSAT_SRC=satcheck_smvsat.cpp
SMVSAT_INCLUDE=-I ../$(SMVSAT)/include
SMVSAT_LIB=../$(SMVSAT)/lib/libsmvsat.a
endif

SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(SMVSAT_SRC) \
      cnf.cpp dimacs_cnf.cpp cnf_clause_list.cpp \
      pbs_dimacs_cnf.cpp qdimacs_cnf.cpp cvc_prop.cpp qbf_quantor.cpp \
      satcheck_zcore.cpp and_graph.cpp and_graph_prop.cpp \
      sat_minimizer.cpp smt_prop.cpp

OBJ = $(SRC:.cpp=.o)

include ../common

INCLUDES= -I .. \
 $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) \
 $(SMVSAT_INCLUDE) -I ../util 

###############################################################################

propsolve.o: $(OBJ)
	$(LD) -r -o propsolve.o $(OBJ) \
	$(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) $(SMVSAT_LIB)

clean:
	rm -f *.o
