From 28cca9c2fd3a9acc4febdc2865861ada052e1b08 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 13:01:27 +0100 Subject: [PATCH 1/4] Remove unused DIMACS parser --- src/solvers/Makefile | 1 - src/solvers/sat/read_dimacs_cnf.cpp | 105 ---------------------------- src/solvers/sat/read_dimacs_cnf.h | 19 ----- 3 files changed, 125 deletions(-) delete mode 100644 src/solvers/sat/read_dimacs_cnf.cpp delete mode 100644 src/solvers/sat/read_dimacs_cnf.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 958373871d0..20100504caa 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -199,7 +199,6 @@ SRC = $(BOOLEFORCE_SRC) \ sat/cnf_clause_list.cpp \ sat/dimacs_cnf.cpp \ sat/pbs_dimacs_cnf.cpp \ - sat/read_dimacs_cnf.cpp \ sat/resolution_proof.cpp \ sat/satcheck.cpp \ smt1/smt1_conv.cpp \ diff --git a/src/solvers/sat/read_dimacs_cnf.cpp b/src/solvers/sat/read_dimacs_cnf.cpp deleted file mode 100644 index 4228851fcdf..00000000000 --- a/src/solvers/sat/read_dimacs_cnf.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/*******************************************************************\ - -Module: Reading DIMACS CNF - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Reading DIMACS CNF - -#include "read_dimacs_cnf.h" - -#include -#include // for abs() - -#include - -// #define VERBOSE - -void read_dimacs_cnf(std::istream &in, cnft &dest) -{ - #define DELIMITERS "\t\n\v\f\r " - #define CHAR_DELIMITERS "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" - - bvt new_bv; - std::string line; - - while(getline(in, line)) - { - line += " "; - - while(true) - { - if(line.empty()) - break; - - #ifdef VERBOSE - std::cout << "begin line " << line << '\n'; - #endif - size_t pos = line.find_first_of(DELIMITERS, 0); - #ifdef VERBOSE - std::cout << "pos " << pos << '\n'; - #endif - size_t pos_char = line.find_first_of(CHAR_DELIMITERS, 0); - - if(pos!=std::string::npos) - { - std::string decision = line.substr(0, pos); - line.erase(0, pos+1); - #ifdef VERBOSE - std::cout << "i am here\n"; - std::cout << decision << '\n'; - std::cout << "line" << line << '\n'; - #endif - if(!decision.compare(std::string("c"))) - { - #ifdef VERBOSE - std::cout << "c \n"; - #endif - break; - } - - if(!decision.compare(std::string("p"))) - { - #ifdef VERBOSE - std::cout << "p \n"; - #endif - break; - } - - if(pos_char == std::string::npos) // no char present in the clause - { - int parsed_lit = unsafe_string2int(decision); - #ifdef VERBOSE - std::cout << "parsed_lit " << parsed_lit << " \n"; - #endif - if(parsed_lit == 0) - { - bvt no_dup=cnft::eliminate_duplicates(new_bv); - #ifdef VERBOSE - std::cout << "calling lcnf " << new_bv.size() << '\n'; - #endif - dest.lcnf(no_dup); - new_bv.clear(); - no_dup.clear(); - } - else - { - unsigned var = abs(parsed_lit); // because of the const variable - literalt l; - bool sign = (parsed_lit > 0) ? false : true; - l.set(var, sign); - #ifdef VERBOSE - std::cout << "setting l to " << l.get() << '\n'; - #endif - new_bv.push_back(l); - if(dest.no_variables() <= var) - dest.set_no_variables(var+1); - } - } - } - } - } -} diff --git a/src/solvers/sat/read_dimacs_cnf.h b/src/solvers/sat/read_dimacs_cnf.h deleted file mode 100644 index 96bb752867a..00000000000 --- a/src/solvers/sat/read_dimacs_cnf.h +++ /dev/null @@ -1,19 +0,0 @@ -/*******************************************************************\ - -Module: Reading DIMACS CNF - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Reading DIMACS CNF - -#ifndef CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H -#define CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H - -#include "cnf.h" - -void read_dimacs_cnf(std::istream &in, cnft &dest); - -#endif // CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H From a0fd3f7be612061f37aaaaed170fe61bba58040b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 13:04:57 +0100 Subject: [PATCH 2/4] Remove support for Limmat as a SAT solver It wasn't available via configuration options anymore anyway and Limmat's victory at the SAT competition dates back to 2002. --- src/solvers/CMakeLists.txt | 4 - src/solvers/Makefile | 8 -- src/solvers/sat/satcheck_limmat.cpp | 137 ---------------------------- src/solvers/sat/satcheck_limmat.h | 33 ------- 4 files changed, 182 deletions(-) delete mode 100644 src/solvers/sat/satcheck_limmat.cpp delete mode 100644 src/solvers/sat/satcheck_limmat.h diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 5acd6652114..f41995fd662 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -44,9 +44,6 @@ set(booleforce_source set(minibdd_source ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp ) -set(limmat_source - ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp -) file(GLOB_RECURSE sources "*.cpp" "*.h") list(REMOVE_ITEM sources @@ -62,7 +59,6 @@ list(REMOVE_ITEM sources ${lingeling_source} ${booleforce_source} ${minibdd_source} - ${limmat_source} ) add_library(solvers ${sources}) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 20100504caa..8a2b869783f 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -77,13 +77,6 @@ ifneq ($(LINGELING),) CP_CXXFLAGS += -DHAVE_LINGELING endif -ifneq ($(LIMMAT),) - LIMMAT_SRC=sat/satcheck_limmat.cpp - LIMMAT_INCLUDE=-I $(LIMMAT) - LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT) - CP_CXXFLAGS += -DHAVE_LIMMAT -endif - SRC = $(BOOLEFORCE_SRC) \ $(CHAFF_SRC) \ $(CUDD_SRC) \ @@ -96,7 +89,6 @@ SRC = $(BOOLEFORCE_SRC) \ $(PRECOSAT_SRC) \ $(SMVSAT_SRC) \ $(SQUOLEM2_SRC) \ - $(LIMMAT_SRC) \ cvc/cvc_conv.cpp \ cvc/cvc_dec.cpp \ flattening/arrays.cpp \ diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp deleted file mode 100644 index 10fd310ff35..00000000000 --- a/src/solvers/sat/satcheck_limmat.cpp +++ /dev/null @@ -1,137 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "satcheck_limmat.h" - -#include - -extern "C" -{ -#include "limmat.h" -} - -satcheck_limmatt::satcheck_limmatt() -{ - solver=new_Limmat(NULL); -} - -satcheck_limmatt::~satcheck_limmatt() -{ - if(solver!=NULL) - delete_Limmat(solver); -} - -tvt satcheck_limmatt::l_get(literalt a) const -{ - if(a.is_true()) - return tvt(true); - else if(a.is_false()) - return tvt(false); - - tvt result; - unsigned v=a.var_no(); - - assert(vsize()+1]; - - for(unsigned j=0; jsize(); j++) - clause[j]=(*it)[j].dimacs(); - - // zero-terminated - clause[it->size()]=0; - - add_Limmat(solver, clause); - - delete clause; - } -} - -propt::resultt satcheck_limmatt::prop_solve() -{ - copy_cnf(); - - { - std::string msg= - std::to_string(maxvar_Limmat(solver))+" variables, "+ - std::to_string(clauses_Limmat(solver))+" clauses"; - messaget::status() << msg << messaget::eom; - } - - int status=sat_Limmat(solver, -1); - - { - std::string msg; - - switch(status) - { - case 0: - msg="SAT checker: instance is UNSATISFIABLE"; - break; - - case 1: - msg="SAT checker: instance is SATISFIABLE"; - break; - - default: - msg="SAT checker failed: unknown result"; - break; - } - - messaget::status() << msg << messaget::eom; - } - - if(status==0) - { - assignment.clear(); - return P_UNSATISFIABLE; - } - - if(status==1) - { - assignment.resize(no_variables()+1, 2); // unknown is default - - for(const int *a=assignment_Limmat(solver); *a!=0; a++) - { - int v=*a; - if(v<0) - v=-v; - assert((unsigned)v=0; - } - - return P_SATISFIABLE; - } - - return P_ERROR; -} diff --git a/src/solvers/sat/satcheck_limmat.h b/src/solvers/sat/satcheck_limmat.h deleted file mode 100644 index 91e8e3d9df8..00000000000 --- a/src/solvers/sat/satcheck_limmat.h +++ /dev/null @@ -1,33 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H -#define CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H - -#include -#include "dimacs_cnf.h" - -class satcheck_limmatt:public dimacs_cnft -{ - public: - satcheck_limmatt(); - virtual ~satcheck_limmatt(); - - virtual const std::string solver_text(); - virtual resultt prop_solve(); - virtual tvt l_get(literalt a) const; - - void copy_cnf(); - - protected: - struct Limmat *solver; - std::vector assignment; -}; - -#endif // CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H From 2aa81eb25b353976277bcc7e2675986c860ccb54 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 13:08:34 +0100 Subject: [PATCH 3/4] 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. --- src/config.inc | 5 - src/solvers/CMakeLists.txt | 4 - src/solvers/Makefile | 11 +- src/solvers/sat/satcheck_smvsat.cpp | 233 ---------------------------- src/solvers/sat/satcheck_smvsat.h | 90 ----------- 5 files changed, 2 insertions(+), 341 deletions(-) delete mode 100644 src/solvers/sat/satcheck_smvsat.cpp delete mode 100644 src/solvers/sat/satcheck_smvsat.h diff --git a/src/config.inc b/src/config.inc index 93b44e39a50..3c0ad3397d3 100644 --- a/src/config.inc +++ b/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" diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index f41995fd662..c61355546b1 100644 --- a/src/solvers/CMakeLists.txt +++ b/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} diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 8a2b869783f..e89ef96dde1 100644 --- a/src/solvers/Makefile +++ b/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) ############################################################################### diff --git a/src/solvers/sat/satcheck_smvsat.cpp b/src/solvers/sat/satcheck_smvsat.cpp deleted file mode 100644 index 1018a4d96b1..00000000000 --- a/src/solvers/sat/satcheck_smvsat.cpp +++ /dev/null @@ -1,233 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "satcheck_smvsat.h" - -#include -#include - -#include -#include - -satcheck_smvsatt::satcheck_smvsatt() -{ - satsolver= - sat_instance_new_type(SATSOLVERCORE1, no_variables(), true); - - // now we can do l_const - init_const(); -} - -satcheck_smvsat_coret::satcheck_smvsat_coret() -{ -} - -satcheck_smvsatt::~satcheck_smvsatt() -{ -} - -tvt satcheck_smvsatt::l_get(literalt a) const -{ - assert(status==SAT); - - if(a.is_true()) - return tvt(true); - else if(a.is_false()) - return tvt(false); - - tvt result; - unsigned v=a.var_no(); - - switch(sat_instance_value(satsolver, v)) - { - case 0: result=tvt(false); break; - case 1: result=tvt(true); break; - default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break; - } - - if(a.sign()) - result=!result; - - return result; -} - -const std::string satcheck_smvsatt::solver_text() -{ - return std::string("SMVSAT"); -} - -void satcheck_smvsatt::lcnf(const bvt &bv) -{ - bvt tmp; - - if(process_clause(bv, tmp)) - return; - - int *lits=new int[tmp.size()+1]; - - for(unsigned i=0; iset_clause_partition(i, p); - } - - int output=interpolator_satsolver->interpolate(0, 0); - - build_aig(*interpolator_satsolver, output, dest); - - delete interpolator_satsolver; -} - -void satcheck_smvsat_interpolatort::build_aig( - // NOLINTNEXTLINE(readability/identifiers) - struct interpolator &interpolator_satsolver, - int output, - exprt &dest) -{ - std::stack stack; - - stack.push(entryt(output, &dest)); - - while(!stack.empty()) - { - entryt x=stack.top(); - stack.pop(); - - bool invert=x.g<0; - int n=invert?-x.g:x.g; - - assert(n!=0); - - exprt &e=*x.e; - - if(n==INT_MAX) - e.make_true(); - else if(n<=satsolver->num_variables()) - { // a SAT variable - e.id(ID_symbol); - e.set(ID_identifier, n); - } - else - { - e.id(ID_and); - e.operands().resize(2); - - unsigned g0=interpolator_satsolver.aig_arg(n, 0); - unsigned g1=interpolator_satsolver.aig_arg(n, 1); - - stack.push(entryt(g0, &e.op0())); - stack.push(entryt(g1, &e.op1())); - } - - if(invert) - e.make_not(); - } -} diff --git a/src/solvers/sat/satcheck_smvsat.h b/src/solvers/sat/satcheck_smvsat.h deleted file mode 100644 index c9d13c1d000..00000000000 --- a/src/solvers/sat/satcheck_smvsat.h +++ /dev/null @@ -1,90 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H -#define CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H - -#include -#include - -#include - -#include "cnf.h" - -class satcheck_smvsatt:public cnf_solvert -{ -public: - satcheck_smvsatt(); - virtual ~satcheck_smvsatt(); - - virtual const std::string solver_text(); - virtual resultt prop_solve(); - virtual tvt l_get(literalt a) const; - virtual void lcnf(const bvt &bv); - -protected: - // NOLINTNEXTLINE(readability/identifiers) - struct sat_instance *satsolver; -}; - -class satcheck_smvsat_coret:public satcheck_smvsatt -{ -public: - satcheck_smvsat_coret(); - - virtual resultt prop_solve(); - - bool is_in_core(literalt l) const - { - assert(l.var_no() in_core; -}; - -class satcheck_smvsat_interpolatort:public satcheck_smvsatt -{ -public: - satcheck_smvsat_interpolatort():partition_no(0) - { - } - - void set_partition_no(short p) - { - partition_no=p; - } - - void interpolate(exprt &dest); - -protected: - virtual void lcnf(const bvt &bv); - short partition_no; - - std::vector partition_numbers; - - void build_aig( - // NOLINTNEXTLINE(readability/identifiers) - struct interpolator &interpolator_satsolver, - int output, - exprt &dest); - - struct entryt - { - int g; - exprt *e; - - entryt(int _g, exprt *_e):g(_g), e(_e) - { - } - }; -}; - -#endif // CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H From 70741ff1c757889fd086b37baf07262f6c7290c5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Apr 2018 13:17:32 +0100 Subject: [PATCH 4/4] Remove support for Precosat Precosat has last been released in 2010. --- src/common | 6 +- src/config.inc | 5 -- src/solvers/CMakeLists.txt | 4 - src/solvers/Makefile | 12 +-- src/solvers/sat/satcheck.h | 12 --- src/solvers/sat/satcheck_precosat.cpp | 121 -------------------------- src/solvers/sat/satcheck_precosat.h | 44 ---------- 7 files changed, 3 insertions(+), 201 deletions(-) delete mode 100644 src/solvers/sat/satcheck_precosat.cpp delete mode 100644 src/solvers/sat/satcheck_precosat.h diff --git a/src/common b/src/common index e4f1ecdb35b..ef872268350 100644 --- a/src/common +++ b/src/common @@ -159,7 +159,7 @@ 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 @@ -167,10 +167,6 @@ ifneq ($(IPASIR),) CP_CXXFLAGS += -DHAVE_IPASIR endif -ifneq ($(PRECOSAT),) - CP_CXXFLAGS += -DHAVE_PRECOSAT -endif - ifneq ($(PICOSAT),) CP_CXXFLAGS += -DHAVE_PICOSAT endif diff --git a/src/config.inc b/src/config.inc index 3c0ad3397d3..5f2b7d9d4ec 100644 --- a/src/config.inc +++ b/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 diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index c61355546b1..19aa7d29c55 100644 --- a/src/solvers/CMakeLists.txt +++ b/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} diff --git a/src/solvers/Makefile b/src/solvers/Makefile index e89ef96dde1..ab0f2cb2f7f 100644 --- a/src/solvers/Makefile +++ b/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) ############################################################################### diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h index cc20e33476a..6896be55da4 100644 --- a/src/solvers/sat/satcheck.h +++ b/src/solvers/sat/satcheck.h @@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com // #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, kroening@kroening.com #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" diff --git a/src/solvers/sat/satcheck_precosat.cpp b/src/solvers/sat/satcheck_precosat.cpp deleted file mode 100644 index 6e9a2248c94..00000000000 --- a/src/solvers/sat/satcheck_precosat.cpp +++ /dev/null @@ -1,121 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk - -\*******************************************************************/ - -#include "satcheck_precosat.h" - -#include - -#include - -#include - -#ifndef HAVE_PRECOSAT -#error "Expected HAVE_PRECOSAT" -#endif - -#define precosat_lit(a) ((a).var_no()*2 + !(a).sign()) - -tvt satcheck_precosatt::l_get(literalt a) const -{ - if(a.is_constant()) - return tvt(a.sign()); - - tvt result; - - if(a.var_no()>solver->getMaxVar()) - return tvt(tvt::tv_enumt::TV_UNKNOWN); - - const int val=solver->val(precosat_lit(a)); - if(val>0) - result=tvt(true); - else if(val<0) - result=tvt(false); - else - return tvt(tvt::tv_enumt::TV_UNKNOWN); - - return result; -} - -const std::string satcheck_precosatt::solver_text() -{ - return "PrecoSAT"; -} - -void satcheck_precosatt::lcnf(const bvt &bv) -{ - bvt new_bv; - - if(process_clause(bv, new_bv)) - return; - - forall_literals(it, new_bv) - solver->add(precosat_lit(*it)); - - solver->add(0); - - clause_counter++; -} - -propt::resultt satcheck_precosatt::prop_solve() -{ - assert(status!=ERROR); - - // We start counting at 1, thus there is one variable fewer. - { - std::string msg= - std::to_string(no_variables()-1)+" variables, "+ - std::to_string(solver->getAddedOrigClauses())+" clauses"; - messaget::status() << msg << messaget::eom; - } - - std::string msg; - - const int res=solver->solve(); - if(res==1) - { - msg="SAT checker: instance is SATISFIABLE"; - messaget::status() << msg << messaget::eom; - status=SAT; - return P_SATISFIABLE; - } - else - { - assert(res==-1); - msg="SAT checker: instance is UNSATISFIABLE"; - messaget::status() << msg << messaget::eom; - } - - status=UNSAT; - return P_UNSATISFIABLE; -} - -void satcheck_precosatt::set_assignment(literalt a, bool value) -{ - assert(false); -} - -satcheck_precosatt::satcheck_precosatt() : - solver(new PrecoSat::Solver()) -{ - solver->init(); -} - -satcheck_precosatt::~satcheck_precosatt() -{ - delete solver; -} - -/* -void satcheck_precosatt::set_assumptions(const bvt &bv) -{ - assumptions=bv; - - forall_literals(it, assumptions) - assert(!it->is_constant()); -} -*/ diff --git a/src/solvers/sat/satcheck_precosat.h b/src/solvers/sat/satcheck_precosat.h deleted file mode 100644 index 78caad55d7d..00000000000 --- a/src/solvers/sat/satcheck_precosat.h +++ /dev/null @@ -1,44 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk - -\*******************************************************************/ - - -#ifndef CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H -#define CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H - -#include "cnf.h" - -namespace PrecoSat // NOLINT(readability/namespace) -{ -class Solver; // NOLINT(readability/identifiers) -} - -class satcheck_precosatt:public cnf_solvert -{ -public: - satcheck_precosatt(); - virtual ~satcheck_precosatt(); - - virtual const std::string solver_text(); - virtual resultt prop_solve(); - virtual tvt l_get(literalt a) const; - - virtual void lcnf(const bvt &bv); - virtual void set_assignment(literalt a, bool value); - - // PicoSAT has this, PrecoSAT doesn't - // virtual bool is_in_conflict(literalt a) const; - // virtual void set_assumptions(const bvt &_assumptions); - virtual bool has_set_assumptions() const { return false; } - virtual bool has_is_in_conflict() const { return false; } - -protected: - PrecoSat::Solver *solver; - // bvt assumptions; -}; - -#endif // CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H