1 files changed, 104 insertions, 74 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 3da574f6c..977da46e5 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -1,5 +1,6 @@
 /************************************************************************************[SimpSolver.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2006,      Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,158 +18,187 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_SimpSolver_h
+#define Minisat_SimpSolver_h
 
-#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
-#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
+#include "cvc4_private.h"
 
-#include <cstdio>
-#include <cassert>
+#include "mtl/Queue.h"
+#include "core/Solver.h"
 
-#include "../mtl/Queue.h"
-#include "../core/Solver.h"
 
 namespace CVC4 {
 namespace prop {
+  class SatSolver;
+}
+}
 
-class SatSolver;
+namespace Minisat {
 
-namespace minisat {
+//=================================================================================================
 
 class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver(SatSolver* proxy, context::Context* context);
+    SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context);
     CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
-    bool    addClause (vec<Lit>& ps, ClauseType type);
+    bool    addClause (const vec<Lit>& ps, ClauseType type);
+    bool    addEmptyClause(ClauseType type);                  // Add the empty clause to the solver.
+    bool    addClause (Lit p, ClauseType type);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, ClauseType type);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps, ClauseType type);
+    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
     // 
     void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+    bool    isEliminated(Var v) const;
 
     // Solving:
     //
-    bool    solve     (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
-    bool    solve     (bool do_simp = true, bool turn_off_simp = false);
-    bool    eliminate (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
+    bool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    lbool   solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
+    bool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
+
+    // Memory managment:
+    //
+    virtual void garbageCollect();
+
 
     // Generate a (possibly simplified) DIMACS file:
     //
+#if 0
+    void    toDimacs  (const char* file, const vec<Lit>& assumps);
     void    toDimacs  (const char* file);
+    void    toDimacs  (const char* file, Lit p);
+    void    toDimacs  (const char* file, Lit p, Lit q);
+    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);
+#endif
 
     // Mode of operation:
     //
-    int     grow;             // Allow a variable elimination step to grow by a number of clauses (default to zero).
-    bool    asymm_mode;       // Shrink clauses by asymmetric branching.
-    bool    redundancy_check; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).
+    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.
+                               // -1 means no limit.
+    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.
+    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+    bool    use_asymm;         // Shrink clauses by asymmetric branching.
+    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+    bool    use_elim;          // Perform variable elimination.
 
     // Statistics:
     //
     int     merges;
     int     asymm_lits;
-    int     remembered_clauses;
+    int     eliminated_vars;
 
-// protected:
-  public:
+ protected:
 
     // Helper structures:
     //
-    struct ElimData {
-        int          order;      // 0 means not eliminated, >0 gives an index in the elimination order
-        vec<Clause*> eliminated;
-        ElimData() : order(0) {} };
-
-    struct ElimOrderLt {
-        const vec<ElimData>& elimtable;
-        ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
-        bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
-
     struct ElimLt {
         const vec<int>& n_occ;
-        ElimLt(const vec<int>& no) : n_occ(no) {}
-        int  cost      (Var x)        const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
-        bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
-
+        explicit ElimLt(const vec<int>& no) : n_occ(no) {}
+
+        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+        // 32-bit implementation instead then, but this will have to do for now.
+        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
+        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+        
+        // TODO: investigate this order alternative more.
+        // bool operator()(Var x, Var y) const { 
+        //     int c_x = cost(x);
+        //     int c_y = cost(y);
+        //     return c_x < c_y || c_x == c_y && x < y; }
+    };
+
+    struct ClauseDeleted {
+        const ClauseAllocator& ca;
+        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
 
     // Solver state:
     //
     int                 elimorder;
     bool                use_simplification;
-    vec<ElimData>       elimtable;
+    vec<uint32_t>       elimclauses;
     vec<char>           touched;
-    vec<vec<Clause*> >  occurs;
+    OccLists<Var, vec<CRef>, ClauseDeleted>
+                        occurs;
     vec<int>            n_occ;
     Heap<ElimLt>        elim_heap;
-    Queue<Clause*>      subsumption_queue;
+    Queue<CRef>         subsumption_queue;
     vec<char>           frozen;
+    vec<char>           eliminated;
     int                 bwdsub_assigns;
+    int                 n_touched;
 
     // Temporaries:
     //
-    Clause*             bwdsub_tmpunit;
+    CRef                bwdsub_tmpunit;
 
     // Main internal methods:
     //
-    bool          asymm                    (Var v, Clause& c);
+    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);
+    bool          asymm                    (Var v, CRef cr);
     bool          asymmVar                 (Var v);
     void          updateElimHeap           (Var v);
-    void          cleanOcc                 (Var v);
-    vec<Clause*>& getOccurs                (Var x);
     void          gatherTouchedClauses     ();
     bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
-    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v);
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);
     bool          backwardSubsumptionCheck (bool verbose = false);
-    bool          eliminateVar             (Var v, bool fail = false);
-    void          remember                 (Var v);
+    bool          eliminateVar             (Var v);
     void          extendModel              ();
-    void          verifyModel              ();
 
-    void          removeClause             (Clause& c);
-    bool          strengthenClause         (Clause& c, Lit l);
+    void          removeClause             (CRef cr);
+    bool          strengthenClause         (CRef cr, Lit l);
     void          cleanUpClauses           ();
     bool          implied                  (const vec<Lit>& c);
-    void          toDimacs                 (FILE* f, Clause& c);
-    bool          isEliminated             (Var v) const;
-
+    void          relocAll                 (ClauseAllocator& to);
 };
 
 
 //=================================================================================================
 // Implementation of inline methods:
 
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
 inline void SimpSolver::updateElimHeap(Var v) {
-    if (elimtable[v].order == 0)
+    assert(use_simplification);
+    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
         elim_heap.update(v); }
 
-inline void SimpSolver::cleanOcc(Var v) {
-    assert(use_simplification);
-    Clause **begin = (Clause**)occurs[v];
-    Clause **end = begin + occurs[v].size();
-    Clause **i, **j;
-    for (i = begin, j = end; i < j; i++)
-        if ((*i)->mark() == 1){
-            *i = *(--j);
-            i--;
-        }
-    //occurs[v].shrink_(end - j);  // This seems slower. Why?!
-    occurs[v].shrink(end - j);
-}
 
-inline vec<Clause*>& SimpSolver::getOccurs(Var x) {
-    cleanOcc(x); return occurs[x]; }
+inline bool SimpSolver::addClause    (const vec<Lit>& ps, ClauseType type)    { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addEmptyClause(ClauseType type)                       { add_tmp.clear(); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addClause    (Lit p, ClauseType type)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, ClauseType type)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, ClauseType type)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); }
+inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
-inline bool  SimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; }
-inline void  SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
-inline bool  SimpSolver::solve        (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
+inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
 
 //=================================================================================================
-#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */
+}
+
+#endif