Either fix it or break it

mwolf76 · Jan 1, 2014 · 16bb72e · 16bb72e
1 parent 6abdd85
commit 16bb72e
Show file tree

Hide file tree

Showing 21 changed files with 79 additions and 112 deletions.
diff --git 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 -I$(top_srcdir)/src/dd/cudd-2.5.0/cudd		\
--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/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
-PKG_HH = satdefs.hh sat.hh time_mapper.hh proof/simple.hh		\
+PKG_CC = time_mapper.cc cnf_nocut.cc cnf_singlecut.cc solver.cc	\
-proof/interpolator.hh proof/proof.hh terms/terms.hh terms/ddterms.hh	\
+proof.cc interpolator.cc logger.cc
-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_SOURCES = $(PKG_H) $(PKG_CC)
 
 # -------------------------------------------------------
 
-noinst_LTLIBRARIES = libminisat.la
+noinst_LTLIBRARIES = libsat.la
-libminisat_la_SOURCES = $(PKG_SOURCES)
+libsat_la_SOURCES = $(PKG_SOURCES)
diff --git 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 <sat.hh>
 #include <dd_walker.hh>
 
-#if 0
 namespace Minisat {
+#if 0
 
     class CNFBuilderNoCut : public ADDWalker {
     public:
-        CNFBuilderNoCut(CuddMgr& mgr, SAT& sat)
+        CNFBuilderNoCut(SAT& sat, step_t time, group_t group, color_t color)
-            : ADDWalker()
+            : f_sat(sat)
-            , f_sat(sat)
+            // , f_time(time),
-            , f_owner(mgr)
+            // , 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<Lit> ps; ps.push(f_sat.cnf_find_group_lit(group));
+            vec<Lit> 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
@@ -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 <dd_walker.hh>
 
-// #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
@@ -24,11 +24,11 @@
  *
  **/
 #include <sat.hh>
+#include <proof.hh>
 
 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
@@ -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<Lit> &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
@@ -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 <common.hh>
 using namespace Minisat;

diff --git 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 "minisat/mtl/Vec.hh"
-#include "mtl/Heap.hh"
+#include "minisat/mtl/Heap.hh"
-#include "mtl/Alg.hh"
+#include "minisat/mtl/Alg.hh"
-#include "utils/Options.hh"
+#include "minisat/utils/Options.hh"
-#include "core/SolverTypes.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
@@ -28,11 +28,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <iostream>
 using std::ostream;
 
-#include "mtl/IntTypes.hh"
+#include "minisat/mtl/IntTypes.hh"
-#include "mtl/Alg.hh"
+#include "minisat/mtl/Alg.hh"
-#include "mtl/Vec.hh"
+#include "minisat/mtl/Vec.hh"
-#include "mtl/Map.hh"
+#include "minisat/mtl/Map.hh"
-#include "mtl/Alloc.hh"
+#include "minisat/mtl/Alloc.hh"
 
 namespace Minisat {
 

diff --git 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
@@ -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 "minisat/mtl/XAlloc.hh"
-#include "mtl/Vec.hh"
+#include "minisat/mtl/Vec.hh"
 
 namespace Minisat {
 

diff --git 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
@@ -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 "minisat/mtl/IntTypes.hh"
-#include "mtl/Vec.hh"
+#include "minisat/mtl/Vec.hh"
 
 namespace Minisat {
 

diff --git 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
@@ -24,8 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 #include <new>
 
-#include "mtl/IntTypes.hh"
+#include "minisat/mtl/IntTypes.hh"
-#include "mtl/XAlloc.hh"
+#include "minisat/mtl/XAlloc.hh"
 
 namespace Minisat {
 

diff --git 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 <math.h>
 #include <string.h>
 
-#include "mtl/IntTypes.hh"
+#include "minisat/mtl/IntTypes.hh"
-#include "mtl/Vec.hh"
+#include "minisat/mtl/Vec.hh"
-#include "utils/ParseUtils.hh"
+#include "minisat/utils/ParseUtils.hh"
 
 namespace Minisat {
 

diff --git 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 <stack>
 
 #include "proof.hh"
-#include <mtl/Sort.hh>
 
 namespace Minisat {
 

diff --git 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 <Vec.hh>
+#include <common.hh>
-#include <Map.hh>
 
-#include "core/Solver.hh"
+#include <minisat/mtl/Vec.hh>
+#include <minisat/mtl/Map.hh>
+#include <minisat/mtl/Sort.hh>
 
-#include <common.hh>
+#include "minisat/core/Solver.hh"
-#include "utils/solverlogger.hh"
 
 // comment this out to disable debugging
 // #define DEBUG_PROOF_LOGGING