diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-25 10:38:46 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-25 10:38:46 -0700 |
| commit | 1eb4ddfc5c47c16c66bb3e8eb87351470854ceec (patch) | |
| tree | bfe44753267b32a1bb8079e4bea5fb983357433d | |
| parent | 98a3c6c737293216545790af6e95f0504494432c (diff) | |
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 94878f7bc..00ff5315c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1789,9 +1789,10 @@ CRef Solver::updateLemmas() { ( TNode cnf_assertion = lemmas_cnf_assertion[i].first; TNode cnf_def = lemmas_cnf_assertion[i].second; + bool isInput = ProofManager::getCnfProof()->isAssertion(cnf_assertion) && ProofManager::getCnfProof()->getProofRule(cnf_assertion) == RULE_GIVEN; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); + ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, isInput ? INPUT : THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); ); @@ -1806,9 +1807,10 @@ CRef Solver::updateLemmas() { ( Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; + bool isInput = ProofManager::getCnfProof()->isAssertion(cnf_assertion) && ProofManager::getCnfProof()->getProofRule(cnf_assertion) == RULE_GIVEN; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); + ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], isInput ? INPUT : THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); ); |