From 16bb72e59b8f0cb41d0f51cb1afcea3baf979afa Mon Sep 17 00:00:00 2001 From: Markus Wolf Date: Wed, 1 Jan 2014 13:04:35 +0100 Subject: [PATCH] Either fix it or break it --- src/sat/Makefile.am | 24 ++++++++------------- src/sat/cnf_nocut.cc | 33 ++++++++++++----------------- src/sat/cnf_singlecut.cc | 6 +----- src/sat/interpolator.cc | 5 ++--- src/sat/logger.cc | 9 +++----- src/sat/minisat/core/Solver.cc | 2 +- src/sat/minisat/core/Solver.hh | 10 ++++----- src/sat/minisat/core/SolverTypes.hh | 10 ++++----- src/sat/minisat/mtl/Alg.hh | 2 +- src/sat/minisat/mtl/Alloc.hh | 4 ++-- src/sat/minisat/mtl/Heap.hh | 2 +- src/sat/minisat/mtl/Map.hh | 4 ++-- src/sat/minisat/mtl/Sort.hh | 2 +- src/sat/minisat/mtl/Vec.hh | 4 ++-- src/sat/minisat/utils/Options.hh | 6 +++--- src/sat/proof.cc | 4 ---- src/sat/proof.hh | 13 +++++------- src/sat/sat.hh | 30 ++++++++++++++------------ src/sat/satdefs.hh | 17 +++++---------- src/sat/terms/terms.hh | 2 -- src/sat/time_mapper.hh | 2 -- 21 files changed, 79 insertions(+), 112 deletions(-) diff --git a/src/sat/Makefile.am b/src/sat/Makefile.am index 82f53352..682f5c5e 100644 --- a/src/sat/Makefile.am +++ b/src/sat/Makefile.am @@ -1,3 +1,6 @@ +AUTOMAKE_OPTIONS = subdir-objects +SUBDIRS = minisat + AM_CPPFLAGS = @AM_CPPFLAGS@ AM_CFLAGS = @AM_CFLAGS@ AM_CXXFLAGS = -Wno-unused-variable -Wno-unused-function @@ -6,28 +9,19 @@ INCLUDES = -I$(top_srcdir)/src/ -I$(top_srcdir)/src/dd \ -I$(top_srcdir)/src/enc -I$(top_srcdir)/src/expr \ -I$(top_srcdir)/src/type -I$(top_srcdir)/src/model \ -I$(top_srcdir)/src/witness -I$(top_srcdir)/src/3rdparty/ezlogger \ --I$(top_srcdir)/src/sat/core -I$(top_srcdir)/src/sat/mtl \ --I$(top_srcdir)/src/sat/proof -I$(top_srcdir)/src/sat/utils \ --I$(top_srcdir)/src/dd/cudd-2.5.0/cudd \ +-I$(top_srcdir)/src/sat -I$(top_srcdir)/src/dd/cudd-2.5.0/cudd \ -I$(top_srcdir)/src/dd/cudd-2.5.0/mtr \ -I$(top_srcdir)/src/dd/cudd-2.5.0/st \ -I$(top_srcdir)/src/dd/cudd-2.5.0/util \ -I$(top_srcdir)/src/dd/cudd-2.5.0/obj - -PKG_HH = satdefs.hh sat.hh time_mapper.hh proof/simple.hh \ -proof/interpolator.hh proof/proof.hh terms/terms.hh terms/ddterms.hh \ -core/SolverTypes.hh core/Solver.hh mtl/Alloc.hh mtl/Sort.hh mtl/Set.hh \ -mtl/Heap.hh mtl/Map.hh mtl/Alg.hh mtl/Vec.hh mtl/IntTypes.hh \ -mtl/Queue.hh mtl/XAlloc.hh utils/Options.hh utils/solverlogger.hh \ -utils/System.hh utils/ParseUtils.hh - -PKG_CC = proof/proof.cc core/Solver.cc utils/Options.cc time_mapper.cc \ -cnf_nocut.cc cnf_singlecut.cc logger.cc interpolator.cc solver.cc +PKG_HH = satdefs.hh sat.hh +PKG_CC = time_mapper.cc cnf_nocut.cc cnf_singlecut.cc solver.cc \ +proof.cc interpolator.cc logger.cc PKG_SOURCES = $(PKG_H) $(PKG_CC) # ------------------------------------------------------- -noinst_LTLIBRARIES = libminisat.la -libminisat_la_SOURCES = $(PKG_SOURCES) +noinst_LTLIBRARIES = libsat.la +libsat_la_SOURCES = $(PKG_SOURCES) diff --git a/src/sat/cnf_nocut.cc b/src/sat/cnf_nocut.cc index c9e7abad..a3a061d9 100644 --- a/src/sat/cnf_nocut.cc +++ b/src/sat/cnf_nocut.cc @@ -2,10 +2,6 @@ * @file sat.cc * @brief SAT interface implementation * - * This module contains the interface for services that implement an - * CNF clauses generation in a form that is suitable for direct - * injection into the SAT solver. - * * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com > * * This library is free software; you can redistribute it and/or @@ -26,15 +22,17 @@ #include #include -#if 0 namespace Minisat { +#if 0 class CNFBuilderNoCut : public ADDWalker { public: - CNFBuilderNoCut(CuddMgr& mgr, SAT& sat) - : ADDWalker() - , f_sat(sat) - , f_owner(mgr) + CNFBuilderNoCut(SAT& sat, step_t time, group_t group, color_t color) + : f_sat(sat) + // , f_time(time), + // , f_group(group) + // , f_color(color) + , f_owner(CuddMgr::INSTANCE()) {} ~CNFBuilderNoCut() @@ -54,17 +52,14 @@ namespace Minisat { group_t group = MAINGROUP; color_t color = BACKGROUND; - vec ps; ps.push(f_sat.cnf_find_group_lit(group)); - + vec ps; ps.push( f_sat.cnf_find_group_lit( group)); unsigned i, size = f_owner.dd().getManager()->size; - int v; for (i = 0; i < size; ++ i) { - v = f_data[i]; - if (v == 0) { + if (value == 0) { ps.push( mkLit( f_sat.cnf_find_index_var(i), false)); } - else if (v == 1) { + else if (value == 1) { ps.push( mkLit( f_sat.cnf_find_index_var(i), true)); } else { @@ -85,11 +80,11 @@ namespace Minisat { CuddMgr& f_owner; }; - void SAT::cnf_push_no_cut(Term phi, const group_t group, const color_t color) + void SAT::cnf_push_no_cut(Term phi, step_t time, const group_t group, const color_t color) { - CNFBuilderNoCut builder(CuddMgr::INSTANCE(), *this); + CNFBuilderNoCut builder(*this, time, group, color); builder(phi); } - -}; #endif +}; + diff --git a/src/sat/cnf_singlecut.cc b/src/sat/cnf_singlecut.cc index 5be8d882..3c72a856 100644 --- a/src/sat/cnf_singlecut.cc +++ b/src/sat/cnf_singlecut.cc @@ -2,10 +2,6 @@ * @file sat.cc * @brief SAT interface implementation * - * This module contains the interface for services that implement an - * CNF clauses generation in a form that is suitable for direct - * injection into the SAT solver. - * * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com > * * This library is free software; you can redistribute it and/or @@ -28,7 +24,7 @@ #include -// #define DEBUG_CNF +#define DEBUG_CNF namespace Minisat { /* internal, used only for CNF-ization */ diff --git a/src/sat/interpolator.cc b/src/sat/interpolator.cc index 64540008..2cb41e75 100644 --- a/src/sat/interpolator.cc +++ b/src/sat/interpolator.cc @@ -24,11 +24,11 @@ * **/ #include +#include namespace Minisat { -#if 0 // TODO LATER - +#if 0 Term SAT::itp_build_interpolant(const Colors& a) { // local accessors @@ -197,6 +197,5 @@ namespace Minisat { } } // for each literal in the clause } // SAT::init_interpolation - #endif }; diff --git a/src/sat/logger.cc b/src/sat/logger.cc index c71b00b9..10767936 100644 --- a/src/sat/logger.cc +++ b/src/sat/logger.cc @@ -29,8 +29,8 @@ namespace Minisat { ostream &operator<<(ostream &out, const Lit &lit) { - out << (sign(lit) ? "~" : "") << var(lit); - + if (!var(lit)) return out; + out << (sign(lit) ? "-" : "") << var(lit); return out; } @@ -54,16 +54,13 @@ namespace Minisat { ostream &operator<<(ostream &out, const vec &lits) { - out << "{"; - for (int i = 0; i < lits.size()-1; ++i) { - out << lits[i] << " ; "; + out << lits[i] << " "; } if (0 != lits.size()) { out << lits[lits.size()-1]; } - out << "}"; return out; } diff --git a/src/sat/minisat/core/Solver.cc b/src/sat/minisat/core/Solver.cc index 93f7dc0d..02046182 100644 --- a/src/sat/minisat/core/Solver.cc +++ b/src/sat/minisat/core/Solver.cc @@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.hh" #include "core/Solver.hh" -#include "proof/proof.hh" +#include "proof.hh" #include using namespace Minisat; diff --git a/src/sat/minisat/core/Solver.hh b/src/sat/minisat/core/Solver.hh index fbcb2d2d..b6f96879 100644 --- a/src/sat/minisat/core/Solver.hh +++ b/src/sat/minisat/core/Solver.hh @@ -23,11 +23,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Solver_h #define Minisat_Solver_h -#include "mtl/Vec.hh" -#include "mtl/Heap.hh" -#include "mtl/Alg.hh" -#include "utils/Options.hh" -#include "core/SolverTypes.hh" +#include "minisat/mtl/Vec.hh" +#include "minisat/mtl/Heap.hh" +#include "minisat/mtl/Alg.hh" +#include "minisat/utils/Options.hh" +#include "minisat/core/SolverTypes.hh" #ifdef NDEBUG #undef PROOF_CHECK // disable proof self checking diff --git a/src/sat/minisat/core/SolverTypes.hh b/src/sat/minisat/core/SolverTypes.hh index b38edc21..e49a9f9e 100644 --- a/src/sat/minisat/core/SolverTypes.hh +++ b/src/sat/minisat/core/SolverTypes.hh @@ -28,11 +28,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include using std::ostream; -#include "mtl/IntTypes.hh" -#include "mtl/Alg.hh" -#include "mtl/Vec.hh" -#include "mtl/Map.hh" -#include "mtl/Alloc.hh" +#include "minisat/mtl/IntTypes.hh" +#include "minisat/mtl/Alg.hh" +#include "minisat/mtl/Vec.hh" +#include "minisat/mtl/Map.hh" +#include "minisat/mtl/Alloc.hh" namespace Minisat { diff --git a/src/sat/minisat/mtl/Alg.hh b/src/sat/minisat/mtl/Alg.hh index bbf06444..ce3f86c3 100644 --- a/src/sat/minisat/mtl/Alg.hh +++ b/src/sat/minisat/mtl/Alg.hh @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alg_h #define Minisat_Alg_h -#include "mtl/Vec.hh" +#include "minisat/mtl/Vec.hh" namespace Minisat { diff --git a/src/sat/minisat/mtl/Alloc.hh b/src/sat/minisat/mtl/Alloc.hh index e5694c7f..b9c64d64 100644 --- a/src/sat/minisat/mtl/Alloc.hh +++ b/src/sat/minisat/mtl/Alloc.hh @@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alloc_h #define Minisat_Alloc_h -#include "mtl/XAlloc.hh" -#include "mtl/Vec.hh" +#include "minisat/mtl/XAlloc.hh" +#include "minisat/mtl/Vec.hh" namespace Minisat { diff --git a/src/sat/minisat/mtl/Heap.hh b/src/sat/minisat/mtl/Heap.hh index 94d44203..65870679 100644 --- a/src/sat/minisat/mtl/Heap.hh +++ b/src/sat/minisat/mtl/Heap.hh @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Heap_h #define Minisat_Heap_h -#include "mtl/Vec.hh" +#include "minisat/mtl/Vec.hh" namespace Minisat { diff --git a/src/sat/minisat/mtl/Map.hh b/src/sat/minisat/mtl/Map.hh index 4f7d306b..98507193 100644 --- a/src/sat/minisat/mtl/Map.hh +++ b/src/sat/minisat/mtl/Map.hh @@ -20,8 +20,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Map_h #define Minisat_Map_h -#include "mtl/IntTypes.hh" -#include "mtl/Vec.hh" +#include "minisat/mtl/IntTypes.hh" +#include "minisat/mtl/Vec.hh" namespace Minisat { diff --git a/src/sat/minisat/mtl/Sort.hh b/src/sat/minisat/mtl/Sort.hh index 34a7636d..1149826e 100644 --- a/src/sat/minisat/mtl/Sort.hh +++ b/src/sat/minisat/mtl/Sort.hh @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Sort_h #define Minisat_Sort_h -#include "mtl/Vec.hh" +#include "minisat/mtl/Vec.hh" //================================================================================================= // Some sorting algorithms for vec's diff --git a/src/sat/minisat/mtl/Vec.hh b/src/sat/minisat/mtl/Vec.hh index 66dddbb1..f39d55bc 100644 --- a/src/sat/minisat/mtl/Vec.hh +++ b/src/sat/minisat/mtl/Vec.hh @@ -24,8 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "mtl/IntTypes.hh" -#include "mtl/XAlloc.hh" +#include "minisat/mtl/IntTypes.hh" +#include "minisat/mtl/XAlloc.hh" namespace Minisat { diff --git a/src/sat/minisat/utils/Options.hh b/src/sat/minisat/utils/Options.hh index 13b85f00..e7b0bbe8 100644 --- a/src/sat/minisat/utils/Options.hh +++ b/src/sat/minisat/utils/Options.hh @@ -25,9 +25,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "mtl/IntTypes.hh" -#include "mtl/Vec.hh" -#include "utils/ParseUtils.hh" +#include "minisat/mtl/IntTypes.hh" +#include "minisat/mtl/Vec.hh" +#include "minisat/utils/ParseUtils.hh" namespace Minisat { diff --git a/src/sat/proof.cc b/src/sat/proof.cc index f0d19932..21da53b8 100644 --- a/src/sat/proof.cc +++ b/src/sat/proof.cc @@ -2,9 +2,6 @@ * @file proof.cc * @brief UNSAT proof logging * - * This module contains the definitions for Unsatisfiability proof - * logging. - * * Authors: Alberto Griggio, Marco Pensallorto * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com > * @@ -29,7 +26,6 @@ #include #include "proof.hh" -#include namespace Minisat { diff --git a/src/sat/proof.hh b/src/sat/proof.hh index dcfb5745..7932ab1d 100644 --- a/src/sat/proof.hh +++ b/src/sat/proof.hh @@ -2,9 +2,6 @@ * @file proof.hh * @brief UNSAT proof logging * - * This module contains the definitions for Unsatisfiability proof - * logging. - * * Authors: Alberto Griggio, Marco Pensallorto * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com > * @@ -26,13 +23,13 @@ #ifndef PROOF_H_DEFINED #define PROOF_H_DEFINED -#include -#include +#include -#include "core/Solver.hh" +#include +#include +#include -#include -#include "utils/solverlogger.hh" +#include "minisat/core/Solver.hh" // comment this out to disable debugging // #define DEBUG_PROOF_LOGGING diff --git a/src/sat/sat.hh b/src/sat/sat.hh index e1ab5c92..1fac77af 100644 --- a/src/sat/sat.hh +++ b/src/sat/sat.hh @@ -26,28 +26,30 @@ #ifndef SAT_H #define SAT_H -// general purpose decls +#include +#include + #include -#include "satdefs.hh" #include "terms/ddterms.hh" -#include "proof/proof.hh" -#include "cuddObj.hh" #include -/* MTL */ -#include -#include -#include - -// the glorious Minisat SAT solver -#include "core/Solver.hh" -#include "core/SolverTypes.hh" +// the Minisat SAT solver +#include +#include namespace Minisat { + using std::ostream; + + ostream &operator<<(ostream &out, const Lit &lit); + ostream &operator<<(ostream &out, const Clause *clause); + ostream &operator<<(ostream &out, const Clause &clause); + ostream &operator<<(ostream &out, const vec &lits); + class SAT : public IObject { friend class CNFBuilderSingleCut; + friend class CNFBuilderNoCut; public: /** @@ -206,6 +208,7 @@ namespace Minisat { Group2VarMap f_groups_map; +#if 0 // -- Interpolator ----------------------------------------------------- typedef struct ptr_hasher InferenceRuleHasher; typedef Map< InferenceRule* , Term, InferenceRuleHasher> R2T_Map; @@ -250,9 +253,10 @@ namespace Minisat { inline bool clause_is_of_A(CRef cr) const { return a_clauses.has(cr); } +#endif // -- Low level services ----------------------------------------------- - // Lit cnf_find_group_lit(group_t group, bool enabled = true); + Lit cnf_find_group_lit(group_t group, bool enabled = true); Term itp_build_interpolant(const Colors& a); void itp_init_interpolation(const Colors& ga); diff --git a/src/sat/satdefs.hh b/src/sat/satdefs.hh index 287f3966..f653264b 100644 --- a/src/sat/satdefs.hh +++ b/src/sat/satdefs.hh @@ -1,10 +1,6 @@ /** - * @file defs.hh - * @brief DEFS interface - * - * This module contains the interface for services that implement an - * CNF clauses generation in a form that is suitable for direct - * injection into the SAT solver. + * @file satdefs.hh + * @brief SAT interface * * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com > * @@ -29,14 +25,11 @@ #include #include -#include - -/* from MTL */ -#include - // for the definition of Term #include +#include + namespace Minisat { typedef unsigned id_t; @@ -69,7 +62,7 @@ namespace Minisat { typedef unsigned color_t; static color_t BACKGROUND(0); - typedef Set Colors; + typedef set Colors; typedef vector Variables; typedef vector Literals; diff --git a/src/sat/terms/terms.hh b/src/sat/terms/terms.hh index d4e74475..84af84a5 100644 --- a/src/sat/terms/terms.hh +++ b/src/sat/terms/terms.hh @@ -25,8 +25,6 @@ #ifndef TERMS_H_INCLUDED #define TERMS_H_INCLUDED -#include - namespace Minisat { template class TermFactory { diff --git a/src/sat/time_mapper.hh b/src/sat/time_mapper.hh index 4c5afdfc..b4f03c51 100644 --- a/src/sat/time_mapper.hh +++ b/src/sat/time_mapper.hh @@ -32,8 +32,6 @@ #include -#include "core/SolverTypes.hh" - namespace Minisat { class SAT; // fwd decl