diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-09 13:49:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 15:49:10 -0500 |
| commit | c74e9c8ba946387616345b70d63028896a0022c2 (patch) | |
| tree | a7446c7a7682845073390801b4f4acc498baccce /src | |
| parent | 3740873b8b1ac7e1f2c203b26de6dd1a0ef73f43 (diff) | |
Make registration of unit clauses more robust (#3965)
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
Diffstat (limited to 'src')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 6abaa30c6..80cce599f 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1956,22 +1956,24 @@ CRef Solver::updateLemmas() { clauses_persistent.push(lemma_ref); } attachClause(lemma_ref); - } else { - PROOF - ( - Node cnf_assertion = lemmas_cnf_assertion[j].first; - Node cnf_def = lemmas_cnf_assertion[j].second; - - Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); - ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); - ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); - ); } // If the lemma is propagating enqueue its literal (or set the conflict) if (conflict == CRef_Undef && value(lemma[0]) != l_True) { if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) { + if (PROOF_ON() && lemma.size() == 1) + { + Node cnf_assertion = lemmas_cnf_assertion[j].first; + Node cnf_def = lemmas_cnf_assertion[j].second; + + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) " + << cnf_assertion << value(lemma[0]) << std::endl; + ClauseId id = ProofManager::getSatProof()->registerUnitClause( + lemma[0], THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); + } + if (value(lemma[0]) == l_False) { // We have a conflict if (lemma.size() > 1) { |