diff options
Diffstat (limited to 'src/proof/array_proof.cpp')
-rw-r--r-- | src/proof/array_proof.cpp | 1260 |
1 files changed, 1260 insertions, 0 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp new file mode 100644 index 000000000..764028c6b --- /dev/null +++ b/src/proof/array_proof.cpp @@ -0,0 +1,1260 @@ +/********************* */ +/*! \file uf_proof.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" +#include "proof/array_proof.h" +#include "theory/arrays/theory_arrays.h" +#include <stack> + +namespace CVC4 { + +inline static Node eqNode(TNode n1, TNode n2) { + return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); +} + +// congrence matching term helper +inline static bool match(TNode n1, TNode n2) { + Debug("mgd") << "match " << n1 << " " << n2 << std::endl; + if(ProofManager::currentPM()->hasOp(n1)) { + n1 = ProofManager::currentPM()->lookupOp(n1); + } + if(ProofManager::currentPM()->hasOp(n2)) { + n2 = ProofManager::currentPM()->lookupOp(n2); + } + Debug("mgd") << "+ match " << n1 << " " << n2 << std::endl; + Debug("pf::array") << "+ match: step 1" << std::endl; + if(n1 == n2) { + return true; + } + + if(n1.getType().isFunction() && n2.hasOperator()) { + if(ProofManager::currentPM()->hasOp(n2.getOperator())) { + return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator()); + } else { + return n1 == n2.getOperator(); + } + } + + if(n2.getType().isFunction() && n1.hasOperator()) { + if(ProofManager::currentPM()->hasOp(n1.getOperator())) { + return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator()); + } else { + return n2 == n1.getOperator(); + } + } + + if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) { + if (!((n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_0) || + (n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_1) || + (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::SELECT) || + (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::PARTIAL_SELECT_0) || + (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::SELECT) || + (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::PARTIAL_SELECT_1) + )) { + return false; + } + } + + for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) { + if(n1[i] != n2[i]) { + return false; + } + } + + return true; +} + +void ProofArray::toStream(std::ostream& out) { + Trace("pf::array") << "; Print Array proof..." << std::endl; + //AJR : carry this further? + LetMap map; + toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map); + Debug("pf::array") << "; Print Array proof done!" << std::endl; +} + +void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) { + Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; + pf->debug_print("pf::array"); + Debug("pf::array") << std::endl; + toStreamRecLFSC( out, tp, pf, 0, map ); + Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; +} + +void ProofArray::registerSkolem(Node equality, Node skolem) { + d_nodeToSkolem[equality] = skolem; +} + +Node ProofArray::toStreamRecLFSC(std::ostream& out, + TheoryProof* tp, + theory::eq::EqProof* pf, + unsigned tb, + const LetMap& map) { + + Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; + pf->debug_print("pf::array"); + Debug("pf::array") << std::endl; + + if(tb == 0) { + Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.size() >= 2); + + int neg = -1; + theory::eq::EqProof subTrans; + subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS; + subTrans.d_node = pf->d_node; + + size_t i = 0; + while (i < pf->d_children.size()) { + // Look for the negative clause, with which we will form a contradiction. + if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { + Assert(neg < 0); + neg = i; + ++i; + } + + // Handle congruence closures over equalities. + else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + Debug("pf::array") << "Handling congruence over equalities" << std::endl; + + // Gather the sequence of consecutive congruence closures. + std::vector<const theory::eq::EqProof *> congruenceClosures; + unsigned count; + Debug("pf::array") << "Collecting congruence sequence" << std::endl; + for (count = 0; + i + count < pf->d_children.size() && + pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + 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"); + congruenceClosures.push_back(pf->d_children[i+count]); + } + + Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; + + // Determine if the "target" of the congruence sequence appears right before or right after the sequence. + bool targetAppearsBefore = true; + bool targetAppearsAfter = true; + + if ((i == 0) || (i == 1 && neg == 0)) { + Debug("pf::array") << "Target does not appear before" << std::endl; + targetAppearsBefore = false; + } + + if ((i + count >= pf->d_children.size()) || + (!pf->d_children[i + count]->d_node.isNull() && + pf->d_children[i + count]->d_node.getKind() == kind::NOT)) { + Debug("pf::array") << "Target does not appear after" << std::endl; + targetAppearsAfter = false; + } + + // Assert that we have precisely one target clause. + Assert(targetAppearsBefore != targetAppearsAfter); + + // Begin breaking up the congruences and ordering the equalities correctly. + std::vector<theory::eq::EqProof *> orderedEqualities; + + // Insert target clause first. + if (targetAppearsBefore) { + orderedEqualities.push_back(pf->d_children[i - 1]); + // The target has already been added to subTrans; remove it. + subTrans.d_children.pop_back(); + } else { + orderedEqualities.push_back(pf->d_children[i + count]); + } + + // Start with the congruence closure closest to the target clause, and work our way back/forward. + if (targetAppearsBefore) { + for (unsigned j = 0; j < count; ++j) { + if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); + if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + } + } else { + for (unsigned j = 0; j < count; ++j) { + if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]); + if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]); + } + } + + // Copy the result into the main transitivity proof. + subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + + // Increase i to skip over the children that have been processed. + i += count; + if (targetAppearsAfter) { + ++i; + } + } + + // Else, just copy the child proof as is + else { + subTrans.d_children.push_back(pf->d_children[i]); + ++i; + } + } + Assert(neg >= 0); + + Node n1; + std::stringstream ss, ss2; + //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); + Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; + if(pf->d_children.size() > 2) { + n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); + } else { + n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); + Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + } + + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + Debug("mgdx") << "\nhave proven: " << n1 << std::endl; + Debug("mgdx") << "n2 is " << n2 << std::endl; + Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; + Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; + + if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } + + if (pf->d_children[neg]->d_id == theory::eq::MERGED_ARRAYS_EXT) { + // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. + + // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6 + + out << "(clausify_false (contra _ "; + out << ss.str(); + + toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + + out << " "; + out << ss2.str(); + out << "))"; + + } else { + // The negative node is, e.g., a pure equality + out << "(clausify_false (contra _ "; + + if(n2[0].getKind() == kind::APPLY_UF) { + out << "(trans _ _ _ _ "; + out << "(symm _ _ _ "; + out << ss.str(); + out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; + } else { + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + if(n1[1] == n2[0][0]) { + out << "(symm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } + Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " << + ProofManager::getLitName(n2[0]) << std::endl; + + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + } + } + + return Node(); + } + + switch(pf->d_id) { + case theory::eq::MERGED_THROUGH_CONGRUENCE: { + Debug("mgd") << "\nok, looking at congruence:\n"; + pf->debug_print("mgd"); + std::stack<const theory::eq::EqProof*> stk; + for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + Assert(!pf2->d_node.isNull()); + Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || + pf2->d_node.getKind() == kind::BUILTIN || + pf2->d_node.getKind() == kind::APPLY_UF || + pf2->d_node.getKind() == kind::SELECT || + pf2->d_node.getKind() == kind::PARTIAL_SELECT_0 || + pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 || + pf2->d_node.getKind() == kind::STORE); + + Assert(pf2->d_children.size() == 2); + out << "(cong _ _ _ _ _ _ "; + stk.push(pf2); + } + Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); + NodeBuilder<> b1, b2; + + const theory::eq::EqProof* pf2 = stk.top(); + stk.pop(); + Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); + Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map); + out << " "; + std::stringstream ss; + Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + + + Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; + pf2->debug_print("mgd"); + // 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; + // + Debug("mgd") << "looking at " << pf2->d_node << "\n"; + Debug("mgd") << " " << n1 << "\n"; + Debug("mgd") << " " << n2 << "\n"; + + int side = 0; + if(match(pf2->d_node, n1[0])) { + Debug("mgd") << "SIDE IS 0\n"; + side = 0; + } else { + 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"); + } + Assert(match(pf2->d_node, n1[1])); + side = 1; + } + + if(n1[side].getKind() == kind::APPLY_UF || + n1[side].getKind() == kind::PARTIAL_APPLY_UF || + n1[side].getKind() == kind::SELECT || + n1[side].getKind() == kind::PARTIAL_SELECT_1 || + n1[side].getKind() == kind::STORE) { + if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) { + b1 << kind::PARTIAL_APPLY_UF; + b1 << n1[side].getOperator(); + } else if (n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::PARTIAL_SELECT_1) { + // b1 << n1[side].getKind(); + b1 << kind::SELECT; + } else { + b1 << kind::PARTIAL_APPLY_UF; + b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); + } + b1.append(n1[side].begin(), n1[side].end()); + } + else if (n1[side].getKind() == kind::PARTIAL_SELECT_0) { + b1 << kind::PARTIAL_SELECT_1; + } else { + b1 << n1[side]; + } + + if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || + n1[1-side].getKind() == kind::APPLY_UF || + n1[1-side].getKind() == kind::SELECT || + n1[1-side].getKind() == kind::PARTIAL_SELECT_1 || + n1[1-side].getKind() == kind::STORE) { + if(n1[1-side].getKind() == kind::APPLY_UF || + n1[1-side].getKind() == kind::PARTIAL_APPLY_UF) { + b2 << kind::PARTIAL_APPLY_UF; + b2 << n1[1-side].getOperator(); + } else if (n1[1-side].getKind() == kind::SELECT || n1[1-side].getKind() == kind::PARTIAL_SELECT_1) { + // b2 << n1[1-side].getKind(); + b2 << kind::SELECT; + } else { + b2 << kind::PARTIAL_APPLY_UF; + b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); + } + b2.append(n1[1-side].begin(), n1[1-side].end()); + } else if (n1[1-side].getKind() == kind::PARTIAL_SELECT_0) { + b2 << kind::PARTIAL_SELECT_1; + } else { + b2 << n1[1-side]; + } + Debug("mgd") << "pf2->d_node " << pf2->d_node << std::endl; + Debug("mgd") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl; + Debug("mgd") << "n1 " << n1 << std::endl; + Debug("mgd") << "n2 " << n2 << std::endl; + // These debug prints can cause a problem if we're constructing a SELECT node and it doesn't have enough + // children yet. + // Debug("mgd") << "b1 " << b1 << std::endl; + // Debug("mgd") << "b2 " << b2 << std::endl; + Debug("mgd") << "side " << side << std::endl; + Debug("mgd") << "pf2->d_node's number of children: " << pf2->d_node.getNumChildren() << std::endl; + Debug("mgd") << "pf2->d_node's meta kind: " << pf2->d_node.getMetaKind() << std::endl; + Debug("mgd") << "Is this meta kind considered parameterized? " << (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED) << std::endl; + + if(pf2->d_node[b1.getNumChildren() + + (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) + + (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) - + (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) { + b1 << n2[side]; + b2 << n2[1-side]; + out << ss.str(); + } else { + Assert(pf2->d_node[b1.getNumChildren() + + (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) + + (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) - + (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + b1 << n2[1-side]; + b2 << n2[side]; + out << "(symm _ _ _ " << ss.str() << ")"; + } + + Debug("mgd") << "After first insertion:" << std::endl; + Debug("mgd") << "b1 " << b1 << std::endl; + Debug("mgd") << "b2 " << b2 << std::endl; + + out << ")"; + while(!stk.empty()) { + + Debug("mgd") << "\nMORE TO DO\n"; + + pf2 = stk.top(); + stk.pop(); + Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); + out << " "; + ss.str(""); + n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + + Debug("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n"; + Debug("mgd") << "looking at " << pf2->d_node << "\n"; + Debug("mgd") << " " << n1 << "\n"; + Debug("mgd") << " " << n2 << "\n"; + Debug("mgd") << " " << b1 << "\n"; + Debug("mgd") << " " << b2 << "\n"; + if(pf2->d_node[b1.getNumChildren()] == n2[side]) { + b1 << n2[side]; + b2 << n2[1-side]; + out << ss.str(); + } else { + Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]); + b1 << n2[1-side]; + b2 << n2[side]; + out << "(symm _ _ _ " << ss.str() << ")"; + } + out << ")"; + } + n1 = b1; + n2 = b2; + + Debug("mgd") << "at end assert!" << std::endl + << "pf2->d_node = " << pf2->d_node << std::endl + << "n1 (assigned from b1) = " << n1 << std::endl + << "n2 (assigned from b2) = " << n2 << std::endl; + + if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) { + Assert(n1 == pf2->d_node); + } + + Debug("mgd") << "n1.getOperator().getType().getNumChildren() = " + << n1.getOperator().getType().getNumChildren() << std::endl; + Debug("mgd") << "n1.getNumChildren() + 1 = " + << n1.getNumChildren() + 1 << std::endl; + + Assert(!((n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2))); + if (n1.getKind() == kind::PARTIAL_SELECT_1 && n1.getNumChildren() == 2) { + Debug("mgd") << "Finished a SELECT. Updating.." << std::endl; + b1.clear(kind::SELECT); + b1.append(n1.begin(), n1.end()); + n1 = b1; + Debug("mgd") << "New n1: " << n1 << std::endl; + // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b1.clear(kind::PARTIAL_SELECT_1); + // b1.append(n1.begin(), n1.end()); + // n1 = b1; + // Debug("mgd") << "New n1: " << n1 << std::endl; + // } else + } else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) { + if(ProofManager::currentPM()->hasOp(n1.getOperator())) { + b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); + } else { + b1.clear(kind::APPLY_UF); + b1 << n1.getOperator(); + } + b1.append(n1.begin(), n1.end()); + n1 = b1; + Debug("mgd") << "at[2] end assert, got " << pf2->d_node << " and " << n1 << std::endl; + if(pf2->d_node.getKind() == kind::APPLY_UF) { + Assert(n1 == pf2->d_node); + } + } + + Debug("mgd") << "n2.getOperator().getType().getNumChildren() = " + << n2.getOperator().getType().getNumChildren() << std::endl; + Debug("mgd") << "n2.getNumChildren() + 1 = " + << n2.getNumChildren() + 1 << std::endl; + + Assert(!((n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2))); + if (n2.getKind() == kind::PARTIAL_SELECT_1 && n2.getNumChildren() == 2) { + Debug("mgd") << "Finished a SELECT. Updating.." << std::endl; + b2.clear(kind::SELECT); + b2.append(n2.begin(), n2.end()); + n2 = b2; + Debug("mgd") << "New n2: " << n2 << std::endl; + // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b2.clear(kind::PARTIAL_SELECT_1); + // b2.append(n2.begin(), n2.end()); + // n2 = b2; + // Debug("mgd") << "New n2: " << n2 << std::endl; + // } else + } else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) { + if(ProofManager::currentPM()->hasOp(n2.getOperator())) { + b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); + } else { + b2.clear(kind::APPLY_UF); + b2 << n2.getOperator(); + } + b2.append(n2.begin(), n2.end()); + n2 = b2; + } + Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); + + Debug("mgdx") << "\ncong proved: " << n << "\n"; + return n; + } + + case theory::eq::MERGED_THROUGH_REFLEXIVITY: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + out << "(refl _ "; + tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); + out << ")"; + return eqNode(pf->d_node, pf->d_node); + + case theory::eq::MERGED_THROUGH_EQUALITY: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " << + ProofManager::getLitName(pf->d_node.negate()) << std::endl; + out << ProofManager::getLitName(pf->d_node.negate()); + return pf->d_node; + + case theory::eq::MERGED_THROUGH_TRANS: { + bool firstNeg = false; + bool secondNeg = false; + + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.size() >= 2); + std::stringstream ss; + Debug("mgd") << "\ndoing trans proof[[\n"; + pf->debug_print("mgd"); + Debug("mgd") << "\n"; + Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; + if(tb == 1) { + Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; + } + + bool identicalEqualities = false; + bool evenLengthSequence; + Node nodeAfterEqualitySequence; + + std::map<size_t, Node> childToStream; + + for(size_t i = 1; i < pf->d_children.size(); ++i) { + std::stringstream ss1(ss.str()), ss2; + ss.str(""); + + // It is possible that we've already converted the i'th child to stream. If so, + // use previously stored result. Otherwise, convert and store. + Node n2; + if (childToStream.find(i) != childToStream.end()) + n2 = childToStream[i]; + else { + n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + childToStream[i] = n2; + } + + Debug("mgd") << "\ndoing trans proof, got (first) n2 " << n2 << "\n"; + + // The following branch is dedicated to handling sequences of identical equalities, + // i.e. trans[ a=b, a=b, a=b ]. + // + // There are two cases: + // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality, + // i.e. a=b. + // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this, + // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs + // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, + // and use it to determine which option we need. + if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { + // We are in a sequence of identical equalities + + Debug("pf::array") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + + if (!identicalEqualities) { + // The sequence of identical equalities has started just now + identicalEqualities = true; + + Debug("pf::array") << "The sequence is just beginning. Determining length..." << std::endl; + + // Determine whether the length of this sequence is odd or even. + evenLengthSequence = true; + bool sequenceOver = false; + size_t j = i + 1; + + while (j < pf->d_children.size() && !sequenceOver) { + std::stringstream dontCare; + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + + if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || + ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { + evenLengthSequence = !evenLengthSequence; + } else { + sequenceOver = true; + } + + ++j; + } + + if (evenLengthSequence) { + // If the length is even, we need to apply transitivity for the "correct" hand of the equality. + + Debug("pf::array") << "Equality sequence of even length" << std::endl; + Debug("pf::array") << "n1 is: " << n1 << std::endl; + Debug("pf::array") << "n2 is: " << n2 << std::endl; + Debug("pf::array") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence << std::endl; + + ss << "(trans _ _ _ _ "; + + // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us. + if (!sequenceOver) { + if (match(n1[0], pf->d_node[0])) { + n1 = eqNode(n1[0], n1[0]); + ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; + } else if (match(n1[1], pf->d_node[1])) { + n1 = eqNode(n1[1], n1[1]); + ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); + } else { + Debug("pf::array") << "Error: identical equalities over, but hands don't match what we're proving." + << std::endl; + Assert(false); + } + } else { + // We have a "next node". Use it to guide us. + if (nodeAfterEqualitySequence.getKind() == kind::NOT) { + nodeAfterEqualitySequence = nodeAfterEqualitySequence[0]; + } + + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || + nodeAfterEqualitySequence.getKind() == kind::IFF); + + if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { + + // Eliminate n1[1] + ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; + n1 = eqNode(n1[0], n1[0]); + + } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) { + + // Eliminate n1[0] + ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); + n1 = eqNode(n1[1], n1[1]); + + } else { + Debug("pf::array") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; + Assert(false); + } + } + + ss << ")"; + + } else { + Debug("pf::array") << "Equality sequence length is odd!" << std::endl; + ss.str(ss1.str()); + } + + Debug("pf::array") << "Have proven: " << n1 << std::endl; + } else { + ss.str(ss1.str()); + } + + // Ignore the redundancy. + continue; + } + } + + if (identicalEqualities) { + // We were in a sequence of identical equalities, but it has now ended. Resume normal operation. + identicalEqualities = false; + } + + Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; + if(tb == 1) { + Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; + Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + + if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { + Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; + Debug("mgdx") << n1[0].getId() << " " << n1[0] << "\n"; + Debug("mgdx") << n1[1].getId() << " " << n1[1] << "\n"; + Debug("mgdx") << n2[0].getId() << " " << n2[0] << "\n"; + Debug("mgdx") << n2[1].getId() << " " << n2[1] << "\n"; + Debug("mgdx") << (n1[0] == n2[0]) << "\n"; + Debug("mgdx") << (n1[1] == n2[1]) << "\n"; + Debug("mgdx") << (n1[0] == n2[1]) << "\n"; + Debug("mgdx") << (n1[1] == n2[0]) << "\n"; + } + } + + // We can hadnle one of the equalities being negative, but not both + Assert((n1.getKind() != kind::NOT) || (n2.getKind() != kind::NOT)); + + firstNeg = false; + secondNeg = false; + + if (n1.getKind() == kind::NOT) { + Debug("mgdx") << "n1 is negative" << std::endl; + Debug("pf::array") << "n1 = " << n1 << ", n2 = " << n2 << std::endl; + firstNeg = true; + ss << "(negtrans1 _ _ _ _ "; + n1 = n1[0]; + } else if (n2.getKind() == kind::NOT) { + Debug("mgdx") << "n2 is negative" << std::endl; + Debug("pf::array") << "n1 = " << n1 << ", n2 = " << n2 << std::endl; + secondNeg = true; + ss << "(negtrans2 _ _ _ _ "; + n2 = n2[0]; + } else { + ss << "(trans _ _ _ _ "; + } + + if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && + (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + // Both elements of the transitivity rule are equalities/iffs + { + if(n1[0] == n2[0]) { + if(tb == 1) { Debug("mgdx") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str(); + } else if(n1[1] == n2[1]) { + if(tb == 1) { Debug("mgdx") << "case 2\n"; } + n1 = eqNode(n1[0], n2[0]); + ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")"; + } else if(n1[0] == n2[1]) { + if(tb == 1) { Debug("mgdx") << "case 3\n"; } + if(!firstNeg && !secondNeg) { + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + } else if (firstNeg) { + n1 = eqNode(n1[1], n2[0]); + ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; + } else { + Assert(secondNeg); + n1 = eqNode(n1[1], n2[0]); + ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")"; + } + if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } + } else if(n1[1] == n2[0]) { + if(tb == 1) { Debug("mgdx") << "case 4\n"; } + n1 = eqNode(n1[0], n2[1]); + ss << ss1.str() << " " << ss2.str(); + } else { + 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); + //toStreamRec(Warning.getStream(), pf, 0); + Warning() << "\n\n"; + Unreachable(); + } + Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl; + } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + // n1 is an equality/iff, but n2 is a predicate + if(n1[0] == n2) { + n1 = n1[1]; + ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") + << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; + } else if(n1[1] == n2) { + n1 = n1[0]; + ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; + } else { + Unreachable(); + } + } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + // n2 is an equality/iff, but n1 is a predicate + if(n2[0] == n1) { + n1 = n2[1]; + ss << (secondNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") + << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; + } else if(n2[1] == n1) { + n1 = n2[0]; + ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; + } else { + Unreachable(); + } + } else { + // Both n1 and n2 are prediacates. Don't know what to do... + Unreachable(); + } + + ss << ")"; + + if (firstNeg || secondNeg) { + n1 = (n1.getKind() == kind::NOT) ? n1[0] : n1.notNode(); + } + } + + out << ss.str(); + Debug("mgd") << "\n++ trans proof done, have proven " << n1 << std::endl; + //return (firstNeg || secondNeg) ? n1.notNode() : n1; + return n1; + } + + case theory::eq::MERGED_ARRAYS_ROW: { + Debug("mgd") << "row lemma: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + + + if (pf->d_node[1].getKind() == kind::SELECT) { + // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k). + TNode t1, t2, t3, t4; + Node ret; + if(pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0].getKind() == kind::STORE && + pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0] == pf->d_node[1][0][0] && + pf->d_node[0][1] == pf->d_node[1][1]) { + t2 = pf->d_node[1][0][1]; + t3 = pf->d_node[1][1]; + t1 = pf->d_node[0][0]; + t4 = pf->d_node[1][0][2]; + ret = pf->d_node[1].eqNode(pf->d_node[0]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + } else { + Assert(pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0].getKind() == kind::STORE && + pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0] == pf->d_node[0][0][0] && + pf->d_node[1][1] == pf->d_node[0][1]); + t2 = pf->d_node[0][0][1]; + t3 = pf->d_node[0][1]; + t1 = pf->d_node[1][0]; + t4 = pf->d_node[0][0][2]; + ret = pf->d_node; + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + } + + // inner index != outer index + // t3 is the outer index + + + Assert(pf->d_children.size() == 1); + std::stringstream ss; + Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + + out << "(row _ _ "; + tp->printTerm(t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << " "; + tp->printTerm(t1.toExpr(), out, map); + out << " "; + tp->printTerm(t4.toExpr(), out, map); + out << " "; + + Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node + << ". t3 is: " << t3 << std::endl + << "subproof is: " << subproof << std::endl; + + Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + + if (subproof[0][1] == t3) { + Debug("pf::array") << "Dont need symmetry!" << std::endl; + out << ss.str(); + } else { + Debug("pf::array") << "Need symmetry!" << std::endl; + out << "(negsymm _ _ _ " << ss.str() << ")"; + } + + out << ")"; + + return ret; + } else { + Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl; + + Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node << std::endl; + + // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k]) + + // If we wanted to remove the need for "negativerow", we would need to prove i==k using a new satlem. We would: + // 1. Create a new satlem. + // 2. Assume that i != k + // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k]) + // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), obtaining our contradiction + + TNode t1, t2, t3, t4; + Node ret; + + // pf->d_node is an equality, i==k. + t1 = pf->d_node[0]; + t2 = pf->d_node[1]; + + // pf->d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))), + // or its symmetrical version. + + unsigned side; + if (pf->d_children[0]->d_node[0][0].getKind() == kind::SELECT && + pf->d_children[0]->d_node[0][0][0].getKind() == kind::STORE) { + side = 0; + } else if (pf->d_children[0]->d_node[0][1].getKind() == kind::SELECT && + pf->d_children[0]->d_node[0][1][0].getKind() == kind::STORE) { + side = 1; + } + else { + Unreachable(); + } + + Debug("pf::array") << "Side is: " << side << std::endl; + + // The array's index and element types will come from the subproof... + t3 = pf->d_children[0]->d_node[0][side][0][0]; + t4 = pf->d_children[0]->d_node[0][side][0][2]; + ret = pf->d_node; + + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + + Assert(pf->d_children.size() == 1); + std::stringstream ss; + Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + + Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; + + out << "(negativerow _ _ "; + tp->printTerm(t1.toExpr(), out, map); + out << " "; + tp->printTerm(t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << " "; + tp->printTerm(t4.toExpr(), out, map); + out << " "; + + + // if (subproof[0][1] == t3) { + Debug("pf::array") << "Dont need symmetry!" << std::endl; + out << ss.str(); + // } else { + // Debug("pf::array") << "Need symmetry!" << std::endl; + // out << "(negsymm _ _ _ " << ss.str() << ")"; + // } + + out << ")"; + + // Unreachable(); + + return ret; + } + } + + case theory::eq::MERGED_ARRAYS_ROW1: { + Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + TNode t1, t2, t3; + Node ret; + if(pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0].getKind() == kind::STORE && + pf->d_node[1][0][1] == pf->d_node[1][1] && + pf->d_node[1][0][2] == pf->d_node[0]) { + t1 = pf->d_node[1][0][0]; + t2 = pf->d_node[1][0][1]; + t3 = pf->d_node[0]; + ret = pf->d_node[1].eqNode(pf->d_node[0]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + } else { + Assert(pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0].getKind() == kind::STORE && + pf->d_node[0][0][1] == pf->d_node[0][1] && + pf->d_node[0][0][2] == pf->d_node[1]); + t1 = pf->d_node[0][0][0]; + t2 = pf->d_node[0][0][1]; + t3 = pf->d_node[1]; + ret = pf->d_node; + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + } + out << "(row1 _ _ "; + tp->printTerm(t1.toExpr(), out, map); + out << " "; + tp->printTerm(t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << ")"; + return ret; + } + + case theory::eq::MERGED_ARRAYS_EXT: { + theory::eq::EqProof *child_proof; + + Assert(pf->d_node.getKind() == kind::NOT); + Assert(pf->d_node[0].getKind() == kind::EQUAL); + Assert(pf->d_children.size() == 1); + + child_proof = pf->d_children[0]; + Assert(child_proof->d_node.getKind() == kind::NOT); + Assert(child_proof->d_node[0].getKind() == kind::EQUAL); + + Debug("mgd") << "EXT lemma: " << pf->d_node << std::endl; + + TNode t1, t2, t3; + t1 = child_proof->d_node[0][0]; + t2 = child_proof->d_node[0][1]; + t3 = pf->d_node[0][0][1]; + + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + + out << "(or_elim_1 _ _ "; + out << ProofManager::getLitName(child_proof->d_node[0]); + out << " "; + out << ProofManager::getArrayProof()->skolemToLiteral(t3.toExpr()); + out << ")"; + + return pf->d_node; + } + + default: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + AlwaysAssert(false); + return pf->d_node; + } +} + +ArrayProof::ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* pe) + : TheoryProof(arrays, pe) +{} + +void ArrayProof::registerTerm(Expr term) { + // already registered + if (d_declarations.find(term) != d_declarations.end()) + return; + + Type type = term.getType(); + if (type.isSort()) { + // declare uninterpreted sorts + d_sorts.insert(type); + } + + if (term.getKind() == kind::APPLY_UF) { + Expr function = term.getOperator(); + d_declarations.insert(function); + } + + if (term.isVariable()) { + d_declarations.insert(term); + } + + // recursively declare all other terms + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + // could belong to other theories + d_proofEngine->registerTerm(term[i]); + } +} + +std::string ArrayProof::skolemToLiteral(Expr skolem) { + Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end()); + return d_skolemToLiteral[skolem]; +} + +void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { + Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl; + + Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY); + + if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) { + // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term + // hiding as a subterm of an array term. In that case, send it back to the dispatcher. + d_proofEngine->printBoundTerm(term, os, map); + return; + } + + if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM) { + os << term; + return; + } + + Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE)); + + switch (term.getKind()) { + case kind::SELECT: + Assert(term.getNumChildren() == 2); + os << "(apply _ _ (apply _ _ (read "; + printSort(ArrayType(term[0].getType()).getIndexType(), os); + os << " "; + printSort(ArrayType(term[0].getType()).getConstituentType(), os); + os << ") "; + printTerm(term[0], os, map); + os << ") "; + printTerm(term[1], os, map); + os << ") "; + return; + + case kind::PARTIAL_SELECT_0: + Assert(term.getNumChildren() == 1); + os << "(read "; + printSort(ArrayType(term[0].getType()).getIndexType(), os); + os << " "; + printSort(ArrayType(term[0].getType()).getConstituentType(), os); + os << ") "; + return; + + case kind::PARTIAL_SELECT_1: + Debug("pf::array") << "This branch has not beed tested yet." << std::endl; + Unreachable(); + + Assert(term.getNumChildren() == 1); + os << "(apply _ _ (read "; + printSort(ArrayType(term[0].getType()).getIndexType(), os); + os << " "; + printSort(ArrayType(term[0].getType()).getConstituentType(), os); + os << ") "; + printTerm(term[0], os, map); + os << ") "; + return; + + case kind::STORE: + os << "(apply _ _ (apply _ _ (apply _ _ (write "; + printSort(ArrayType(term[0].getType()).getIndexType(), os); + os << " "; + printSort(ArrayType(term[0].getType()).getConstituentType(), os); + os << ") "; + printTerm(term[0], os, map); + os << ") "; + printTerm(term[1], os, map); + os << ") "; + printTerm(term[2], os, map); + os << ") "; + return; + + default: + Unreachable(); + return; + } +} + +void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { + Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; + Assert (type.isArray() || type.isSort()); + os << type <<" "; +} + +void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { + os << " ;; Array Theory Lemma \n;;"; + for (unsigned i = 0; i < lemma.size(); ++i) { + os << lemma[i] <<" "; + } + os <<"\n"; + //os << " (clausify_false trust)"; + ArrayProof::printTheoryLemmaProof(lemma, os, paren); +} + +void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { + // declaring the sorts + Debug("pf::array") << "Arrays declaring sorts..." << std::endl; + + for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { + if (!ProofManager::currentPM()->wasPrinted(*it)) { + os << "(% " << *it << " sort\n"; + paren << ")"; + ProofManager::currentPM()->markPrinted(*it); + } + } +} + +void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::array") << "Arrays declaring terms..." << std::endl; + + for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { + Expr term = *it; + + Assert(term.getType().isArray() || term.isVariable()); + + Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is: " << term + << ". It's type is: " << term.getType() + << std::endl; + + if (term.getType().isArray()){ + ArrayType array_type(term.getType()); + + Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is an array. Index type: " + << array_type.getIndexType() + << ", element type: " << array_type.getConstituentType() << std::endl; + + os << "(% " << ProofManager::sanitize(term) << " "; + os << "(term "; + os << "(Array "; + + printSort(array_type.getIndexType(), os); + os << " "; + printSort(array_type.getConstituentType(), os); + + os << "))\n"; + } else { + Assert(term.isVariable()); + if (ProofManager::getSkolemizationManager()->isSkolem(*it)) { + Debug("pf::array") << "This term is a skoelm!" << std::endl; + d_skolemDeclarations.insert(*it); + } else { + os << "(% " << ProofManager::sanitize(term) << " "; + os << "(term "; + os << term.getType() << ")\n"; + } + } + + paren << ")"; + } + + Debug("pf::array") << "Declaring terms done!" << std::endl; +} + +void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::array") << "Array: print deferred declarations called" << std::endl; + + for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) { + Expr term = *it; + Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it); + + Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: term is: " << *it << std::endl + << "It is a witness for: " << equality << std::endl; + + std::ostringstream newSkolemLiteral; + newSkolemLiteral << ".sl" << d_skolemToLiteral.size(); + std::string skolemLiteral = newSkolemLiteral.str(); + + d_skolemToLiteral[*it] = skolemLiteral; + + Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: new skolem literal is: " << skolemLiteral << std::endl; + + Assert(equality.getKind() == kind::NOT); + Assert(equality[0].getKind() == kind::EQUAL); + + Node array_one = equality[0][0]; + Node array_two = equality[0][1]; + + LetMap map; + + os << "(ext _ _ "; + printTerm(array_one.toExpr(), os, map); + os << " "; + printTerm(array_two.toExpr(), os, map); + os << " (\\ "; + printTerm(*it, os, map); + os << " (\\ "; + os << skolemLiteral.c_str(); + os << "\n"; + + paren << ")))"; + } +} + +} /* CVC4 namespace */ |