From: Tim King Date: Wed, 11 Oct 2017 23:01:32 +0000 (-0700) Subject: Cleaning up ProofArray class. (#1208) X-Git-Tag: cvc5-1.0.0~5563 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=435d9f0118914c634defa509e6c54a57c7b954ce;p=cvc5.git Cleaning up ProofArray class. (#1208) --- diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index e5b7e64e5..fab9a896d 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -16,14 +16,49 @@ **/ #include "proof/array_proof.h" + +#include + #include "proof/proof_manager.h" #include "proof/simplify_boolean_node.h" #include "proof/theory_proof.h" #include "theory/arrays/theory_arrays.h" -#include namespace CVC4 { +namespace { + +class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter { + public: + ArrayProofPrinter(unsigned row, unsigned row1, unsigned ext) + : d_row(row), d_row1(row1), d_ext(ext) {} + + std::string printTag(unsigned tag) override; + + private: + const unsigned d_row; + const unsigned d_row1; + const unsigned d_ext; +}; // class ArrayProofPrinter + +std::string ArrayProofPrinter::printTag(unsigned tag) { + if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence"; + if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality"; + if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity"; + if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants"; + if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity"; + + if (tag == d_row) return "Read Over Write"; + if (tag == d_row1) return "Read Over Write (1)"; + if (tag == d_ext) return "Extensionality"; + + std::ostringstream result; + result << tag; + return result.str(); +} + +} // namespace + inline static Node eqNode(TNode n1, TNode n2) { return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } @@ -80,32 +115,9 @@ inline static bool match(TNode n1, TNode n2) { return true; } -void ProofArray::setRowMergeTag(unsigned tag) { - d_reasonRow = tag; - d_proofPrinter.d_row = tag; -} - -void ProofArray::setRow1MergeTag(unsigned tag) { - d_reasonRow1 = tag; - d_proofPrinter.d_row1 = tag; -} - -void ProofArray::setExtMergeTag(unsigned tag) { - d_reasonExt = tag; - d_proofPrinter.d_ext = tag; -} - -unsigned ProofArray::getRowMergeTag() const { - return d_reasonRow; -} - -unsigned ProofArray::getRow1MergeTag() const { - return d_reasonRow1; -} - -unsigned ProofArray::getExtMergeTag() const { - return d_reasonExt; -} +ProofArray::ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1, + unsigned ext) + : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {} void ProofArray::toStream(std::ostream& out) { ProofLetMap map; @@ -118,11 +130,13 @@ void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) { Debug("pf::array") << "; Print Array proof done!" << std::endl; } -void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map) { +void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, + theory::eq::EqProof* pf, const ProofLetMap& map) { Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; - pf->debug_print("pf::array", 0, &d_proofPrinter); + ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); + pf->debug_print("pf::array", 0, &proofPrinter); Debug("pf::array") << std::endl; - toStreamRecLFSC( out, tp, pf, 0, map ); + toStreamRecLFSC(out, tp, pf, 0, map); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; } @@ -133,7 +147,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, const ProofLetMap& map) { Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::array", 0, &d_proofPrinter); + ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); + pf->debug_print("pf::array", 0, &proofPrinter); Debug("pf::array") << std::endl; if(tb == 0) { @@ -172,8 +187,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf->d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter); - congruenceClosures.push_back(pf->d_children[i+count]); + pf->d_children[i + count]->debug_print("pf::array", 0, &proofPrinter); + congruenceClosures.push_back(pf->d_children[i + count]); } Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -319,7 +334,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd", 0, &d_proofPrinter); + pf->debug_print("mgd", 0, &proofPrinter); std::stack stk; for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl; @@ -351,7 +366,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; - pf2->debug_print("mgd", 0, &d_proofPrinter); + pf2->debug_print("mgd", 0, &proofPrinter); // Temp Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl; Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl; @@ -368,7 +383,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "SIDE IS 1\n"; if(!match(pf2->d_node, n1[1])) { Debug("mgd") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter); + pf2->d_children[0]->debug_print("mgd", 0, &proofPrinter); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -605,7 +620,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf->d_children.size() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; - pf->debug_print("mgd", 0, &d_proofPrinter); + pf->debug_print("mgd", 0, &proofPrinter); Debug("mgd") << "\n"; pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); @@ -832,7 +847,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("mgdx", 0, &d_proofPrinter); + pf->debug_print("mgdx", 0, &proofPrinter); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 9a2eef9e7..f40f13ea6 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -29,65 +29,33 @@ namespace CVC4 { -//proof object outputted by TheoryARRAY +// Proof object outputted by TheoryARRAY. class ProofArray : public Proof { -private: - class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter { - public: - ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) { - } - - std::string printTag(unsigned tag) { - if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence"; - if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality"; - if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity"; - if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants"; - if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity"; - - if (tag == d_row) return "Read Over Write"; - if (tag == d_row1) return "Read Over Write (1)"; - if (tag == d_ext) return "Extensionality"; - - std::ostringstream result; - result << tag; - return result.str(); - } - - unsigned d_row; - unsigned d_row1; - unsigned d_ext; - }; + public: + ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1, + unsigned ext); + void registerSkolem(Node equality, Node skolem); + + void toStream(std::ostream& out); + void toStream(std::ostream& out, const ProofLetMap& map); + void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, + const ProofLetMap& map); + + private: Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - theory::eq::EqProof* pf, - unsigned tb, + theory::eq::EqProof* pf, unsigned tb, const ProofLetMap& map); + // it is simply an equality engine proof + theory::eq::EqProof* d_proof; + /** Merge tag for ROW applications */ unsigned d_reasonRow; /** Merge tag for ROW1 applications */ unsigned d_reasonRow1; /** Merge tag for EXT applications */ unsigned d_reasonExt; - - ArrayProofPrinter d_proofPrinter; -public: - ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} - //it is simply an equality engine proof - theory::eq::EqProof *d_proof; - void toStream(std::ostream& out); - void toStream(std::ostream& out, const ProofLetMap& map); - void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map); - - void registerSkolem(Node equality, Node skolem); - - void setRowMergeTag(unsigned tag); - void setRow1MergeTag(unsigned tag); - void setExtMergeTag(unsigned tag); - - unsigned getRowMergeTag() const; - unsigned getRow1MergeTag() const; - unsigned getExtMergeTag() const; }; namespace theory { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2f5a9a14f..a17f506de 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2247,10 +2247,8 @@ void TheoryArrays::conflict(TNode a, TNode b) { if (d_proofsEnabled) { proof->debug_print("pf::array"); - proof_array = new ProofArray( proof ); - proof_array->setRowMergeTag(d_reasonRow); - proof_array->setRow1MergeTag(d_reasonRow1); - proof_array->setExtMergeTag(d_reasonExt); + proof_array = new ProofArray(proof, /*row=*/d_reasonRow, + /*row1=*/d_reasonRow1, /*ext=*/d_reasonExt); } d_out->conflict(d_conflictNode, proof_array);