Remove support for Precosat

Precosat has last been released in 2010.

Author: tautschnig

src/common

@@ -159,18 +159,14 @@ else
 endif
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
 ifneq ($(IPASIR),)
   CP_CXXFLAGS += -DHAVE_IPASIR
 endif
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DHAVE_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DHAVE_PICOSAT
 endif

src/config.inc

@@ -16,7 +16,6 @@ endif
 #LIB_GLPK = -lglpk
 
 # SAT-solvers we have
-#PRECOSAT = ../../precosat-576-7e5e66f-120112
 #PICOSAT = ../../picosat-959
 #LINGELING = ../../lingeling-587f-4882048-110513
 #CHAFF = ../../zChaff
@@ -30,10 +29,6 @@ endif
 # when linking against an IPASIR solver.
 LIBSOLVER =
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DSATCHECK_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DSATCHECK_PICOSAT
 endif

src/solvers/CMakeLists.txt

@@ -26,9 +26,6 @@ set(cudd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_bdd_core.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_skizzo_core.cpp
 )
-set(precosat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_precosat.cpp
-)
 set(picosat_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_picosat.cpp
 )
@@ -50,7 +47,6 @@ list(REMOVE_ITEM sources
     ${glucose_source}
     ${squolem2_source}
     ${cudd_source}
-    ${precosat_source}
     ${picosat_source}
     ${lingeling_source}
     ${booleforce_source}

src/solvers/Makefile

@@ -50,13 +50,6 @@ ifneq ($(CUDD),)
            -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
 endif
 
-ifneq ($(PRECOSAT),)
-  PRECOSAT_SRC=sat/satcheck_precosat.cpp
-  PRECOSAT_INCLUDE=-I $(PRECOSAT)
-  PRECOSAT_LIB=$(PRECOSAT)/precosat$(OBJEXT)
-  CP_CXXFLAGS += -DHAVE_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   PICOSAT_SRC=sat/satcheck_picosat.cpp
   PICOSAT_INCLUDE=-I $(PICOSAT)
@@ -80,7 +73,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
-      $(PRECOSAT_SRC) \
       $(SQUOLEM2_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
@@ -199,7 +191,7 @@ INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
   $(IPASIR_INCLUDE) \
   $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
-	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
+	$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 
 CLEANFILES = solvers$(LIBEXT) \
   smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT)
@@ -216,7 +208,7 @@ endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
         $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
-	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
+        $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
 
 ###############################################################################
 

src/solvers/sat/satcheck.h

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 // #define SATCHECK_MINISAT2
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
-// #define SATCHECK_PRECOSAT
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
 
@@ -47,10 +46,6 @@ Author: Daniel Kroening, [email protected]
 #define SATCHECK_BOOLEFORCE
 #endif
 
-#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT)
-#define SATCHECK_PRECOSAT
-#endif
-
 #if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
 #define SATCHECK_PICOSAT
 #endif
@@ -94,13 +89,6 @@ typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
 typedef satcheck_ipasirt satcheckt;
 typedef satcheck_ipasirt satcheck_no_simplifiert;
 
-#elif defined SATCHECK_PRECOSAT
-
-#include "satcheck_precosat.h"
-
-typedef satcheck_precosatt satcheckt;
-typedef satcheck_precosatt satcheck_no_simplifiert;
-
 #elif defined SATCHECK_PICOSAT
 
 #include "satcheck_picosat.h"