diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-12-11 18:58:13 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-11 18:58:13 -0300 |
commit | 8d0de294c259e789a149bc5ceb5d6501868e83d0 (patch) | |
tree | d714a7b920fc369bbbe3d37730fc4a6edeedde0e /src/prop/theory_proxy.cpp | |
parent | 49215e6948aba1d6b762e28a7293581e25c2df8c (diff) |
[proof-new] Updating theory proxy to new proof infrastructure (#5653)
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 38 |
1 files changed, 26 insertions, 12 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d0d593f8a..1b9e78d80 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -75,26 +75,40 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - theory::TrustNode texp = d_theoryEngine->getExplanation(lNode); - Node theoryExplanation = texp.getNode(); - + theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); + Node theoryExplanation = tte.getNode(); + if (CVC4::options::proofNew()) + { + d_propEngine->getProofCnfStream()->convertPropagation(tte); + } if (options::unsatCores()) { ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); } - Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; - if (theoryExplanation.getKind() == kind::AND) { - Node::const_iterator it = theoryExplanation.begin(); - Node::const_iterator it_end = theoryExplanation.end(); - explanation.push_back(l); - for (; it != it_end; ++ it) { - explanation.push_back(~d_cnfStream->getLiteral(*it)); + explanation.push_back(l); + if (theoryExplanation.getKind() == kind::AND) + { + for (const Node& n : theoryExplanation) + { + explanation.push_back(~d_cnfStream->getLiteral(n)); } - } else { - explanation.push_back(l); + } + else + { explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); } + if (Trace.isOn("sat-proof")) + { + std::stringstream ss; + ss << "TheoryProxy::explainPropagation: clause for lit is "; + for (unsigned i = 0, size = explanation.size(); i < size; ++i) + { + ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i]) + << "] "; + } + Trace("sat-proof") << ss.str() << "\n"; + } } void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { |