--- /dev/null
+/************************************************************************************[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 <math.h>
+#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<Lit> 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<Lit>& assumps, bool do_simp, bool turn_off_simp) {
+ vec<Var> 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<Lit>& 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<Lit>& 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<Clause*>& 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<Lit>& 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<Clause*>& _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<Clause*> pos, neg;
+ const vec<Clause*>& 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<Clause*>& 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<Clause*> 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<Lit> 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<Lit > 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<Lit> 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<Var> 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<Var> 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<Lit>& 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<Lit>& 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()
+};
--- /dev/null
+/****************************************************************************
+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 <cstdio>
+
+#include "Queue.h"
+#include "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<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 = 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<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 abductive_merge (const Clause& _ps,
+ const Clause& _qs,
+ Var v, vec<Lit >& out_clauses, bool s=true);
+ bool abductive_neg_merge (const Clause& _ps,
+ const Clause& _qs,
+ Var v, vec<Lit>& 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<Lit>& 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<Clause*>& 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<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
+
+//=================================================================================================
+#endif
+};
projects / francis / stp.git / commitdiff