from meeting

1 files changed, 166 insertions, 0 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
new file mode 100644
index 000000000..221b4c6e2
--- /dev/null
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -0,0 +1,166 @@
+/************************************************************************************[SimpSolver.h]
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef CVC4_MiniSat_SimpSolver_h
+#define CVC4_MiniSat_SimpSolver_h
+
+#include <cstdio>
+
+#include "Queue.h"
+#include "Solver.h"
+
+namespace CVC4 {
+namespace MiniSat {
+
+class SimpSolver : public Solver {
+ public:
+    // Constructor/Destructor:
+    //
+    SimpSolver();
+    ~SimpSolver();
+
+    // Problem specification:
+    //
+    Var     newVar    (bool polarity = true, bool dvar = true);
+    bool    addClause (vec<Lit>& ps);
+
+    // Variable mode:
+    // 
+    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+
+    // 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. 
+
+    // Generate a (possibly simplified) DIMACS file:
+    //
+    void    toDimacs  (const char* file);
+
+    // 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 :)
+
+    // Statistics:
+    //
+    int     merges;
+    int     asymm_lits;
+    int     remembered_clauses;
+
+// protected:
+  public:
+
+    // 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); } };
+
+
+    // Solver state:
+    //
+    int                 elimorder;
+    bool                use_simplification;
+    vec<ElimData>       elimtable;
+    vec<char>           touched;
+    vec<vec<Clause*> >  occurs;
+    vec<int>            n_occ;
+    Heap<ElimLt>        elim_heap;
+    Queue<Clause*>      subsumption_queue;
+    vec<char>           frozen;
+    int                 bwdsub_assigns;
+
+    // Temporaries:
+    //
+    Clause*             bwdsub_tmpunit;
+
+    // Main internal methods:
+    //
+    bool          asymm                    (Var v, Clause& c);
+    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          backwardSubsumptionCheck (bool verbose = false);
+    bool          eliminateVar             (Var v, bool fail = false);
+    void          remember                 (Var v);
+    void          extendModel              ();
+    void          verifyModel              ();
+
+    void          removeClause             (Clause& c);
+    bool          strengthenClause         (Clause& c, Lit l);
+    void          cleanUpClauses           ();
+    bool          implied                  (const vec<Lit>& c);
+    void          toDimacs                 (FILE* f, Clause& c);
+    bool          isEliminated             (Var v) const;
+
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+inline void SimpSolver::updateElimHeap(Var v) {
+    if (elimtable[v].order == 0)
+        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::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); }
+
+}/* CVC4::MiniSat namespace */
+}/* CVC4 namespace */
+
+//=================================================================================================
+#endif /* CVC4_MiniSat_SimpSolver_h */