diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.h')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 174 |
1 files changed, 0 insertions, 174 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h deleted file mode 100644 index 3da574f6c..000000000 --- a/src/prop/minisat/simp/SimpSolver.h +++ /dev/null @@ -1,174 +0,0 @@ -/************************************************************************************[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. -**************************************************************************************************/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H -#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H - -#include <cstdio> -#include <cassert> - -#include "../mtl/Queue.h" -#include "../core/Solver.h" - -namespace CVC4 { -namespace prop { - -class SatSolver; - -namespace minisat { - -class SimpSolver : public Solver { - public: - // Constructor/Destructor: - // - SimpSolver(SatSolver* proxy, 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); - - // 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::prop::minisat namespace */ -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ - -//================================================================================================= -#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */ |