From: trevor_hansen Date: Tue, 13 Apr 2010 14:18:06 +0000 (+0000) Subject: Remove unsound-minisat as per Vijay's advice. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7521ea6b2ca82d1f7fecb09baea3bec8dfcf9f8f;p=francis%2Fstp.git Remove unsound-minisat as per Vijay's advice. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@669 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 62282e5..fe16bb2 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -35,14 +35,6 @@ ifeq ($(SAT),minisat) SOLVER_INCLUDE = $(TOP)/src/sat/core endif -# OPTION to compile UNSOUND MiniSAT -ifeq ($(SAT),unsound) - UNSOUND = true - CFLAGS_BASE = $(OPTIMIZE) -DUNSOUND - MTL = $(TOP)/src/sat/mtl - SOLVER_INCLUDE = $(TOP)/src/sat/unsound -endif - # OPTION to compile Simplifying MiniSAT ifeq ($(SAT),simp) SIMP = true diff --git a/scripts/Makefile.in b/scripts/Makefile.in index c12ea94..fda3bc3 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -34,9 +34,7 @@ endif ifdef SIMP $(MAKE) -C $(SRC)/sat simp endif -ifdef UNSOUND - $(MAKE) -C $(SRC)/sat unsound -endif + $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main $(AR) rc libstp.a $(SRC)/AST/*.o \ diff --git a/scripts/configure b/scripts/configure index 279b8d0..d3773a3 100755 --- a/scripts/configure +++ b/scripts/configure @@ -21,8 +21,6 @@ while [ $# -gt 0 ]; do echo "Using g++ instead of gcc";; --with-minisat-core) SAT=minisat;; - --with-minisat-unsound) - SAT=unsound;; --with-minisat-simp) SAT=simp;; --with-cryptominisat2) @@ -32,7 +30,6 @@ while [ $# -gt 0 ]; do echo " --with-prefix=/prefix/path Install STP at the specified path" echo " --with-g++=/path/to/g++ Use g++ at the specified path" echo " --with-minisat-core Use core MiniSAT solver (default)" - echo " --with-minisat-unsound Use unsound MiniSAT solver" echo " --with-minisat-simp Use simplifying MiniSAT solver" echo " --with-cryptominisat2 Use CRYPTOMiniSAT 2.x solver" echo "$0 failed" diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 27e1399..269d148 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -6,8 +6,17 @@ * * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ -#ifndef TOPLEVEL_H -#define TOPLEVEL_H +#ifndef USEFULDEFS_H +#define USEFULDEFS_H + +#ifndef CRYPTOMINISAT2 +#ifndef CORE +#ifndef SIMP +#error "A SAT solver must be specified." +#endif +#endif +#endif + #include #include diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index a9ad03f..84aafb2 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -36,10 +36,6 @@ namespace BEEV { MINISAT::SimpSolver NewSolver; #endif -#ifdef UNSOUND - MINISAT::UnsoundSimpSolver NewSolver; -#endif - if(bm->UserFlags.stats_flag) { NewSolver.verbosity = 1; diff --git a/src/sat/Makefile b/src/sat/Makefile index 439fb83..5ac03f3 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -7,11 +7,6 @@ simp: $(MAKE) -C core lib all $(MAKE) -C simp lib all -.PHONY: unsound -unsound: - $(MAKE) -C core lib all - $(MAKE) -C unsound lib all - .PHONY: cryptominisat cryptominisat: $(MAKE) -C cryptominisat lib all @@ -26,7 +21,6 @@ clean: rm -rf *.o *~ libminisat.a $(MAKE) -C core clean $(MAKE) -C simp clean - $(MAKE) -C unsound clean $(MAKE) -C cryptominisat clean $(MAKE) -C cryptominisat2 clean diff --git a/src/sat/sat.h b/src/sat/sat.h index e27a544..7892b9e 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -21,9 +21,4 @@ #include "core/SolverTypes.h" #endif -#ifdef UNSOUND -#include "unsound/UnsoundSimpSolver.h" -#include "core/SolverTypes.h" -#endif - #endif diff --git a/src/sat/unsound/Makefile b/src/sat/unsound/Makefile deleted file mode 100644 index f1d5ecd..0000000 --- a/src/sat/unsound/Makefile +++ /dev/null @@ -1,26 +0,0 @@ -TOP = ../../.. -include $(TOP)/scripts/Makefile.common - -MTL = ../mtl -SOURCES = UnsoundSimpSolver.C ../core/Solver.C -OBJECTS = $(SOURCES:.C=.o) -LIB = libminisat.a -CFLAGS += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c -EXEC = minisat -LFLAGS = -lz - -all: $(LIB) #$(EXEC) -lib: $(LIB) - -$(LIB): $(OBJECTS) - rm -f $@ - ar cq $@ $(OBJECTS) - ranlib $@ - cp $(LIB) ../ - cp $(OBJECTS) ../ - -clean: - rm -f $(OBJECTS) $(LIB) - -.C.o: - $(CC) $(CFLAGS) $< -o $@ diff --git a/src/sat/unsound/UnsoundSimpSolver.C b/src/sat/unsound/UnsoundSimpSolver.C deleted file mode 100644 index 1901ccc..0000000 --- a/src/sat/unsound/UnsoundSimpSolver.C +++ /dev/null @@ -1,797 +0,0 @@ -/************************************************************************************[UnsoundSimpSolver.C] -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 -#include "Sort.h" -#include "UnsoundSimpSolver.h" - - -namespace MINISAT { - -//================================================================================================= -// Constructor/Destructor: - - -UnsoundSimpSolver::UnsoundSimpSolver() : - grow (0) - , asymm_mode (false) - , redundancy_check (false) - , merges (0) - , asymm_lits (0) - , remembered_clauses (0) - , elimorder (1) - , use_simplification (true) - , elim_heap (ElimLt(n_occ)) - , bwdsub_assigns (0) -{ - vec dummy(1,lit_Undef); - bwdsub_tmpunit = Clause_new(dummy); - remove_satisfied = false; -} - - -UnsoundSimpSolver::~UnsoundSimpSolver() -{ - free(bwdsub_tmpunit); - - // NOTE: elimtable.size() might be lower than nVars() at the moment - for (int i = 0; i < elimtable.size(); i++) - for (int j = 0; j < elimtable[i].eliminated.size(); j++) - free(elimtable[i].eliminated[j]); -} - - -Var UnsoundSimpSolver::newVar(bool sign, bool dvar) { - Var v = Solver::newVar(sign, dvar); - - if (use_simplification){ - n_occ .push(0); - n_occ .push(0); - occurs .push(); - frozen .push((char)false); - touched .push(0); - elim_heap.insert(v); - elimtable.push(); - } - return v; } - - - -bool UnsoundSimpSolver::solve(const vec& assumps, bool do_simp, bool turn_off_simp) { - vec extra_frozen; - bool result = true; - - do_simp &= use_simplification; - - //if (do_simp){ - // Assumptions must be temporarily frozen to run variable elimination: - for (int i = 0; i < assumps.size(); i++){ - Var v = var(assumps[i]); - - // If an assumption has been eliminated, remember it. - if (isEliminated(v)) - remember(v); - - if (!frozen[v]){ - // Freeze and store. - setFrozen(v, true); - extra_frozen.push(v); - } } - - result = eliminate(turn_off_simp); - //} - // - - if (result) - result = Solver::solve(assumps); - - if (result) { - extendModel(); - //#ifndef NDEBUG - verifyModel(); - //#endif - } - - if (do_simp) - // Unfreeze the assumptions that were frozen: - for (int i = 0; i < extra_frozen.size(); i++) - setFrozen(extra_frozen[i], false); - - return result; -} - - - -bool UnsoundSimpSolver::addClause(vec& ps) -{ - for (int i = 0; i < ps.size(); i++) - if (isEliminated(var(ps[i]))) - remember(var(ps[i])); - - int nclauses = clauses.size(); - - if (redundancy_check && implied(ps)) - return true; - - if (!Solver::addClause(ps)) - return false; - - if (use_simplification && clauses.size() == nclauses + 1){ - Clause& c = *clauses.last(); - - subsumption_queue.insert(&c); - - for (int i = 0; i < c.size(); i++){ - assert(occurs.size() > var(c[i])); - assert(!find(occurs[var(c[i])], &c)); - - occurs[var(c[i])].push(&c); - n_occ[toInt(c[i])]++; - touched[var(c[i])] = 1; - assert(elimtable[var(c[i])].order == 0); - if (elim_heap.inHeap(var(c[i]))) - elim_heap.increase_(var(c[i])); - } - } - - return true; -} - - -void UnsoundSimpSolver::removeClause(Clause& c) -{ - assert(!c.learnt()); - - if (use_simplification) - for (int i = 0; i < c.size(); i++){ - n_occ[toInt(c[i])]--; - updateElimHeap(var(c[i])); - } - - detachClause(c); - c.mark(1); -} - - -bool UnsoundSimpSolver::strengthenClause(Clause& c, Lit l) -{ - assert(decisionLevel() == 0); - assert(c.mark() == 0); - assert(!c.learnt()); - assert(find(watches[toInt(~c[0])], &c)); - assert(find(watches[toInt(~c[1])], &c)); - - // FIX: this is too inefficient but would be nice to have (properly implemented) - // if (!find(subsumption_queue, &c)) - subsumption_queue.insert(&c); - - // If l is watched, delete it from watcher list and watch a new literal - if (c[0] == l || c[1] == l){ - Lit other = c[0] == l ? c[1] : c[0]; - if (c.size() == 2){ - removeClause(c); - c.strengthen(l); - }else{ - c.strengthen(l); - remove(watches[toInt(~l)], &c); - - // Add a watch for the correct literal - watches[toInt(~(c[1] == other ? c[0] : c[1]))].push(&c); - - // !! this version assumes that remove does not change the order !! - //watches[toInt(~c[1])].push(&c); - clauses_literals -= 1; - } - } - else{ - c.strengthen(l); - clauses_literals -= 1; - } - - // if subsumption-indexing is active perform the necessary updates - if (use_simplification){ - remove(occurs[var(l)], &c); - n_occ[toInt(l)]--; - updateElimHeap(var(l)); - } - - return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true; -} - - -// Returns FALSE if clause is always satisfied ('out_clause' should not be used). -bool UnsoundSimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) -{ - merges++; - out_clause.clear(); - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) - if (ps[j] == ~qs[i]) - return false; - else - goto next; - out_clause.push(qs[i]); - } - next:; - } - - for (int i = 0; i < ps.size(); i++) - if (var(ps[i]) != v) - out_clause.push(ps[i]); - - return true; -} - - -// Returns FALSE if clause is always satisfied. -bool UnsoundSimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v) -{ - merges++; - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - const Lit* __ps = (const Lit*)ps; - const Lit* __qs = (const Lit*)qs; - - for (int i = 0; i < qs.size(); i++){ - if (var(__qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) - if (__ps[j] == ~__qs[i]) - return false; - else - goto next; - } - next:; - } - - return true; -} - - -void UnsoundSimpSolver::gatherTouchedClauses() -{ - //fprintf(stderr, "Gathering clauses for backwards subsumption\n"); - int ntouched = 0; - for (int i = 0; i < touched.size(); i++) - if (touched[i]){ - const vec& cs = getOccurs(i); - ntouched++; - for (int j = 0; j < cs.size(); j++) - if (cs[j]->mark() == 0){ - subsumption_queue.insert(cs[j]); - cs[j]->mark(2); - } - touched[i] = 0; - } - - //fprintf(stderr, "Touched variables %d of %d yields %d clauses to - //check\n", ntouched, touched.size(), clauses.size()); - for (int i = 0; i < subsumption_queue.size(); i++) - subsumption_queue[i]->mark(0); -} - - -bool UnsoundSimpSolver::implied(const vec& c) -{ - assert(decisionLevel() == 0); - - trail_lim.push(trail.size()); - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True){ - cancelUntil(0); - return false; - }else if (value(c[i]) != l_False){ - assert(value(c[i]) == l_Undef); - uncheckedEnqueue(~c[i]); - } - - bool result = propagate() != NULL; - cancelUntil(0); - return result; -} - - -// Backward subsumption + backward subsumption resolution -bool UnsoundSimpSolver::backwardSubsumptionCheck(bool verbose) -{ - int cnt = 0; - int subsumed = 0; - int deleted_literals = 0; - assert(decisionLevel() == 0); - - while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){ - - // Check top-level assignments by creating a dummy clause and placing it in the queue: - if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){ - Lit l = trail[bwdsub_assigns++]; - (*bwdsub_tmpunit)[0] = l; - bwdsub_tmpunit->calcAbstraction(); - assert(bwdsub_tmpunit->mark() == 0); - subsumption_queue.insert(bwdsub_tmpunit); } - - Clause& c = *subsumption_queue.peek(); subsumption_queue.pop(); - - if (c.mark()) continue; - - if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) - reportf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); - - assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point. - - // Find best variable to scan: - Var best = var(c[0]); - for (int i = 1; i < c.size(); i++) - if (occurs[var(c[i])].size() < occurs[best].size()) - best = var(c[i]); - - // Search all candidates: - vec& _cs = getOccurs(best); - Clause** cs = (Clause**)_cs; - - for (int j = 0; j < _cs.size(); j++) - if (c.mark()) - break; - else if (!cs[j]->mark() && cs[j] != &c){ - Lit l = c.subsumes(*cs[j]); - - if (l == lit_Undef) - subsumed++, removeClause(*cs[j]); - else if (l != lit_Error){ - deleted_literals++; - - if (!strengthenClause(*cs[j], ~l)) - return false; - - // Did current candidate get deleted from cs? Then check candidate at index j again: - if (var(l) == best) - j--; - } - } - } - - return true; -} - - -bool UnsoundSimpSolver::asymm(Var v, Clause& c) -{ - assert(decisionLevel() == 0); - - if (c.mark() || satisfied(c)) return true; - - trail_lim.push(trail.size()); - Lit l = lit_Undef; - for (int i = 0; i < c.size(); i++) - if (var(c[i]) != v && value(c[i]) != l_False) - uncheckedEnqueue(~c[i]); - else - l = c[i]; - - if (propagate() != NULL){ - cancelUntil(0); - asymm_lits++; - if (!strengthenClause(c, l)) - return false; - }else - cancelUntil(0); - - return true; -} - - -bool UnsoundSimpSolver::asymmVar(Var v) -{ - assert(!frozen[v]); - assert(use_simplification); - - vec pos, neg; - const vec& cls = getOccurs(v); - - if (value(v) != l_Undef || cls.size() == 0) - return true; - - for (int i = 0; i < cls.size(); i++) - if (!asymm(v, *cls[i])) - return false; - - return backwardSubsumptionCheck(); -} - - -void UnsoundSimpSolver::verifyModel() -{ - bool failed = false; - int cnt = 0; - // NOTE: elimtable.size() might be lower than nVars() at the moment - for (int i = 0; i < elimtable.size(); i++) - if (elimtable[i].order > 0) - for (int j = 0; j < elimtable[i].eliminated.size(); j++){ - cnt++; - Clause& c = *elimtable[i].eliminated[j]; - for (int k = 0; k < c.size(); k++) - if (modelValue(c[k]) == l_True) - goto next; - - reportf("unsatisfied clause: "); - printClause(*elimtable[i].eliminated[j]); - reportf("\n"); - failed = true; - next:; - } - - assert(!failed); - reportf("Verified %d eliminated clauses.\n", cnt); -} - - -bool UnsoundSimpSolver::eliminateVar(Var v, bool fail, bool stop_unsoundness) -{ - if (!fail && asymm_mode && !asymmVar(v)) return false; - - const vec& cls = getOccurs(v); - -// if (value(v) != l_Undef || cls.size() == 0) return true; - if (value(v) != l_Undef) return true; - - // Split the occurrences into positive and negative: - vec pos, neg; - for (int i = 0; i < cls.size(); i++) - (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]); - - // Check if number of clauses decreases: - int cnt = 0; - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow) - return true; - - // Delete and store old clauses: - setDecisionVar(v, false); - elimtable[v].order = elimorder++; - assert(elimtable[v].eliminated.size() == 0); - for (int i = 0; i < cls.size(); i++){ - elimtable[v].eliminated.push(Clause_new(*cls[i])); - removeClause(*cls[i]); } - - // Produce clauses in cross product: - int top = clauses.size(); - vec resolvent; - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent)) - return false; - - - if(!stop_unsoundness) - { - //abductive logic - vec resolvedClauses; - for (int i = 0; i < pos.size(); i++) { - for (int j = 0; j < pos.size(); j++) { - if(i == j) - continue; - abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true); - if(!addClause(resolvedClauses)) - return false; - } - } - //} - - resolvedClauses.clear(); - for (int i = 0; i < neg.size(); i++) { - for (int j = 0; j < neg.size(); j++) { - if(i == j) - continue; - abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true); - if(!addClause(resolvedClauses)) - return false; - } - } - } - - // DEBUG: For checking that a clause set is saturated with respect - // to variable elimination. If the clause set is expected - // to be saturated at this point, this constitutes an - // error. - if (fail){ - reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); - reportf("previous clauses:\n"); - for (int i = 0; i < cls.size(); i++){ - printClause(*cls[i]); reportf("\n"); } - reportf("new clauses:\n"); - for (int i = top; i < clauses.size(); i++){ - printClause(*clauses[i]); reportf("\n"); } - assert(0); } - - return backwardSubsumptionCheck(); -} - - -void UnsoundSimpSolver::remember(Var v) -{ - assert(decisionLevel() == 0); - assert(isEliminated(v)); - - vec clause; - - // Re-activate variable: - elimtable[v].order = 0; - setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now. - - if (use_simplification) - updateElimHeap(v); - - // Reintroduce all old clauses which may implicitly remember other clauses: - for (int i = 0; i < elimtable[v].eliminated.size(); i++){ - Clause& c = *elimtable[v].eliminated[i]; - clause.clear(); - for (int j = 0; j < c.size(); j++) - clause.push(c[j]); - - remembered_clauses++; - check(addClause(clause)); - free(&c); - } - - elimtable[v].eliminated.clear(); -} - - -void UnsoundSimpSolver::extendModel() -{ - vec vs; - - // NOTE: elimtable.size() might be lower than nVars() at the moment - for (int v = 0; v < elimtable.size(); v++) - if (elimtable[v].order > 0) - vs.push(v); - - sort(vs, ElimOrderLt(elimtable)); - - for (int i = 0; i < vs.size(); i++){ - Var v = vs[i]; - Lit l = lit_Undef; - - for (int j = 0; j < elimtable[v].eliminated.size(); j++){ - Clause& c = *elimtable[v].eliminated[j]; - - for (int k = 0; k < c.size(); k++) - if (var(c[k]) == v) - l = c[k]; - else if (modelValue(c[k]) != l_False) - goto next; - - assert(l != lit_Undef); - model[v] = lbool(!sign(l)); - break; - - next:; - } - - if (model[v] == l_Undef) - model[v] = l_True; - } -} - - -bool UnsoundSimpSolver::eliminate(bool turn_off_elim) -{ - if (!ok || !use_simplification) - return ok; - - // Main simplification loop: - //assert(subsumption_queue.size() == 0); - //gatherTouchedClauses(); - while (subsumption_queue.size() > 0 || elim_heap.size() > 0){ - - //fprintf(stderr, "subsumption phase: (%d)\n", subsumption_queue.size()); - if (!backwardSubsumptionCheck(true)) - return false; - - //fprintf(stderr, "elimination phase:\n (%d)", elim_heap.size()); - for (int cnt = 0; !elim_heap.empty(); cnt++){ - bool stop_unsoundness = true; - if(cnt > log(nClauses())) { - stop_unsoundness = false; - //return true; - } - - Var elim = elim_heap.removeMin(); - - if (verbosity >= 2 && cnt % 100 == 0) - reportf("elimination left: %10d\r", elim_heap.size()); - - if (!frozen[elim] && !eliminateVar(elim, false, stop_unsoundness)) - return false; - } - - assert(subsumption_queue.size() == 0); - gatherTouchedClauses(); - } - - // Cleanup: - cleanUpClauses(); - order_heap.filter(VarFilter(*this)); - -#ifdef INVARIANTS - // Check that no more subsumption is possible: - reportf("Checking that no more subsumption is possible\n"); - for (int i = 0; i < clauses.size(); i++){ - if (i % 1000 == 0) - reportf("left %10d\r", clauses.size() - i); - - assert(clauses[i]->mark() == 0); - for (int j = 0; j < i; j++) - assert(clauses[i]->subsumes(*clauses[j]) == lit_Error); - } - reportf("done.\n"); - - // Check that no more elimination is possible: - reportf("Checking that no more elimination is possible\n"); - for (int i = 0; i < nVars(); i++) - if (!frozen[i]) eliminateVar(i, true, true); - reportf("done.\n"); - checkLiteralCount(); -#endif - - // If no more simplification is needed, free all simplification-related data structures: - if (turn_off_elim){ - use_simplification = false; - touched.clear(true); - occurs.clear(true); - n_occ.clear(true); - subsumption_queue.clear(true); - elim_heap.clear(true); - remove_satisfied = true; - } - - - return true; -} - - -void UnsoundSimpSolver::cleanUpClauses() -{ - int i , j; - vec dirty; - for (i = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1){ - Clause& c = *clauses[i]; - for (int k = 0; k < c.size(); k++) - if (!seen[var(c[k])]){ - seen[var(c[k])] = 1; - dirty.push(var(c[k])); - } } - - for (i = 0; i < dirty.size(); i++){ - cleanOcc(dirty[i]); - seen[dirty[i]] = 0; } - - for (i = j = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1) - free(clauses[i]); - else - clauses[j++] = clauses[i]; - clauses.shrink(i - j); -} - - -//================================================================================================= -// Convert to DIMACS: - - -void UnsoundSimpSolver::toDimacs(FILE* f, Clause& c) -{ - if (satisfied(c)) return; - - for (int i = 0; i < c.size(); i++) - if (value(c[i]) != l_False) - fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", var(c[i])+1); - fprintf(f, "0\n"); -} - - -void UnsoundSimpSolver::toDimacs(const char* file) -{ - assert(decisionLevel() == 0); - FILE* f = fopen(file, "wr"); - if (f != NULL){ - - // Cannot use removeClauses here because it is not safe - // to deallocate them at this point. Could be improved. - int cnt = 0; - for (int i = 0; i < clauses.size(); i++) - if (!satisfied(*clauses[i])) - cnt++; - - fprintf(f, "p cnf %d %d\n", nVars(), cnt); - - for (int i = 0; i < clauses.size(); i++) - toDimacs(f, *clauses[i]); - - fprintf(stderr, "Wrote %d clauses...\n", clauses.size()); - }else - fprintf(stderr, "could not open file %s\n", file); -} - - -// Returns FALSE if clause is always satisfied ('out_clause' should not be used). -bool UnsoundSimpSolver::abductive_merge(const Clause& _ps, - const Clause& _qs, - Var v, - vec& out_clause, bool s) { - merges++; - out_clause.clear(); - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v) - out_clause.push(qs[i]); - } - - for (int j = 0; j < ps.size(); j++) { - if(var(ps[j]) != v) - out_clause.push(ps[j]); - } - - return true; -} //end of abductive_merge() - -// Returns FALSE if clause is always satisfied ('out_clause' should not be used). -bool UnsoundSimpSolver::abductive_neg_merge(const Clause& _ps, - const Clause& _qs, - Var v, vec& out_clause, bool s) { - merges++; - out_clause.clear(); - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - - //if(s) { - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v) - out_clause.push(qs[i]); - } - //} - //else { - for (int j = 0; j < ps.size(); j++) { - if(var(ps[j]) != v) - out_clause.push(ps[j]); - } - //} - return true; -} //end of abductive_merge() -}; diff --git a/src/sat/unsound/UnsoundSimpSolver.h b/src/sat/unsound/UnsoundSimpSolver.h deleted file mode 100644 index 0d58019..0000000 --- a/src/sat/unsound/UnsoundSimpSolver.h +++ /dev/null @@ -1,176 +0,0 @@ -/**************************************************************************** -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 UnsoundSimpSolver_h -#define UnsoundSimpSolver_h - -#include - -#include "../mtl/Queue.h" -#include "../core/Solver.h" - - -namespace MINISAT { - -class UnsoundSimpSolver : public Solver { - public: - // Constructor/Destructor: - // - UnsoundSimpSolver(); - ~UnsoundSimpSolver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true); - bool addClause (vec& ps); - - // Variable mode: - // - void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. - - // Solving: - // - bool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - bool solve (bool do_simp = true, bool turn_off_simp = true); - 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 eliminated; - ElimData() : order(0) {} }; - - struct ElimOrderLt { - const vec& elimtable; - ElimOrderLt(const vec& et) : elimtable(et) {} - bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } }; - - struct ElimLt { - const vec& n_occ; - ElimLt(const vec& 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 elimtable; - vec touched; - vec > occurs; - vec n_occ; - Heap elim_heap; - Queue subsumption_queue; - vec 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& getOccurs (Var x); - void gatherTouchedClauses (); - bool merge (const Clause& _ps, const Clause& _qs, Var v, vec& out_clause); - bool merge (const Clause& _ps, const Clause& _qs, Var v); - bool abductive_merge (const Clause& _ps, - const Clause& _qs, - Var v, vec& out_clauses, bool s=true); - bool abductive_neg_merge (const Clause& _ps, - const Clause& _qs, - Var v, vec& out_clause, bool s=true); - - bool backwardSubsumptionCheck (bool verbose = false); - bool eliminateVar (Var v, bool fail = false, - bool stop_unsoundness=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& c); - void toDimacs (FILE* f, Clause& c); - bool isEliminated (Var v) const; - -}; - - -//================================================================================================= -// Implementation of inline methods: - -inline void UnsoundSimpSolver::updateElimHeap(Var v) { - if (elimtable[v].order == 0) - elim_heap.update(v); } - -inline void UnsoundSimpSolver::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& UnsoundSimpSolver::getOccurs(Var x) { - cleanOcc(x); return occurs[x]; } - -inline bool UnsoundSimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; } -inline void UnsoundSimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } } -inline bool UnsoundSimpSolver::solve (bool do_simp, bool turn_off_simp) { vec tmp; return solve(tmp, do_simp, turn_off_simp); } - -//================================================================================================= -#endif -};