diff options
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index aa1fc9587..eda736b8a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -120,7 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const { return find != d_nodeToLiteralMap.end(); } -void TseitinCnfStream::ensureLiteral(TNode n) { +void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // These are not removable and have no proof ID d_removable = false; @@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. - lit = convertAtom(n); + lit = convertAtom(n, noPreregistration); } Assert(hasLiteral(n) && getNode(lit) == n); @@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) { d_cnfProof = proof; } -SatLiteral CnfStream::convertAtom(TNode node) { +SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!hasLiteral(node), "atom already mapped!"); @@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { } else { theoryLiteral = true; canEliminate = false; - preRegister = true; + preRegister = !noPreregistration; } // Make a new literal (variables are not considered theory literals) @@ -258,7 +258,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + + Assert(d_nodeToLiteralMap.contains(node), + "Literal not in the CNF Cache: %s\n", + node.toString().c_str()); + SatLiteral literal = d_nodeToLiteralMap[node]; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; @@ -675,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id, TNode from, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -685,7 +689,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - d_cnfProof->setExplainerTheory(ownerTheory); + if (proofRecipe) { + Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; + proofRecipe->dump("pf::sat"); + d_cnfProof->setProofRecipe(proofRecipe); + } + if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); |