Remove support for SMVSAT

Publications on SMVSAT appeared in 2004 and it's not clear where it
might be available for download. The code base has not fully supported
it anymore either.

Author: tautschnig

src/config.inc

@@ -25,7 +25,6 @@ endif
 #MINISAT2 = ../../minisat-2.2.1
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
-#SMVSAT =
 
 # Extra library for SAT solver. This should link to the archive file to be used
 # when linking against an IPASIR solver.
@@ -63,10 +62,6 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif
 
-ifneq ($(SMVSAT),)
-  CP_CXXFLAGS += -DSATCHECK_SMVSAT
-endif
-
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"

src/solvers/CMakeLists.txt

@@ -18,9 +18,6 @@ set(minisat2_source
 set(glucose_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_glucose.cpp
 )
-set(smvsat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_smvsat.cpp
-)
 set(squolem2_source
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem_core.cpp
@@ -51,7 +48,6 @@ list(REMOVE_ITEM sources
     ${minisat_source}
     ${minisat2_source}
     ${glucose_source}
-    ${smvsat_source}
     ${squolem2_source}
     ${cudd_source}
     ${precosat_source}

src/solvers/Makefile

@@ -36,12 +36,6 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
 endif
 
-ifneq ($(SMVSAT),)
-  SMVSAT_SRC=sat/satcheck_smvsat.cpp
-  SMVSAT_INCLUDE=-I $(SMVSAT)/include
-  SMVSAT_LIB=$(SMVSAT)/lib/libsmvsat$(LIBEXT)
-endif
-
 ifneq ($(SQUOLEM2),)
   SQUOLEM2_SRC=qbf/qbf_squolem.cpp qbf/qbf_squolem_core.cpp
   SQUOLEM2_INCLUDE=-I $(SQUOLEM2)
@@ -87,7 +81,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
       $(PRECOSAT_SRC) \
-      $(SMVSAT_SRC) \
       $(SQUOLEM2_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
@@ -205,7 +198,7 @@ SRC = $(BOOLEFORCE_SRC) \
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
   $(IPASIR_INCLUDE) \
-  $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
+  $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 
 CLEANFILES = solvers$(LIBEXT) \
@@ -222,7 +215,7 @@ endif
 endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
-        $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
+        $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
 	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
 
 ###############################################################################