diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/prop/minisat/core | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/prop/minisat/core')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 74 |
1 files changed, 37 insertions, 37 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b13448bb2..411b89514 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -230,7 +230,7 @@ CRef Solver::reason(Var x) { proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); vec<Lit> explanation; - MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + MinisatSatSolver::toMinisatClause(explanation_cl, explanation); // Sort the literals by trail index level lemma_lt lt(*this); @@ -603,20 +603,20 @@ Lit Solver::pickBranchLit() /*_________________________________________________________________________________________________ | | analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] -| +| | Description: | Analyze conflict and produce a reason clause. -| +| | Pre-conditions: | * 'out_learnt' is assumed to be cleared. | * Current decision level must be greater than root level. -| +| | Post-conditions: | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. -| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the +| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the | rest of literals. There may be others from the same level though. | * returns the maximal level of the resolved clauses -| +| |________________________________________________________________________________________________@*/ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) { @@ -662,14 +662,14 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) } } } - + // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; confl = reason(var(p)); seen[var(p)] = 0; pathC--; - + if ( pathC > 0 && confl != CRef_Undef ) { PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); ) } @@ -695,13 +695,13 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt[j++] = out_learnt[i]; } else { PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) - // Literal is redundant, to be safe, mark the level as current assertion level + // Literal is redundant, to be safe, mark the level as current assertion level // TODO: maybe optimize max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i]))); } } } - + }else if (ccmin_mode == 1){ Unreachable(); for (i = j = 1; i < out_learnt.size(); i++){ @@ -787,7 +787,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) /*_________________________________________________________________________________________________ | | analyzeFinal : (p : Lit) -> [void] -| +| | Description: | Specialized analysis procedure to express the final conflict in terms of assumptions. | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and @@ -866,7 +866,7 @@ CRef Solver::propagate(TheoryCheckType type) if (lemmas.size() > 0) { recheck = true; confl = updateLemmas(); - return confl; + return confl; } else { recheck = proxy->theoryNeedCheck(); return confl; @@ -922,7 +922,7 @@ void Solver::propagateTheory() { proxy->theoryPropagate(propagatedLiteralsClause); vec<Lit> propagatedLiterals; - MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); + MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); int oldTrailSize = trail.size(); Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl; @@ -964,11 +964,11 @@ void Solver::theoryCheck(CVC4::theory::Theory::Effort effort) /*_________________________________________________________________________________________________ | | propagateBool : [void] -> [Clause*] -| +| | Description: | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, | otherwise CRef_Undef. -| +| | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ @@ -1038,16 +1038,16 @@ CRef Solver::propagateBool() /*_________________________________________________________________________________________________ | | reduceDB : () -> [void] -| +| | Description: | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | clauses are clauses that are reason to some assignment. Binary clauses are never removed. |________________________________________________________________________________________________@*/ -struct reduceDB_lt { +struct reduceDB_lt { ClauseAllocator& ca; reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} - bool operator () (CRef x, CRef y) { - return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } + bool operator () (CRef x, CRef y) { + return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } }; void Solver::reduceDB() { @@ -1115,7 +1115,7 @@ void Solver::rebuildOrderHeap() /*_________________________________________________________________________________________________ | | simplify : [void] -> [bool] -| +| | Description: | Simplify the clause database according to the current top-level assigment. Currently, the only | thing done here is the removal of satisfied clauses, but more things can be put here. @@ -1147,11 +1147,11 @@ bool Solver::simplify() /*_________________________________________________________________________________________________ | | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] -| +| | Description: -| Search for a model the specified number of conflicts. +| Search for a model the specified number of conflicts. | NOTE! Use negative value for 'nof_conflicts' indicate infinity. -| +| | Output: | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' @@ -1220,9 +1220,9 @@ lbool Solver::search(int nof_conflicts) max_learnts *= learntsize_inc; if (verbosity >= 1) - printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", - (int)conflicts, - (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", + (int)conflicts, + (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); } @@ -1418,7 +1418,7 @@ lbool Solver::solve_() //================================================================================================= // Writing CNF to DIMACS: -// +// // FIXME: this needs to be rewritten completely. static Var mapVar(Var x, vec<Var>& map, Var& max) @@ -1467,7 +1467,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) for (int i = 0; i < clauses_persistent.size(); i++) if (!satisfied(ca[clauses_persistent[i]])) cnt++; - + for (int i = 0; i < clauses_persistent.size(); i++) if (!satisfied(ca[clauses_persistent[i]])){ Clause& c = ca[clauses_persistent[i]]; @@ -1538,11 +1538,11 @@ void Solver::garbageCollect() { // Initialize the next region to a size corresponding to the estimated utilization degree. This // is not precise but should avoid some unnecessary reallocations for the new region: - ClauseAllocator to(ca.size() - ca.wasted()); + ClauseAllocator to(ca.size() - ca.wasted()); relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", + printf("| Garbage collection: %12d bytes => %12d bytes |\n", ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } @@ -1699,7 +1699,7 @@ CRef Solver::updateLemmas() { int backtrack_index = trail.size(); PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size());); - + // Attach all the clauses and enqueue all the propagations for (int i = 0; i < lemmas.size(); ++ i) { @@ -1740,7 +1740,7 @@ CRef Solver::updateLemmas() { ( Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; - + ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); @@ -1785,20 +1785,20 @@ CRef Solver::updateLemmas() { void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy) { - + // FIXME what is this CRef_lazy if (cr == CRef_Lazy) return; - + CRef old = cr; // save the old reference Clause& c = operator[](cr); if (c.reloced()) { cr = c.relocation(); return; } - + cr = to.alloc(c.level(), c, c.removable()); c.relocate(cr); if (proxy) { - proxy->updateCRef(old, cr); + proxy->updateCRef(old, cr); } - // Copy extra data-fields: + // Copy extra data-fields: // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) to[cr].mark(c.mark()); if (to[cr].removable()) to[cr].activity() = c.activity(); |