diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/proof | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 833 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 82 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 1260 | ||||
-rw-r--r-- | src/proof/array_proof.h | 70 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 67 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 16 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 88 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 30 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 198 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 42 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 12 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 198 | ||||
-rw-r--r-- | src/proof/skolemization_manager.cpp | 55 | ||||
-rw-r--r-- | src/proof/skolemization_manager.h | 42 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 228 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 127 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 265 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 12 |
18 files changed, 3172 insertions, 453 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp new file mode 100644 index 000000000..abe6cf1d4 --- /dev/null +++ b/src/proof/arith_proof.cpp @@ -0,0 +1,833 @@ +/********************* */ +/*! \file arith_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/arith_proof.h" +#include "theory/arith/theory_arith.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("pf::arith") << "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("pf::arith") << "+ match " << n1 << " " << n2 << 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()) { + return false; + } + for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) { + if(n1[i] != n2[i]) { + return false; + } + } + return true; +} + + +void ProofArith::toStream(std::ostream& out) { + Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl; + //AJR : carry this further? + LetMap map; + toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map); +} + +void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) { + Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl; + pf->debug_print("lfsc-arith"); + Debug("lfsc-arith") << std::endl; + toStreamRecLFSC( out, tp, pf, 0, map ); +} + +Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) { + Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; + pf->debug_print("pf::arith"); + Debug("pf::arith") << 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::arith") << "Handling congruence over equalities" << std::endl; + + // Gather the sequence of consecutive congruence closures. + std::vector<const theory::eq::EqProof *> congruenceClosures; + unsigned count; + Debug("pf::arith") << "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::arith") << "Found a congruence: " << std::endl; + pf->d_children[i+count]->debug_print("pf::arith"); + congruenceClosures.push_back(pf->d_children[i+count]); + } + + Debug("pf::arith") << "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::arith") << "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::arith") << "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; + //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); + Debug("pf::arith") << "\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("pf::arith") << "\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); + out << "(clausify_false (contra _ "; + Debug("pf::arith") << "\nhave proven: " << n1 << std::endl; + Debug("pf::arith") << "n2 is " << n2[0] << std::endl; + + if (n2[0].getNumChildren() > 0) { Debug("pf::arith") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("pf::arith") << "n1[1]: " << n1[1] << std::endl; } + + 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(); + } + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + } + return Node(); + } + + switch(pf->d_id) { + case theory::eq::MERGED_THROUGH_CONGRUENCE: { + Debug("pf::arith") << "\nok, looking at congruence:\n"; + pf->debug_print("pf::arith"); + 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::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); + 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("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; + pf2->debug_print("pf::arith"); + Debug("pf::arith") << "looking at " << pf2->d_node << "\n"; + Debug("pf::arith") << " " << n1 << "\n"; + Debug("pf::arith") << " " << n2 << "\n"; + int side = 0; + if(match(pf2->d_node, n1[0])) { + //if(tb == 1) { + Debug("pf::arith") << "SIDE IS 0\n"; + //} + side = 0; + } else { + //if(tb == 1) { + Debug("pf::arith") << "SIDE IS 1\n"; + //} + if(!match(pf2->d_node, n1[1])) { + Debug("pf::arith") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("pf::arith"); + } + 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::STORE) { + if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) { + b1 << n1[side].getOperator(); + } else { + b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); + } + b1.append(n1[side].begin(), n1[side].end()); + } else { + b1 << n1[side]; + } + if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) { + if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) { + b2 << n1[1-side].getOperator(); + } else { + b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); + } + b2.append(n1[1-side].begin(), n1[1-side].end()); + } else { + b2 << n1[1-side]; + } + Debug("pf::arith") << "pf2->d_node " << pf2->d_node << std::endl; + Debug("pf::arith") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl; + Debug("pf::arith") << "n1 " << n1 << std::endl; + Debug("pf::arith") << "n2 " << n2 << std::endl; + Debug("pf::arith") << "side " << side << std::endl; + if(pf2->d_node[b1.getNumChildren() - (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() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + b1 << n2[1-side]; + b2 << n2[side]; + out << "(symm _ _ _ " << ss.str() << ")"; + } + out << ")"; + while(!stk.empty()) { + if(tb == 1) { + Debug("pf::arith") << "\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("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n"; + Debug("pf::arith") << "looking at " << pf2->d_node << "\n"; + Debug("pf::arith") << " " << n1 << "\n"; + Debug("pf::arith") << " " << n2 << "\n"; + Debug("pf::arith") << " " << b1 << "\n"; + Debug("pf::arith") << " " << 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("pf::arith") << "at end assert, got " << pf2->d_node << " and " << n1 << std::endl; + if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) { + Assert(n1 == pf2->d_node); + } + 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("pf::arith") << "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); + } + } + 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)); + if(tb == 1) { + Debug("pf::arith") << "\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()); + out << ProofManager::getLitName(pf->d_node.negate()); + return pf->d_node; + + case theory::eq::MERGED_THROUGH_TRANS: { + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.size() >= 2); + std::stringstream ss; + Debug("pf::arith") << "\ndoing trans proof[[\n"; + pf->debug_print("pf::arith"); + Debug("pf::arith") << "\n"; + Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n"; + if(tb == 1) { + Debug("pf::arith") << "\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; + } + + // 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::arith") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + + if (!identicalEqualities) { + // The sequence of identical equalities has started just now + identicalEqualities = true; + + Debug("pf::arith") << "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::arith") << "Equality sequence of even length" << std::endl; + Debug("pf::arith") << "n1 is: " << n1 << std::endl; + Debug("pf::arith") << "n2 is: " << n2 << std::endl; + Debug("pf::arith") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::arith") << "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::arith") << "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. + + 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::arith") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; + Assert(false); + } + } + + ss << ")"; + + } else { + Debug("pf::arith") << "Equality sequence length is odd!" << std::endl; + ss.str(ss1.str()); + } + + Debug("pf::arith") << "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("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n"; + if(tb == 1) { + Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; + Debug("pf::arith") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + + if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { + Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; + Debug("pf::arith") << n1[0].getId() << " " << n1[0] << "\n"; + Debug("pf::arith") << n1[1].getId() << " " << n1[1] << "\n"; + Debug("pf::arith") << n2[0].getId() << " " << n2[0] << "\n"; + Debug("pf::arith") << n2[1].getId() << " " << n2[1] << "\n"; + Debug("pf::arith") << (n1[0] == n2[0]) << "\n"; + Debug("pf::arith") << (n1[1] == n2[1]) << "\n"; + Debug("pf::arith") << (n1[0] == n2[1]) << "\n"; + Debug("pf::arith") << (n1[1] == n2[0]) << "\n"; + } + } + 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("pf::arith") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); + } else if(n1[1] == n2[1]) { + if(tb == 1) { Debug("pf::arith") << "case 2\n"; } + n1 = eqNode(n1[0], n2[0]); + ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")"; + } else if(n1[0] == n2[1]) { + if(tb == 1) { Debug("pf::arith") << "case 3\n"; } + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + if(tb == 1) { Debug("pf::arith") << "++ proved " << n1 << "\n"; } + } else if(n1[1] == n2[0]) { + if(tb == 1) { Debug("pf::arith") << "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("pf::arith",0); + //toStreamRec(Warning.getStream(), pf, 0); + Warning() << "\n\n"; + Unreachable(); + } + Debug("pf::arith") << "++ 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 << "(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 << "(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 << ")"; + } + out << ss.str(); + Debug("pf::arith") << "\n++ trans proof done, have proven " << n1 << std::endl; + return n1; + } + + default: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + Debug("pf::arith") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + AlwaysAssert(false); + return pf->d_node; + } +} + +ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe) + : TheoryProof(arith, pe), d_realMode(false) +{} + +void ArithProof::registerTerm(Expr term) { + Debug("pf::arith") << "Arith register term: " << term << ". Kind: " << term.getKind() + << ". Type: " << term.getType() << std::endl; + + if (term.getType().isReal() && !term.getType().isInteger()) { + Debug("pf::arith") << "Entering real mode" << std::endl; + d_realMode = true; + } + + // recursively declare all other terms + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + // could belong to other theories + d_proofEngine->registerTerm(term[i]); + } +} + +void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { + Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind() + << ". Type: " << term.getType() + << ". Number of children: " << term.getNumChildren() << std::endl; + + // !d_realMode <--> term.getType().isInteger() + + Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH); + switch (term.getKind()) { + + case kind::CONST_RATIONAL: { + Assert (term.getNumChildren() == 0); + Assert (term.getType().isInteger() || term.getType().isReal()); + + const Rational& r = term.getConst<Rational>(); + bool neg = (r < 0); + + os << (!d_realMode ? "(a_int " : "(a_real "); + + if (neg) { + os << "(~ "; + } + + if (!d_realMode) { + os << r.abs(); + } else { + os << r.abs().getNumerator(); + os << "/"; + os << r.getDenominator(); + } + + if (neg) { + os << ") "; + } + + os << ") "; + return; + } + + case kind::UMINUS: { + Assert (term.getNumChildren() == 1); + Assert (term.getType().isInteger() || term.getType().isReal()); + os << (!d_realMode ? "(u-_Int " : "(u-_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << ") "; + return; + } + + case kind::PLUS: { + Assert (term.getNumChildren() >= 2); + + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { + os << (!d_realMode ? "(+_Int " : "(+_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } + + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; + } + + case kind::MINUS: { + Assert (term.getNumChildren() >= 2); + + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { + os << (!d_realMode ? "(-_Int " : "(-_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } + + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; + } + + case kind::MULT: { + Assert (term.getNumChildren() >= 2); + + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { + os << (!d_realMode ? "(*_Int " : "(*_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } + + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; + } + + case kind::DIVISION: + case kind::DIVISION_TOTAL: { + Assert (term.getNumChildren() >= 2); + + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { + os << (!d_realMode ? "(/_Int " : "(/_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } + + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; + } + + case kind::GT: + Assert (term.getNumChildren() == 2); + os << (!d_realMode ? "(>_Int " : "(>_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; + + case kind::GEQ: + Assert (term.getNumChildren() == 2); + os << (!d_realMode ? "(>=_Int " : "(>=_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; + + case kind::LT: + Assert (term.getNumChildren() == 2); + os << (!d_realMode ? "(<_Int " : "(<_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; + + case kind::LEQ: + Assert (term.getNumChildren() == 2); + os << (!d_realMode ? "(<=_Int " : "(<=_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; + + default: + Debug("pf::arith") << "Default printing of term: " << term << std::endl; + os << term; + return; + } +} + +void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) { + Debug("pf::arith") << "Arith print sort: " << type << std::endl; + + if (type.isInteger() && d_realMode) { + // If in "real mode", don't use type Int for, e.g., equality. + os << "Real "; + } else { + os << type << " "; + } +} + +void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { + os << " ;; Arith Theory Lemma \n;;"; + for (unsigned i = 0; i < lemma.size(); ++i) { + os << lemma[i] <<" "; + } + os <<"\n"; + //os << " (clausify_false trust)"; + ArithProof::printTheoryLemmaProof( lemma, os, paren ); +} + +void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { +} + +void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { +} + +void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + +} /* CVC4 namespace */ diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h new file mode 100644 index 000000000..a35a5f57e --- /dev/null +++ b/src/proof/arith_proof.h @@ -0,0 +1,82 @@ +/********************* */ +/*! \file arith_proof.h + ** \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 Arith proof + ** + ** Arith proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ARITH__PROOF_H +#define __CVC4__ARITH__PROOF_H + +#include "expr/expr.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { + +//proof object outputted by TheoryArith +class ProofArith : public Proof { +private: + static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map); +public: + ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {} + //it is simply an equality engine proof + theory::eq::EqProof * d_proof; + void toStream(std::ostream& out); + static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map); +}; + + +namespace theory { +namespace arith { +class TheoryArith; +} +} + +typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; + + +class ArithProof : public TheoryProof { +protected: + // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations + + // TypeSet d_sorts; // all the uninterpreted sorts in this theory + // ExprSet d_declarations; // all the variable/function declarations + + bool d_realMode; + +public: + ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine); + + virtual void registerTerm(Expr term); +}; + +class LFSCArithProof : public ArithProof { +public: + LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) + : ArithProof(arith, proofEngine) + {} + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); +}; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__ARITH__PROOF_H */ 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 */ diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index beaf5194c..9b308dcd8 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -23,53 +23,65 @@ #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "theory/arrays/theory_arrays.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { +//proof object outputted by TheoryARRAY +class ProofArray : public Proof { +private: + static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + theory::eq::EqProof* pf, + unsigned tb, + const LetMap& map); + + std::hash_map<Node, Node, NodeHashFunction> d_nodeToSkolem; +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); + static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); + + void registerSkolem(Node equality, Node skolem); +}; + namespace theory { namespace arrays{ class TheoryArrays; } /* namespace CVC4::theory::arrays */ } /* namespace CVC4::theory */ +typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; + class ArrayProof : public TheoryProof { // TODO: whatever goes in this theory +protected: + TypeSet d_sorts; // all the uninterpreted sorts in this theory + ExprSet d_declarations; // all the variable/function declarations + ExprSet d_skolemDeclarations; // all the skolem variable declarations + std::map<Expr, std::string> d_skolemToLiteral; + public: - ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) - : TheoryProof(arrays, proofEngine) - {} - virtual void registerTerm(Expr term) {} - - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - virtual void printSort(Type type, std::ostream& os) = 0; - /** - * Print a proof for the theory lemma. Must prove - * clause representing lemma to be used in resolution proof. - * - * @param lemma clausal form of lemma - * @param os output stream - */ - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0; - /** - * Print the variable/sorts declarations for this theory. - * - * @param os - * @param paren - */ - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine); + + std::string skolemToLiteral(Expr skolem); + + virtual void registerTerm(Expr term); }; class LFSCArrayProof : public ArrayProof { public: - LFSCArrayProof(theory::arrays::TheoryArrays* uf, TheoryProofEngine* proofEngine) - : ArrayProof(uf, proofEngine) + LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) + : ArrayProof(arrays, proofEngine) {} - // TODO implement - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) {} - virtual void printSort(Type type, std::ostream& os) {} - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {} - virtual void printDeclarations(std::ostream& os, std::ostream& paren) {} + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index a018d8bc5..cc1003b2c 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,8 +15,7 @@ ** \todo document this file **/ -#include "proof/bitvector_proof.h" - +#include "proof/bitvector_proof.h" #include "options/bv_options.h" #include "proof/clause_id.h" #include "proof/proof_utils.h" @@ -131,10 +130,10 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl expr_confl.push_back(expr_lit); } Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); - Debug("bv-proof") << "Make conflict for " << conflict << std::endl; + Debug("pf::bv") << "Make conflict for " << conflict << std::endl; if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { - Debug("bv-proof") << "Abort...already conflict for " << conflict << std::endl; + Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl; // This can only happen when we have eager explanations in the bv solver // if we don't get to propagate p before ~p is already asserted d_resolutionProof->cancelResChain(); @@ -145,30 +144,33 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); d_bbConflictMap[conflict] = clause_id; d_resolutionProof->endResChain(clause_id); - Debug("bv-proof") << "BitVectorProof::endBVConflict id"<<clause_id<< " => " << conflict << "\n"; + Debug("pf::bv") << "BitVectorProof::endBVConflict id"<<clause_id<< " => " << conflict << "\n"; d_isAssumptionConflict = false; } void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - Debug("bv-proof") << "Construct full proof." << std::endl; + Debug("pf::bv") << "Construct full proof." << std::endl; d_resolutionProof->constructProof(); return; } for(unsigned i = 0; i < conflicts.size(); ++i) { Expr confl = conflicts[i]; - Debug("bv-proof") << "Finalize conflict " << confl << std::endl; + Debug("pf::bv") << "Finalize conflict " << confl << std::endl; //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ ClauseId id = d_bbConflictMap[confl]; d_resolutionProof->collectClauses(id); }else{ - Debug("bv-proof") << "Do not collect clauses for " << confl << std::endl; + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl; } } } -void LFSCBitVectorProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { + Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: " + << Theory::theoryOf(term) << std::endl; + Assert (Theory::theoryOf(term) == THEORY_BV); // peel off eager bit-blasting trick @@ -233,7 +235,7 @@ void LFSCBitVectorProof::printTerm(Expr term, std::ostream& os, const LetMap& ma return; } case kind::BITVECTOR_BITOF : { - printBitOf(term, os); + printBitOf(term, os, map); return; } case kind::VARIABLE: @@ -246,13 +248,25 @@ void LFSCBitVectorProof::printTerm(Expr term, std::ostream& os, const LetMap& ma } } -void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os) { +void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& map) { Assert (term.getKind() == kind::BITVECTOR_BITOF); unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex; Expr var = term[0]; - Assert (var.getKind() == kind::VARIABLE || - var.getKind() == kind::SKOLEM); - os << "(bitof " << ProofManager::sanitize(var) <<" " << bit <<")"; + + Debug("pf::bv") << "LFSCBitVectorProof::printBitOf( " << term << " ), " + << "bit = " << bit + << ", var = " << var << std::endl; + + os << "(bitof "; + if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) { + // If var is "simple", we can just sanitize and print + os << ProofManager::sanitize(var); + } else { + // If var is "complex", it can belong to another theory. Therefore, dispatch again. + d_proofEngine->printBoundTerm(var, os, map); + } + + os << " " << bit << ")"; } void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { @@ -333,7 +347,9 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co os <<")"; } -void LFSCBitVectorProof::printSort(Type type, std::ostream& os) { +void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { + Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl; + Assert (type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec "<<width<<")"; @@ -369,12 +385,20 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os ClauseId lemma_id = d_bbConflictMap[lem]; d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); os <<lemma_paren.str(); - }else{ - Debug("bv-proof") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; + } else { + Unreachable(); // If we were to reach here, we would crash because BV replay is currently not supported + // in TheoryProof::printTheoryLemmaProof() + + Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl; BitVectorProof::printTheoryLemmaProof( lemma, os, paren ); } } -void LFSCBitVectorProof::printDeclarations(std::ostream& os, std::ostream& paren) { + +void LFSCBitVectorProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + +void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { @@ -383,6 +407,9 @@ void LFSCBitVectorProof::printDeclarations(std::ostream& os, std::ostream& paren } } +void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { // TODO: once we have the operator elimination rules remove those that we @@ -429,7 +456,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { os <<" _ _ _ _ _ _ "; } os << getBBTermName(term[0]) <<" "; - + for (unsigned i = 1; i < term.getNumChildren(); ++i) { os << getBBTermName(term[i]); os << ") "; @@ -489,7 +516,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { case kind::BITVECTOR_SHL : case kind::BITVECTOR_LSHR : case kind::BITVECTOR_ASHR : { - // these are terms for which bit-blasting is not supported yet + // these are terms for which bit-blasting is not supported yet std::ostringstream paren; os <<"(trust_bblast_term _ "; paren <<")"; diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 80d567f7c..4fabc8be3 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -19,7 +19,7 @@ #ifndef __CVC4__BITVECTOR__PROOF_H #define __CVC4__BITVECTOR__PROOF_H -//#include <cstdint> +//#include <cstdint> #include <ext/hash_map> #include <ext/hash_set> #include <iostream> @@ -45,7 +45,7 @@ template <class T> class TBitblaster; } /* namespace CVC4::theory::bv */ } /* namespace CVC4::theory */ -class CnfProof; +class CnfProof; } /* namespace CVC4 */ namespace CVC4 { @@ -109,7 +109,7 @@ public: virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0; - + virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0; @@ -122,17 +122,19 @@ class LFSCBitVectorProof: public BitVectorProof { void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map); void printPredicate(Expr term, std::ostream& os, const LetMap& map); void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map); - void printBitOf(Expr term, std::ostream& os); + void printBitOf(Expr term, std::ostream& os, const LetMap& map); public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) {} - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); - virtual void printSort(Type type, std::ostream& os); + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTermBitblasting(Expr term, std::ostream& os); virtual void printAtomBitblasting(Expr term, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printBitblasting(std::ostream& os, std::ostream& paren); virtual void printResolutionProof(std::ostream& os, std::ostream& paren); }; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 31c976a63..f9823ea92 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -24,16 +24,15 @@ #include "prop/minisat/minisat.h" #include "prop/sat_solver_types.h" -using namespace CVC4::prop; - namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream, +CnfProof::CnfProof(prop::CnfStream* stream, context::Context* ctx, const std::string& name) : d_cnfStream(stream) , d_clauseToAssertion(ctx) , d_assertionToProofRule(ctx) + , d_clauseIdToOwnerTheory(ctx) , d_currentAssertionStack() , d_currentDefinitionStack() , d_clauseToDefinition(ctx) @@ -56,12 +55,13 @@ bool CnfProof::isDefinition(Node node) { return d_definitions.find(node) != d_definitions.end(); } - + ProofRule CnfProof::getProofRule(Node node) { Assert (isAssertion(node)); NodeToProofRule::iterator it = d_assertionToProofRule.find(node); return (*it).second; } + ProofRule CnfProof::getProofRule(ClauseId clause) { TNode assertion = getAssertionForClause(clause); return getProofRule(assertion); @@ -96,13 +96,14 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { Node current_assertion = getCurrentAssertion(); Node current_expr = getCurrentDefinition(); - + Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause << " assertion = " << current_assertion << clause << " definition = " << current_expr << std::endl; setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); + registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -114,7 +115,7 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { // that since b is top level, it is not cached by the CnfStream) if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) return; - + d_clauseToAssertion.insert (clause, expr); } @@ -128,7 +129,7 @@ void CnfProof::setClauseDefinition(ClauseId clause, Node definition) { d_clauseToDefinition.insert(clause, definition); d_definitions.insert(definition); } - + void CnfProof::registerAssertion(Node assertion, ProofRule reason) { Debug("proof:cnf") << "CnfProof::registerAssertion " << assertion << " reason " << reason << std::endl; @@ -142,6 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } +void CnfProof::registerExplanationLemma(ClauseId clauseId) { + d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); +} + +theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { + Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); + return d_clauseIdToOwnerTheory[clause]; +} + + void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -160,10 +171,10 @@ void CnfProof::pushCurrentAssertion(Node assertion) { void CnfProof::popCurrentAssertion() { Assert (d_currentAssertionStack.size()); - + Debug("proof:cnf") << "CnfProof::popCurrentAssertion " << d_currentAssertionStack.back() << std::endl; - + d_currentAssertionStack.pop_back(); } @@ -172,6 +183,14 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } +void CnfProof::setExplainerTheory(theory::TheoryId theory) { + d_explainerTheory = theory; +} + +theory::TheoryId CnfProof::getExplainerTheory() { + return d_explainerTheory; +} + void CnfProof::pushCurrentDefinition(Node definition) { Debug("proof:cnf") << "CnfProof::pushCurrentDefinition " << definition << std::endl; @@ -181,10 +200,10 @@ void CnfProof::pushCurrentDefinition(Node definition) { void CnfProof::popCurrentDefinition() { Assert (d_currentDefinitionStack.size()); - + Debug("proof:cnf") << "CnfProof::popCurrentDefinition " << d_currentDefinitionStack.back() << std::endl; - + d_currentDefinitionStack.pop_back(); } @@ -204,8 +223,8 @@ Node CnfProof::getAtom(prop::SatVariable var) { void CnfProof::collectAtoms(const prop::SatClause* clause, NodeSet& atoms) { for (unsigned i = 0; i < clause->size(); ++i) { - SatLiteral lit = clause->operator[](i); - SatVariable var = lit.getSatVariable(); + prop::SatLiteral lit = clause->operator[](i); + prop::SatVariable var = lit.getSatVariable(); TNode atom = getAtom(var); if (atoms.find(atom) == atoms.end()) { Assert (atoms.find(atom) == atoms.end()); @@ -247,8 +266,8 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) { - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); + NodeSet::const_iterator it = atoms.begin(); + NodeSet::const_iterator end = atoms.end(); for (;it != end; ++it) { os << "(decl_atom "; @@ -257,7 +276,7 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, //FIXME hideous LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - + os << " (\\ " << ProofManager::getVarName(var, d_name) << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; @@ -297,9 +316,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // paren << "))"; // return; - + Assert( clause->size()>0 ); - + Node base_assertion = getDefinitionForClause(id); //get the assertion for the clause id @@ -359,19 +378,19 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, std::stringstream os_paren; //eliminate each one for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) { + Trace("cnf-pf-debug") << "; base_assertion[" << j << "] is: " << base_assertion[j] + << ", and its kind is: " << base_assertion[j].getKind() << std::endl ; + Node child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; bool child_pol = base_assertion[j].getKind()!=kind::NOT; - - if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ - child_pol = !child_pol; - } - + Trace("cnf-pf-debug") << "; child " << j << " " - << child_base << " " - << child_pol << " " - << childPol[child_base] << std::endl; - + << ", child base: " << child_base + << ", child pol: " << child_pol + << ", childPol[child_base] " + << childPol[child_base] << ", base pol: " << base_pol << std::endl; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); if( itcic!=childIndex.end() ){ @@ -379,7 +398,13 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os_main << "(or_elim_1 _ _ "; prop::SatLiteral lit = (*clause)[itcic->second]; // Should be if in the original formula it was negated - if( childPol[child_base] && base_pol ){ + // if( childPol[child_base] && base_pol ){ + + // Adding the below to catch a specific case where the first child of an IMPLIES is negative, + // in which case we need not_not introduction. + if (base_assertion.getKind() == kind::IMPLIES && !child_pol && base_pol) { + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; + } else if (childPol[child_base] && base_pol) { os_main << ProofManager::getLitName(lit, d_name) << " "; }else{ os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; @@ -393,6 +418,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, success = false; } } + if( success ){ if( base_assertion.getKind()==kind::IMPLIES ){ os_main << "(impl_elim _ _ "; @@ -422,7 +448,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, }else if ((base_assertion.getKind()==kind::AND && base_pol) || ((base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES) && !base_pol)) { - + std::stringstream os_main; Node iatom; @@ -433,7 +459,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Assert( assertion.getNumChildren()==1 ); iatom = assertion[0]; } - + Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl; Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom; bool e_pol = iatom.getKind()!=kind::NOT; @@ -731,6 +757,4 @@ bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) { } } - - } /* CVC4 namespace */ diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index e5a80b428..b4df850f7 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -21,7 +21,7 @@ #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include <ext/hash_map> +#include <ext/hash_map> #include <ext/hash_set> #include <iosfwd> @@ -43,6 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; +typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; class CnfProof { protected: @@ -54,28 +55,33 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; + /** Map from assertion to the theory that added this assertion **/ + ClauseIdToTheory d_clauseIdToOwnerTheory; + + /** The last theory to explain a lemma **/ + theory::TheoryId d_explainerTheory; + /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; /** Top of stack is top-level fact currently being converted to CNF **/ std::vector<Node> d_currentDefinitionStack; - /** Map from ClauseId to the top-level fact that lead to adding this clause **/ ClauseIdToNode d_clauseToDefinition; /** Top-level facts that follow from assertions during convertAndAssert **/ NodeSet d_definitions; - + /** Map from top-level fact to facts/assertion that it follows from **/ NodeToNode d_cnfDeps; ClauseIdSet d_explanations; - + bool isDefinition(Node node); Node getDefinitionForClause(ClauseId clause); - + std::string d_name; public: CnfProof(CVC4::prop::CnfStream* cnfStream, @@ -103,10 +109,10 @@ public: /** Clause is one of the clauses defining top-level assertion node*/ void setClauseAssertion(ClauseId clause, Node node); - + void registerAssertion(Node assertion, ProofRule reason); void setCnfDependence(Node from, Node to); - + void pushCurrentAssertion(Node assertion); // the current assertion being converted void popCurrentAssertion(); Node getCurrentAssertion(); @@ -115,14 +121,18 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - + void setExplainerTheory(theory::TheoryId theory); + theory::TheoryId getExplainerTheory(); + theory::TheoryId getOwnerTheory(ClauseId clause); + + void registerExplanationLemma(ClauseId clauseId); + // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); ProofRule getProofRule(Node assertion); ProofRule getProofRule(ClauseId clause); Node getAssertionForClause(ClauseId clause); - /** Virtual methods for printing things **/ virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, @@ -154,7 +164,7 @@ public: void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); - + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 93752d3cf..0cec6e149 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -1,19 +1,19 @@ /********************* */ /*! \file proof_manager.cpp - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds - ** 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 - **/ +** \verbatim +** Original author: Liana Hadarean +** Major contributors: Morgan Deters +** Minor contributors (to current version): Andrew Reynolds +** 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/proof_manager.h" @@ -105,6 +105,7 @@ UFProof* ProofManager::getUfProof() { TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF); return (UFProof*)pf; } + BitVectorProof* ProofManager::getBitVectorProof() { Assert (options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); @@ -117,6 +118,17 @@ ArrayProof* ProofManager::getArrayProof() { return (ArrayProof*)pf; } +ArithProof* ProofManager::getArithProof() { + Assert (options::proof()); + TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH); + return (ArithProof*)pf; +} + +SkolemizationManager* ProofManager::getSkolemizationManager() { + Assert (options::proof()); + return &(currentPM()->d_skolemizationManager); +} + void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); @@ -210,14 +222,22 @@ std::string ProofManager::getLitName(TNode lit, return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); } -std::string ProofManager::sanitize(TNode var) { - Assert (var.isVar()); - std::string name = var.toString(); - std::replace(name.begin(), name.end(), ' ', '_'); +std::string ProofManager::sanitize(TNode node) { + Assert (node.isVar() || node.isConst()); + + std::string name = node.toString(); + if (node.isVar()) { + std::replace(name.begin(), name.end(), ' ', '_'); + } else if (node.isConst()) { + name.erase(std::remove(name.begin(), name.end(), '('), name.end()); + name.erase(std::remove(name.begin(), name.end(), ')'), name.end()); + name.erase(std::remove(name.begin(), name.end(), ' '), name.end()); + name = "const" + name; + } + return name; } - void ProofManager::traceDeps(TNode n) { Debug("cores") << "trace deps " << n << std::endl; if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) || @@ -319,10 +339,51 @@ void LFSCProof::toStream(std::ostream& out) { d_satProof->collectClausesUsed(used_inputs, used_lemmas); + IdToSatClause::iterator it2; + Debug("pf::pm") << std::endl << "Used inputs: " << std::endl; + for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) { + Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl; + } + Debug("pf::pm") << std::endl; + + // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl; + // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) { + // Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl; + // } + // Debug("pf::pm") << std::endl; + Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl; + for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) { + + std::vector<Expr> clause_expr; + for(unsigned i = 0; i < it2->second->size(); ++i) { + prop::SatLiteral lit = (*(it2->second))[i]; + Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; + clause_expr.push_back(expr_lit); + } + + Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second) << std::endl; + Debug("pf::pm") << "\t"; + for (unsigned i = 0; i < clause_expr.size(); ++i) { + Debug("pf::pm") << clause_expr[i] << " "; + } + Debug("pf::pm") << std::endl; + } + Debug("pf::pm") << std::endl; + // collecting assertions that lead to the clauses being asserted NodeSet used_assertions; d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions); + NodeSet::iterator it3; + Debug("pf::pm") << std::endl << "Used assertions: " << std::endl; + for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) + Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; + NodeSet atoms; // collects the atoms in the clauses d_cnfProof->collectAtomsForClauses(used_inputs, atoms); @@ -334,21 +395,25 @@ void LFSCProof::toStream(std::ostream& out) { utils::collectAtoms(*it, atoms); } - if (Debug.isOn("proof:pm")) { - // std::cout << NodeManager::currentNM(); - Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; - for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } + NodeSet::iterator atomIt; + Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl; + for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) { + Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl; - Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; - for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; + if (Debug.isOn("proof:pm")) { + // std::cout << NodeManager::currentNM(); + Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; + for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { + Debug("proof:pm") << " " << *it << std::endl; + } + + Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; + for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { + Debug("proof:pm") << " " << *it << std::endl; + } } } - - smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; @@ -357,32 +422,55 @@ void LFSCProof::toStream(std::ostream& out) { // declare the theory atoms NodeSet::const_iterator it = atoms.begin(); NodeSet::const_iterator end = atoms.end(); + + Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl; for(; it != end; ++it) { + Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } + + Debug("pf::pm") << std::endl << "Term registration done!" << std::endl << std::endl; + + Debug("pf::pm") << std::endl << "LFSCProof::toStream: starting to print assertions" << std::endl; + // print out all the original assertions + d_theoryProof->registerTermsFromAssertions(); + d_theoryProof->printSortDeclarations(out, paren); + d_theoryProof->printTermDeclarations(out, paren); d_theoryProof->printAssertions(out, paren); + Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl; - out << "(: (holds cln)\n"; + out << "(: (holds cln)\n\n"; + + // Have the theory proofs print deferred declarations, e.g. for skolem variables. + out << " ;; Printing deferred declarations \n"; + d_theoryProof->printDeferredDeclarations(out, paren); // print trust that input assertions are their preprocessed form printPreprocessedAssertions(used_assertions, out, paren); // print mapping between theory atoms and internal SAT variables + out << ";; Printing mapping from preprocessed assertions into atoms \n"; d_cnfProof->printAtomMapping(atoms, out, paren); + Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl; + IdToSatClause::const_iterator cl_it = used_inputs.begin(); // print CNF conversion proof for each clause for (; cl_it != used_inputs.end(); ++cl_it) { d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren); } + Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl; + // FIXME: for now assume all theory lemmas are in CNF form so // distinguish between them and inputs // print theory lemmas for resolution proof - d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); + Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl; + d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); + Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { // print actual resolution proof @@ -404,7 +492,7 @@ void LFSCProof::toStream(std::ostream& out) { void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, std::ostream& paren) { - os << " ;; Preprocessing \n"; + os << "\n ;; In the preprocessor we trust \n"; NodeSet::const_iterator it = assertions.begin(); NodeSet::const_iterator end = assertions.end(); @@ -420,11 +508,12 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, paren << "))"; } -} - + os << "\n"; +} //---from Morgan--- + bool ProofManager::hasOp(TNode n) const { return d_bops.find(n) != d_bops.end(); } @@ -436,16 +525,21 @@ Node ProofManager::lookupOp(TNode n) const { } Node ProofManager::mkOp(TNode n) { + Trace("mgd-pm-mkop") << "MkOp : " << n << " " << n.getKind() << std::endl; if(n.getKind() != kind::BUILTIN) { return n; } + Node& op = d_ops[n]; if(op.isNull()) { - Debug("mgd") << "making an op for " << n << "\n"; + Assert((n.getConst<Kind>() == kind::SELECT) || (n.getConst<Kind>() == kind::STORE)); + + Debug("mgd-pm-mkop") << "making an op for " << n << "\n"; + std::stringstream ss; ss << n; std::string s = ss.str(); - Debug("mgd") << " : " << s << std::endl; + Debug("mgd-pm-mkop") << " : " << s << std::endl; std::vector<TypeNode> v; v.push_back(NodeManager::currentNM()->integerType()); if(n.getConst<Kind>() == kind::SELECT) { @@ -457,44 +551,54 @@ Node ProofManager::mkOp(TNode n) { v.push_back(NodeManager::currentNM()->integerType()); } TypeNode type = NodeManager::currentNM()->mkFunctionType(v); + Debug("mgd-pm-mkop") << "typenode is: " << type << "\n"; op = NodeManager::currentNM()->mkSkolem(s, type, " ignore", NodeManager::SKOLEM_NO_NOTIFY); d_bops[op] = n; } + Debug("mgd-pm-mkop") << "returning the op: " << op << "\n"; return op; } //---end from Morgan--- +bool ProofManager::wasPrinted(const Type& type) const { + return d_printedTypes.find(type) != d_printedTypes.end(); +} + +void ProofManager::markPrinted(const Type& type) { + d_printedTypes.insert(type); +} + std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { switch(k) { case RULE_GIVEN: - out << "RULE_GIVEN"; + out << "RULE_GIVEN"; break; case RULE_DERIVED: - out << "RULE_DERIVED"; + out << "RULE_DERIVED"; break; case RULE_RECONSTRUCT: - out << "RULE_RECONSTRUCT"; + out << "RULE_RECONSTRUCT"; break; case RULE_TRUST: - out << "RULE_TRUST"; + out << "RULE_TRUST"; break; case RULE_INVALID: - out << "RULE_INVALID"; + out << "RULE_INVALID"; break; case RULE_CONFLICT: - out << "RULE_CONFLICT"; + out << "RULE_CONFLICT"; break; case RULE_TSEITIN: - out << "RULE_TSEITIN"; + out << "RULE_TSEITIN"; break; case RULE_SPLIT: - out << "RULE_SPLIT"; + out << "RULE_SPLIT"; break; case RULE_ARRAYS_EXT: - out << "RULE_ARRAYS"; + out << "RULE_ARRAYS"; break; case RULE_ARRAYS_ROW: - out << "RULE_ARRAYS"; + out << "RULE_ARRAYS"; break; default: out << "ProofRule Unknown! [" << unsigned(k) << "]"; diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 58a2f45f7..a39d97816 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -21,7 +21,9 @@ #include <iosfwd> #include <map> - +#include "proof/proof.h" +#include "proof/skolemization_manager.h" +#include "util/proof.h" #include "expr/node.h" #include "proof/clause_id.h" #include "proof/proof.h" @@ -48,11 +50,11 @@ namespace prop { class SmtEngine; const ClauseId ClauseIdEmpty(-1); -const ClauseId ClauseIdUndef(-2); +const ClauseId ClauseIdUndef(-2); const ClauseId ClauseIdError(-3); class Proof; -template <class Solver> class TSatProof; +template <class Solver> class TSatProof; typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof; class CnfProof; @@ -60,10 +62,11 @@ class RewriterProof; class TheoryProofEngine; class TheoryProof; class UFProof; +class ArithProof; class ArrayProof; class BitVectorProof; -template <class Solver> class LFSCSatProof; +template <class Solver> class LFSCSatProof; typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; class LFSCCnfProof; @@ -74,7 +77,7 @@ class LFSCRewriterProof; template <class Solver> class ProofProxy; typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy; -typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; +typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; namespace prop { typedef uint64_t SatVariable; @@ -105,7 +108,7 @@ enum ProofRule { RULE_CONFLICT, /* re-construct as a conflict */ RULE_TSEITIN, /* Tseitin CNF transformation */ RULE_SPLIT, /* A splitting lemma of the form a v ~ a*/ - + RULE_ARRAYS_EXT, /* arrays, extensional */ RULE_ARRAYS_ROW, /* arrays, read-over-write */ };/* enum ProofRules */ @@ -120,6 +123,8 @@ class ProofManager { ExprSet d_inputCoreFormulas; ExprSet d_outputCoreFormulas; + SkolemizationManager d_skolemizationManager; + int d_nextId; Proof* d_fullProof; @@ -129,6 +134,8 @@ class ProofManager { // trace dependences back to unsat core void traceDeps(TNode n); + std::set<Type> d_printedTypes; + protected: LogicInfo d_logic; @@ -153,6 +160,9 @@ public: static UFProof* getUfProof(); static BitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); + static ArithProof* getArithProof(); + + static SkolemizationManager *getSkolemizationManager(); // iterators over data shared by proofs typedef ExprSet::const_iterator assertions_iterator; @@ -163,17 +173,17 @@ public: } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } size_t num_assertions() const { return d_inputFormulas.size(); } - + //---from Morgan--- Node mkOp(TNode n); Node lookupOp(TNode n) const; bool hasOp(TNode n) const; - + std::map<Node, Node> d_ops; std::map<Node, Node> d_bops; //---end from Morgan--- - - + + // variable prefixes static std::string getInputClauseName(ClauseId id, const std::string& prefix = ""); static std::string getLemmaClauseName(ClauseId id, const std::string& prefix = ""); @@ -181,7 +191,7 @@ public: static std::string getLearntClauseName(ClauseId id, const std::string& prefix = ""); static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = ""); static std::string getAssertionName(Node node, const std::string& prefix = ""); - + static std::string getVarName(prop::SatVariable var, const std::string& prefix = ""); static std::string getAtomName(prop::SatVariable var, const std::string& prefix = ""); static std::string getAtomName(TNode atom, const std::string& prefix = ""); @@ -190,14 +200,13 @@ public: // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); - - /** Add proof assertion - unlinke addCoreAssertion this is post definition expansion **/ + /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/ void addAssertion(Expr formula); - + /** Public unsat core methods **/ void addCoreAssertion(Expr formula); - + void addDependence(TNode n, TNode dep); void addUnsatCore(Expr formula); @@ -212,6 +221,9 @@ public: const std::string getLogic() const { return d_logic.getLogicString(); } LogicInfo & getLogicInfo() { return d_logic; } + void markPrinted(const Type& type); + bool wasPrinted(const Type& type) const; + };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index ccb81b9ad..9160ebcfb 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -124,7 +124,7 @@ protected: VarSet d_assumptions; // assumption literals for bv solver IdHashSet d_assumptionConflicts; // assumption conflicts not actually added to SAT solver IdToConflicts d_assumptionConflictsDebug; - + // resolutions IdResMap d_resChains; ResStack d_resStack; @@ -241,13 +241,13 @@ public: ClauseId getTrueUnit() const; ClauseId getFalseUnit() const; - + void registerAssumption(const typename Solver::TVar var); ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); - + ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind); - + /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. @@ -297,12 +297,13 @@ public: virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren) = 0; virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; - void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); void storeClauseGlue(ClauseId clause, int glue); + + private: __gnu_cxx::hash_map<ClauseId, int> d_glueMap; struct Statistics { @@ -321,7 +322,6 @@ private: Statistics d_statistics; };/* class TSatProof */ - template <class S> class ProofProxy { private: diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index d786eef76..653732dd9 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -31,19 +31,19 @@ namespace CVC4 { -template <class Solver> +template <class Solver> void printLit (typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; } -template <class Solver> +template <class Solver> void printClause (typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; } } -template <class Solver> +template <class Solver> void printClause (std::vector<typename Solver::TLit>& c) { for (unsigned i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; @@ -51,7 +51,7 @@ void printClause (std::vector<typename Solver::TLit>& c) { } -template <class Solver> +template <class Solver> void printLitSet(const std::set<typename Solver::TLit>& s) { typename std::set < typename Solver::TLit>::const_iterator it = s.begin(); for(; it != s.end(); ++it) { @@ -62,11 +62,11 @@ void printLitSet(const std::set<typename Solver::TLit>& s) { } // purely debugging functions -template <class Solver> +template <class Solver> void printDebug (typename Solver::TLit l) { Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; } -template <class Solver> +template <class Solver> void printDebug (typename Solver::TClause& c) { for (int i = 0; i < c.size(); i++) { Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; @@ -81,7 +81,7 @@ void printDebug (typename Solver::TClause& c) { * @param id the clause id * @param set the clause converted to a set of literals */ -template <class Solver> +template <class Solver> void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { Assert(set.empty()); if(isUnit(id)) { @@ -95,11 +95,11 @@ void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) { LitVector* clause = d_assumptionConflictsDebug[id]; for (unsigned i = 0; i < clause->size(); ++i) { - set.insert(clause->operator[](i)); + set.insert(clause->operator[](i)); } return; } - + typename Solver::TCRef ref = getClauseRef(id); typename Solver::TClause& c = getClause(ref); for (int i = 0; i < c.size(); i++) { @@ -115,7 +115,7 @@ void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { * @param clause1 * @param clause2 */ -template <class Solver> +template <class Solver> bool resolve(const typename Solver::TLit v, std::set<typename Solver::TLit>& clause1, std::set<typename Solver::TLit>& clause2, bool s) { @@ -134,7 +134,7 @@ bool resolve(const typename Solver::TLit v, } clause1.erase(var); clause2.erase(~var); - typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); + typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); for (; it!= clause2.end(); ++it) { clause1.insert(*it); } @@ -150,7 +150,7 @@ bool resolve(const typename Solver::TLit v, } clause1.erase(~var); clause2.erase(var); - typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); + typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); for (; it!= clause2.end(); ++it) { clause1.insert(*it); } @@ -159,19 +159,19 @@ bool resolve(const typename Solver::TLit v, } /// ResChain -template <class Solver> +template <class Solver> ResChain<Solver>::ResChain(ClauseId start) : d_start(start), d_steps(), d_redundantLits(NULL) {} -template <class Solver> +template <class Solver> void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id, bool sign) { ResStep<Solver> step(lit, id, sign); d_steps.push_back(step); } -template <class Solver> +template <class Solver> void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) { if (d_redundantLits) { d_redundantLits->insert(lit); @@ -183,19 +183,19 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) { /// ProxyProof -template <class Solver> +template <class Solver> ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof): d_proof(proof) {} -template <class Solver> +template <class Solver> void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { d_proof->updateCRef(oldref, newref); } /// SatProof -template <class Solver> +template <class Solver> TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, bool checkRes) : d_solver(solver) , d_cnfProof(NULL) @@ -218,7 +218,7 @@ TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, bool check , d_unitConflictId() , d_storedUnitConflict(false) , d_trueLit(ClauseIdUndef) - , d_falseLit(ClauseIdUndef) + , d_falseLit(ClauseIdUndef) , d_name(name) , d_seenLearnt() , d_seenInputs() @@ -228,10 +228,10 @@ TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, bool check d_proxy = new ProofProxy<Solver>(this); } -template <class Solver> +template <class Solver> TSatProof<Solver>::~TSatProof() { delete d_proxy; - + // FIXME: double free if deleted clause also appears in d_seenLemmas? IdToSatClause::iterator it = d_deletedTheoryLemmas.begin(); IdToSatClause::iterator end = d_deletedTheoryLemmas.end(); @@ -257,8 +257,8 @@ TSatProof<Solver>::~TSatProof() { delete seen_it->second; } } - -template <class Solver> + +template <class Solver> void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) { Assert (d_cnfProof == NULL); d_cnfProof = cnf_proof; @@ -271,7 +271,7 @@ void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) { * * @return */ -template <class Solver> +template <class Solver> bool TSatProof<Solver>::checkResolution(ClauseId id) { if(d_checkRes) { bool validRes = true; @@ -300,9 +300,9 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { if (id == d_emptyClauseId) { return clause1.empty(); } - + LitVector c; - getLitVec(id, c); + getLitVec(id, c); for (unsigned i = 0; i < c.size(); ++i) { int count = clause1.erase(c[i]); @@ -335,7 +335,7 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { /// helper methods -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::getClauseId(typename Solver::TCRef ref) { if(d_clauseId.find(ref) == d_clauseId.end()) { Debug("proof:sat") << "Missing clause \n"; @@ -344,12 +344,12 @@ ClauseId TSatProof<Solver>::getClauseId(typename Solver::TCRef ref) { return d_clauseId[ref]; } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::getClauseId(typename Solver::TLit lit) { Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); return d_unitId[toInt(lit)]; } -template <class Solver> +template <class Solver> typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" " @@ -360,19 +360,19 @@ typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) { return d_idClause[id]; } -template <class Solver> +template <class Solver> typename Solver::TClause& TSatProof<Solver>::getClause(typename Solver::TCRef ref) { Assert(ref != Solver::TCRef_Undef); Assert(ref >= 0 && ref < d_solver->ca.size()); return d_solver->ca[ref]; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) { if (isUnit(id)) { typename Solver::TLit lit = getUnit(id); vec.push_back(lit); - return; + return; } if (isAssumptionConflict(id)) { vec = *(d_assumptionConflictsDebug[id]); @@ -386,44 +386,44 @@ void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) { } -template <class Solver> +template <class Solver> typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) { Assert(d_idUnit.find(id) != d_idUnit.end()); return d_idUnit[id]; } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::isUnit(ClauseId id) { return d_idUnit.find(id) != d_idUnit.end(); } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) { return d_unitId.find(toInt(lit)) != d_unitId.end(); } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) { Assert(isUnit(lit)); return d_unitId[toInt(lit)]; } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::hasResolution(ClauseId id) { return d_resChains.find(id) != d_resChains.end(); } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::isInputClause(ClauseId id) { return (d_inputClauses.find(id) != d_inputClauses.end()); } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::isLemmaClause(ClauseId id) { return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); } -template <class Solver> +template <class Solver> bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) { return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::print(ClauseId id) { if (d_deleted.find(id) != d_deleted.end()) { Debug("proof:sat") << "del"<<id; @@ -437,13 +437,13 @@ void TSatProof<Solver>::print(ClauseId id) { printClause<Solver>(getClause(ref)); } } -template <class Solver> +template <class Solver> void TSatProof<Solver>::printRes(ClauseId id) { Assert(hasResolution(id)); Debug("proof:sat") << "id "<< id <<": "; printRes(d_resChains[id]); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::printRes(ResChain<Solver>* res) { ClauseId start_id = res->getStart(); @@ -468,14 +468,14 @@ void TSatProof<Solver>::printRes(ResChain<Solver>* res) { } /// registration methods -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause, ClauseKind kind) { Assert(clause != Solver::TCRef_Undef); typename ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); - d_clauseId.insert(std::make_pair(clause, newId)); + d_clauseId.insert(std::make_pair(clause, newId)); d_idClause.insert(std::make_pair(newId, clause)); if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); @@ -484,6 +484,11 @@ template <class Solver> if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); d_lemmaClauses.insert(newId); + Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; + d_cnfProof->registerExplanationLemma(newId); } } @@ -497,7 +502,7 @@ template <class Solver> return id; } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, ClauseKind kind) { Debug("cores") << "registerUnitClause " << kind << std::endl; @@ -513,49 +518,54 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " + << lit + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; d_lemmaClauses.insert(newId); + d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; Assert(kind != INPUT || d_inputClauses.count(id)); Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); - Debug("proof:sat:detailed") << "registerUnitClause id: " << id + Debug("proof:sat:detailed") << "registerUnitClause id: " << id <<" kind: " << kind << "\n"; // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); return id; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) { Assert (d_trueLit == ClauseIdUndef); d_trueLit = registerUnitClause(lit, INPUT); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) { Assert (d_falseLit == ClauseIdUndef); d_falseLit = registerUnitClause(lit, INPUT); } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::getTrueUnit() const { Assert (d_trueLit != ClauseIdUndef); return d_trueLit; } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::getFalseUnit() const { Assert (d_falseLit != ClauseIdUndef); return d_falseLit; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) { Assert (d_assumptions.find(var) == d_assumptions.end()); d_assumptions.insert(var); } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TLitVec& confl) { Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; // Uniqueness is checked in the bit-vector proof @@ -565,13 +575,13 @@ ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TL } ClauseId new_id = ProofManager::currentPM()->nextId(); d_assumptionConflicts.insert(new_id); - LitVector* vec_confl = new LitVector(confl.size()); + LitVector* vec_confl = new LitVector(confl.size()); for (int i = 0; i < confl.size(); ++i) { vec_confl->operator[](i) = confl[i]; } if (Debug.isOn("proof:sat:detailed")) { printClause<Solver>(*vec_confl); - Debug("proof:sat:detailed") << "\n"; + Debug("proof:sat:detailed") << "\n"; } d_assumptionConflictsDebug[new_id] = vec_confl; @@ -579,7 +589,7 @@ ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TL } -template <class Solver> +template <class Solver> void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { // if we already added the literal return if (seen.count(lit)) { @@ -606,7 +616,7 @@ void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, LitSet* removedSet } } -template <class Solver> +template <class Solver> void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, ClauseId id) { LitSet* removed = res->getRedundant(); if (removed == NULL) { @@ -637,8 +647,8 @@ void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, ClauseId i } removed->clear(); } - -template <class Solver> + +template <class Solver> void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) { Assert(res != NULL); @@ -662,14 +672,14 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) { /// recording resolutions -template <class Solver> +template <class Solver> void TSatProof<Solver>::startResChain(typename Solver::TCRef start) { ClauseId id = getClauseId(start); ResChain<Solver>* res = new ResChain<Solver>(id); d_resStack.push_back(res); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::startResChain(typename Solver::TLit start) { ClauseId id = getUnitId(start); ResChain<Solver>* res = new ResChain<Solver>(id); @@ -677,7 +687,7 @@ void TSatProof<Solver>::startResChain(typename Solver::TLit start) { } -template <class Solver> +template <class Solver> void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit, typename Solver::TCRef clause, bool sign) { ClauseId id = registerClause(clause, LEARNT); @@ -685,7 +695,7 @@ void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit, res->addStep(lit, id, sign); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::endResChain(ClauseId id) { Debug("proof:sat:detailed") <<"endResChain " << id << "\n"; Assert(d_resStack.size() > 0); @@ -695,7 +705,7 @@ void TSatProof<Solver>::endResChain(ClauseId id) { } -// template <class Solver> +// template <class Solver> // void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) { // Assert(d_resStack.size() > 0); // ClauseId id = registerClause(clause, LEARNT); @@ -704,7 +714,7 @@ void TSatProof<Solver>::endResChain(ClauseId id) { // d_resStack.pop_back(); // } -template <class Solver> +template <class Solver> void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); ClauseId id = registerUnitClause(lit, LEARNT); @@ -716,14 +726,14 @@ void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { } -template <class Solver> +template <class Solver> void TSatProof<Solver>::cancelResChain() { Assert(d_resStack.size() > 0); d_resStack.pop_back(); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); ResChain<Solver>* res = d_resStack.back(); @@ -731,18 +741,18 @@ void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) { } /// constructing resolutions -template <class Solver> +template <class Solver> void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) { ClauseId id = resolveUnit(~lit); ResChain<Solver>* res = d_resStack.back(); res->addStep(lit, id, !sign(lit)); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) { Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; resolveUnit(lit); } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { // first check if we already have a resolution for lit if(isUnit(lit)) { @@ -772,12 +782,12 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { registerResolution(unit_id, res); return unit_id; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::toStream(std::ostream& out) { Debug("proof:sat") << "TSatProof<Solver>::printProof\n"; Unimplemented("native proof printing not supported yet"); } -template <class Solver> +template <class Solver> ClauseId TSatProof<Solver>::storeUnitConflict(typename Solver::TLit conflict_lit, ClauseKind kind) { Debug("cores") << "STORE UNIT CONFLICT" << std::endl; @@ -787,7 +797,7 @@ ClauseId TSatProof<Solver>::storeUnitConflict(typename Solver::TLit conflict_lit Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; return d_unitConflictId; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { Assert(d_resStack.size() == 0); Assert(conflict_ref != Solver::TCRef_Undef); @@ -829,7 +839,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { } /// CRef manager -template <class Solver> +template <class Solver> void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { if (d_clauseId.find(oldref) == d_clauseId.end()) { @@ -841,7 +851,7 @@ void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref, d_temp_clauseId[newref] = id; d_temp_idClause[id] = newref; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::finishUpdateCRef() { d_clauseId.swap(d_temp_clauseId); d_temp_clauseId.clear(); @@ -849,7 +859,7 @@ void TSatProof<Solver>::finishUpdateCRef() { d_idClause.swap(d_temp_idClause); d_temp_idClause.clear(); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { if (d_clauseId.find(clause) != d_clauseId.end()) { ClauseId id = getClauseId(clause); @@ -867,18 +877,18 @@ void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { // template<> // void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, // prop::SatClause& sat_cl) { - + // prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); // } -template <class Solver> +template <class Solver> void TSatProof<Solver>::constructProof(ClauseId conflict) { collectClauses(conflict); } -template <class Solver> +template <class Solver> std::string TSatProof<Solver>::clauseName(ClauseId id) { std::ostringstream os; if (isInputClause(id)) { @@ -894,7 +904,7 @@ std::string TSatProof<Solver>::clauseName(ClauseId id) { } } -template <class Solver> +template <class Solver> prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { if (isUnit(id)) { typename Solver::TLit lit = getUnit(id); @@ -916,7 +926,7 @@ prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { return clause; } -template <class Solver> +template <class Solver> void TSatProof<Solver>::collectClauses(ClauseId id) { if (d_seenInputs.find(id) != d_seenInputs.end() || d_seenLemmas.find(id) != d_seenLemmas.end() || @@ -949,7 +959,7 @@ void TSatProof<Solver>::collectClauses(ClauseId id) { } } -template <class Solver> +template <class Solver> void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas) { inputs = d_seenInputs; @@ -960,13 +970,13 @@ void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs, ); } -template <class Solver> +template <class Solver> void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) { Assert (d_glueMap.find(clause) == d_glueMap.end()); d_glueMap.insert(std::make_pair(clause, glue)); } -template <class Solver> +template <class Solver> TSatProof<Solver>::Statistics::Statistics(const std::string& prefix) : d_numLearnedClauses("satproof::"+prefix+"::NumLearnedClauses", 0) , d_numLearnedInProof("satproof::"+prefix+"::NumLearnedInProof", 0) @@ -986,7 +996,7 @@ TSatProof<Solver>::Statistics::Statistics(const std::string& prefix) smtStatisticsRegistry()->registerStat(&d_usedClauseGlue); } -template <class Solver> +template <class Solver> TSatProof<Solver>::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses); smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof); @@ -1000,7 +1010,7 @@ TSatProof<Solver>::Statistics::~Statistics() { /// LFSCSatProof class -template <class Solver> +template <class Solver> void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { out << "(satlem_simplify _ _ _ "; @@ -1030,7 +1040,7 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std:: } /// LFSCSatProof class -template <class Solver> +template <class Solver> void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) { Assert (this->isAssumptionConflict(id)); // print the resolution proving the assumption conflict @@ -1038,7 +1048,7 @@ void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, std::ostream& // resolve out assumptions to prove empty clause out << "(satlem_simplify _ _ _ "; std::vector<typename Solver::TLit>& confl = *(this->d_assumptionConflictsDebug[id]); - + Assert (confl.size()); for (unsigned i = 0; i < confl.size(); ++i) { @@ -1046,8 +1056,8 @@ void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, std::ostream& out <<"("; out << (lit.isNegated() ? "Q" : "R") <<" _ _ "; } - - out << this->clauseName(id)<< " "; + + out << this->clauseName(id)<< " "; for (int i = confl.size() - 1; i >= 0; --i) { prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]); prop::SatVariable v = lit.getSatVariable(); @@ -1074,20 +1084,20 @@ void LFSCSatProof<Solver>::printResolutions(std::ostream& out, std::ostream& par template <class Solver> void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out, std::ostream& paren) { - printResolution(this->d_emptyClauseId, out, paren); + printResolution(this->d_emptyClauseId, out, paren); } inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { switch(k) { case CVC4::INPUT: - out << "INPUT"; + out << "INPUT"; break; case CVC4::THEORY_LEMMA: - out << "THEORY_LEMMA"; + out << "THEORY_LEMMA"; break; case CVC4::LEARNT: - out << "LEARNT"; + out << "LEARNT"; break; default: out << "ClauseKind Unknown! [" << unsigned(k) << "]"; diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp new file mode 100644 index 000000000..526ea8dbb --- /dev/null +++ b/src/proof/skolemization_manager.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file skolemization_manager.cpp + **/ + +#include "proof/skolemization_manager.h" + +namespace CVC4 { + +void SkolemizationManager::registerSkolem(Node disequality, Node skolem) { + Debug("pf::pm") << "SkolemizationManager: registerSkolem: disequality = " << disequality << ", skolem = " << skolem << std::endl; + + if (isSkolem(skolem)) { + Assert(d_skolemToDisequality[skolem] == disequality); + return; + } + + d_disequalityToSkolem[disequality] = skolem; + d_skolemToDisequality[skolem] = disequality; +} + +bool SkolemizationManager::hasSkolem(Node disequality) { + return (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end()); +} + +Node SkolemizationManager::getSkolem(Node disequality) { + Debug("pf::pm") << "SkolemizationManager: getSkolem( "; + Assert (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end()); + Debug("pf::pm") << disequality << " ) = " << d_disequalityToSkolem[disequality] << std::endl; + return d_disequalityToSkolem[disequality]; +} + +Node SkolemizationManager::getDisequality(Node skolem) { + Assert (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); + return d_skolemToDisequality[skolem]; +} + +bool SkolemizationManager::isSkolem(Node skolem) { + return (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); +} + +void SkolemizationManager::clear() { + Debug("pf::pm") << "SkolemizationManager: clear" << std::endl; + d_disequalityToSkolem.clear(); + d_skolemToDisequality.clear(); +} + +std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() { + return d_disequalityToSkolem.begin(); +} + +std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() { + return d_disequalityToSkolem.end(); +} + +} /* CVC4 namespace */ diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h new file mode 100644 index 000000000..649f0bf40 --- /dev/null +++ b/src/proof/skolemization_manager.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file skolemization_manager.h + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SKOLEMIZATION_MANAGER_H +#define __CVC4__SKOLEMIZATION_MANAGER_H + +#include <iostream> +#include <map> +#include "proof/proof.h" +#include "util/proof.h" +#include "expr/node.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" + +namespace CVC4 { + +class SkolemizationManager { +public: + void registerSkolem(Node disequality, Node skolem); + bool hasSkolem(Node disequality); + Node getSkolem(Node disequality); + Node getDisequality(Node skolem); + bool isSkolem(Node skolem); + + void clear(); + + std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin(); + std::hash_map<Node, Node, NodeHashFunction>::const_iterator end(); + +private: + std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem; + std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality; +}; + +}/* CVC4 namespace */ + + + +#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 6a77faab7..efb6e6606 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -19,6 +19,7 @@ #include "base/cvc4_assert.h" #include "context/context.h" #include "options/bv_options.h" +#include "proof/arith_proof.h" #include "proof/array_proof.h" #include "proof/bitvector_proof.h" #include "proof/clause_id.h" @@ -79,13 +80,16 @@ public: return theory::LemmaStatus(TNode::null(), 0); } void requirePhase(TNode n, bool b) throw() { + Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl; Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl; } bool flipDecision() throw() { + Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl; AlwaysAssert(false); return false; } void setIncomplete() throw() { + Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl; AlwaysAssert(false); } };/* class ProofOutputChannel */ @@ -146,11 +150,18 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); return; } + if (id == theory::THEORY_ARRAY) { d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this); return; } - // TODO other theories + + if (id == theory::THEORY_ARITH) { + d_theoryProofTable[id] = new LFSCArithProof((theory::arith::TheoryArith*)th, this); + return; + } + + // TODO other theories } } } @@ -164,9 +175,12 @@ void TheoryProofEngine::registerTerm(Expr term) { if (d_registrationCache.count(term)) { return; } + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); + Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; + // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || term.getKind() == kind::ITE) { @@ -178,20 +192,33 @@ void TheoryProofEngine::registerTerm(Expr term) { } if (!supportedTheory(theory_id)) return; - + getTheoryProof(theory_id)->registerTerm(term); d_registrationCache.insert(term); } theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { - // TODO: now CNF proof has a map from formula to proof rule - // that should be checked to figure out what theory is responsible for this ProofManager* pm = ProofManager::currentPM(); - if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; - if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; - if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; - Unreachable(); + Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" + << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + + if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) { + Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. " + << "Returning THEORY_ARITH" << std::endl; + return theory::THEORY_ARITH; + } + + return pm->getCnfProof()->getOwnerTheory(id); + + // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; + // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; + // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY; + // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; + + // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl; + + // Unreachable(); } void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { @@ -245,6 +272,9 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) { theory::TheoryId theory_id = theory::Theory::theoryOf(term); + Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term + << ", theory_id = " << theory_id << std::endl; + // boolean terms and ITEs are special because they // are common to all theories if (theory_id == theory::THEORY_BUILTIN || @@ -254,39 +284,55 @@ void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const L return; } // dispatch to proper theory - getTheoryProof(theory_id)->printTerm(term, os, map); + getTheoryProof(theory_id)->printOwnedTerm(term, os, map); } void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) { if (type.isSort()) { - getTheoryProof(theory::THEORY_UF)->printSort(type, os); + getTheoryProof(theory::THEORY_UF)->printOwnedSort(type, os); return; } if (type.isBitVector()) { - getTheoryProof(theory::THEORY_BV)->printSort(type, os); + getTheoryProof(theory::THEORY_BV)->printOwnedSort(type, os); return; } if (type.isArray()) { - getTheoryProof(theory::THEORY_ARRAY)->printSort(type, os); + getTheoryProof(theory::THEORY_ARRAY)->printOwnedSort(type, os); return; } + + if (type.isInteger() || type.isReal()) { + getTheoryProof(theory::THEORY_ARITH)->printOwnedSort(type, os); + return; + } + + if (type.isBoolean()) { + getTheoryProof(theory::THEORY_BOOL)->printOwnedSort(type, os); + return; + } + Unreachable(); } -void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { - unsigned counter = 0; +void LFSCTheoryProofEngine::registerTermsFromAssertions() { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); - // collect declarations first for(; it != end; ++it) { registerTerm(*it); } - printDeclarations(os, paren); +} + +void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl << std::endl; + + unsigned counter = 0; + ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); + ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); - it = ProofManager::currentPM()->begin_assertions(); for (; it != end; ++it) { + Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; // FIXME: merge this with counter os << "(% A" << counter++ << " (th_holds "; printLetTerm(*it, os); @@ -295,13 +341,40 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare } //store map between assertion and counter // ProofManager::currentPM()->setAssertion( *it ); + Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl; } -void LFSCTheoryProofEngine::printDeclarations(std::ostream& os, std::ostream& paren) { +void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl; + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); TheoryProofTable::const_iterator end = d_theoryProofTable.end(); for (; it != end; ++it) { - it->second->printDeclarations(os, paren); + it->second->printSortDeclarations(os, paren); + } + + Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations done" << std::endl << std::endl; +} + +void LFSCTheoryProofEngine::printTermDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printTermDeclarations called" << std::endl << std::endl; + + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->printTermDeclarations(os, paren); + } + + Debug("pf::tp") << "LFSCTheoryProofEngine::printTermDeclarations done" << std::endl << std::endl; +} + +void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printDeferredDeclarations called" << std::endl; + + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->printDeferredDeclarations(os, paren); } } @@ -313,6 +386,16 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, IdToSatClause::const_iterator it = lemmas.begin(); IdToSatClause::const_iterator end = lemmas.end(); + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; + + for (; it != end; ++it) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; + ClauseId id = it->first; + Debug("pf::tp") << "\tLemma = " << id + << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + } + it = lemmas.begin(); + // BitVector theory is special case: must know all // conflicts needed ahead of time for resolution // proof lemmas @@ -353,13 +436,22 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, it = lemmas.begin(); + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; + for (; it != end; ++it) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl; + + // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl; ClauseId id = it->first; + Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl; const prop::SatClause* clause = it->second; // printing clause as it appears in resolution proof os << "(satlem _ _ "; std::ostringstream clause_paren; + + Debug("pf::tp") << "CnfProof printing clause..." << std::endl; pm->getCnfProof()->printClause(*clause, os, clause_paren); + Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl; std::vector<Expr> clause_expr; for(unsigned i = 0; i < clause->size(); ++i) { @@ -373,10 +465,14 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, clause_expr.push_back(expr_lit); } + Debug("pf::tp") << "Expression printing done!" << std::endl; + // query appropriate theory for proof of clause theory::TheoryId theory_id = getTheoryForLemma(id); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl; getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; // os << " (clausify_false trust)"; os << clause_paren.str(); os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; @@ -385,15 +481,19 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { + // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; + LetMap::const_iterator it = map.find(term); - Assert (it != map.end()); - unsigned id = it->second.id; - unsigned count = it->second.count; - if (count > LET_COUNT) { - os <<"let"<<id; - return; + if (it != map.end()) { + unsigned id = it->second.id; + unsigned count = it->second.count; + if (count > LET_COUNT) { + os <<"let"<<id; + return; + } } - printTheoryTerm(term, os, map); + + printTheoryTerm(term, os, map); } void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) { @@ -513,32 +613,83 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); + } else if (d_theory->getId() == theory::THEORY_ARITH) { + Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl; + os << " (clausify_false trust)"; + return; } else { InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic()); } + + Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->ProduceProofs()" << std::endl; th->produceProofs(); + Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl; + MyPreRegisterVisitor preRegVisitor(th); for( unsigned i=0; i<lemma.size(); i++ ){ Node lit = Node::fromExpr( lemma[i] ).negate(); - Trace("theory-proof-debug") << "; preregistering and asserting " << lit << std::endl; + Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit); th->assertFact(lit, false); } + + Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl; th->check(theory::Theory::EFFORT_FULL); + Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->check() DONE" << std::endl; + if(oc.d_conflict.isNull()) { - Trace("theory-proof-debug") << "; conflict is null" << std::endl; + Trace("pf::tp") << "; conflict is null" << std::endl; Assert(!oc.d_lemma.isNull()); - Trace("theory-proof-debug") << "; ++ but got lemma: " << oc.d_lemma << std::endl; - Trace("theory-proof-debug") << "; asserting " << oc.d_lemma[1].negate() << std::endl; - th->assertFact(oc.d_lemma[1].negate(), false); + Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl; + + // Original, as in Liana's branch + // Trace("pf::tp") << "; asserting " << oc.d_lemma[1].negate() << std::endl; + // th->assertFact(oc.d_lemma[1].negate(), false); + // th->check(theory::Theory::EFFORT_FULL); + + // Altered version, to handle OR lemmas + + if (oc.d_lemma.getKind() == kind::OR) { + Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl; + for (unsigned i = 0; i < oc.d_lemma.getNumChildren(); ++i) { + if (oc.d_lemma[i].getKind() == kind::NOT) { + Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[i][0] << std::endl; + th->assertFact(oc.d_lemma[i][0], false); + } + else { + Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[i].notNode() << std::endl; + th->assertFact(oc.d_lemma[i].notNode(), false); + } + } + } + else { + Unreachable(); + + Assert(oc.d_lemma.getKind() == kind::NOT); + Debug("pf::tp") << "NOT lemma" << std::endl; + Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[0] << std::endl; + th->assertFact(oc.d_lemma[0], false); + } + + // Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl; + // Trace("pf::tp") << "; asserting " << oc.d_lemma[1].negate() << std::endl; + // th->assertFact(oc.d_lemma[1].negate(), false); + + // th->check(theory::Theory::EFFORT_FULL); } + Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; oc.d_proof->toStream(os); + Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; + + Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl; delete th; + Debug("pf::tp") << "About to delete the theory solver used for proving the lemma: DONE! " << std::endl; } bool TheoryProofEngine::supportedTheory(theory::TheoryId id) { return (id == theory::THEORY_ARRAY || + id == theory::THEORY_ARITH || id == theory::THEORY_BV || id == theory::THEORY_UF || id == theory::THEORY_BOOL); @@ -560,7 +711,7 @@ void BooleanProof::registerTerm(Expr term) { } } -void LFSCBooleanProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { os << "(p_app " << ProofManager::sanitize(term) <<")"; @@ -611,11 +762,16 @@ void LFSCBooleanProof::printTerm(Expr term, std::ostream& os, const LetMap& map) } -void LFSCBooleanProof::printSort(Type type, std::ostream& os) { +void LFSCBooleanProof::printOwnedSort(Type type, std::ostream& os) { Assert (type.isBoolean()); os << "Bool"; } -void LFSCBooleanProof::printDeclarations(std::ostream& os, std::ostream& paren) { + +void LFSCBooleanProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + +void LFSCBooleanProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { Expr term = *it; @@ -626,6 +782,10 @@ void LFSCBooleanProof::printDeclarations(std::ostream& os, std::ostream& paren) } } +void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index d14704760..b04dd4c60 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -39,14 +39,14 @@ struct LetCount { static unsigned counter; static void resetCounter() { counter = 0; } static unsigned newId() { return ++counter; } - + unsigned count; unsigned id; LetCount() : count(0) , id(-1) {} - + void increment() { ++count; } LetCount(unsigned i) : count(1) @@ -65,7 +65,7 @@ struct LetCount { count = rhs.count; return *this; } -}; +}; struct LetOrderElement { Expr expr; @@ -84,7 +84,7 @@ struct LetOrderElement { typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap; -typedef std::vector<LetOrderElement> Bindings; +typedef std::vector<LetOrderElement> Bindings; class TheoryProof; @@ -124,6 +124,14 @@ public: virtual void printSort(Type type, std::ostream& os) = 0; /** + * Go over the assertions and register all terms with the theories. + * + * @param os + * @param paren closing parenthesis + */ + virtual void registerTermsFromAssertions() = 0; + + /** * Print the theory assertions (arbitrary formulas over * theory atoms) * @@ -131,6 +139,14 @@ public: * @param paren closing parenthesis */ virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + /** + * Print variable declarations that need to appear within the proof, + * e.g. skolemized variables. + * + * @param os + * @param paren closing parenthesis + */ + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; /** * Print proofs of all the theory lemmas (must prove @@ -168,11 +184,14 @@ public: LFSCTheoryProofEngine() : TheoryProofEngine() {} - void printDeclarations(std::ostream& os, std::ostream& paren); + void registerTermsFromAssertions(); + void printSortDeclarations(std::ostream& os, std::ostream& paren); + void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printLetTerm(Expr term, std::ostream& os); virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printAssertions(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); @@ -189,41 +208,74 @@ public: : d_theory(th) , d_proofEngine(proofEngine) {} - virtual ~TheoryProof() {}; - /** - * Print a term belonging to this theory. - * + virtual ~TheoryProof() {}; + /** + * Print a term belonging some theory, not neccessarily this one. + * * @param term expresion representing term * @param os output stream */ - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - /** - * Print the proof representation of the given type. - * - * @param type - * @param os + void printTerm(Expr term, std::ostream& os, const LetMap& map) { + d_proofEngine->printBoundTerm(term, os, map); + } + /** + * Print a term belonging to THIS theory. + * + * @param term expresion representing term + * @param os output stream + */ + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + /** + * Print the proof representation of the given type that belongs to some theory. + * + * @param type + * @param os */ - virtual void printSort(Type type, std::ostream& os) = 0; - /** + void printSort(Type type, std::ostream& os) { + d_proofEngine->printSort(type, os); + } + /** + * Print the proof representation of the given type that belongs to THIS theory. + * + * @param type + * @param os + */ + virtual void printOwnedSort(Type type, std::ostream& os) = 0; + /** * Print a proof for the theory lemmas. Must prove * clause representing lemmas to be used in resolution proof. - * + * * @param os output stream */ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - /** - * Print the variable/sorts declarations for this theory. - * - * @param os - * @param paren + /** + * Print the sorts declarations for this theory. + * + * @param os + * @param paren */ - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; - /** + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print the term declarations for this theory. + * + * @param os + * @param paren + */ + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print any deferred variable/sorts declarations for this theory + * (those that need to appear inside the actual proof). + * + * @param os + * @param paren + */ + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** * Register a term of this theory that appears in the proof. - * - * @param term + * + * @param term */ - virtual void registerTerm(Expr term) = 0; + virtual void registerTerm(Expr term) = 0; }; class BooleanProof : public TheoryProof { @@ -233,12 +285,14 @@ public: BooleanProof(TheoryProofEngine* proofEngine); virtual void registerTerm(Expr term); - - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - virtual void printSort(Type type, std::ostream& os) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + + virtual void printOwnedSort(Type type, std::ostream& os) = 0; virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0; - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; }; class LFSCBooleanProof : public BooleanProof { @@ -246,13 +300,14 @@ public: LFSCBooleanProof(TheoryProofEngine* proofEngine) : BooleanProof(proofEngine) {} - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); - virtual void printSort(Type type, std::ostream& os); + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); }; - } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index ec0d90ae7..6a6f8d906 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -21,10 +21,7 @@ #include "theory/uf/theory_uf.h" #include <stack> -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; - +namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); @@ -32,14 +29,14 @@ inline static Node eqNode(TNode n1, TNode n2) { // congrence matching term helper inline static bool match(TNode n1, TNode n2) { - Debug("mgd") << "match " << n1 << " " << n2 << std::endl; + Debug("pf::uf") << "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::uf") << "+ match " << n1 << " " << n2 << std::endl; if(n1 == n2) { return true; } @@ -77,6 +74,7 @@ void ProofUF::toStream(std::ostream& out) { } void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) { + Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl; Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl; pf->debug_print("lfsc-uf"); Debug("lfsc-uf") << std::endl; @@ -84,18 +82,18 @@ void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqPr } Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) { - Debug("gk::proof") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("gk::proof"); - Debug("gk::proof") << std::endl; + Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; + pf->debug_print("pf::uf"); + Debug("pf::uf") << std::endl; if(tb == 0) { - Assert(pf->d_id == eq::MERGED_THROUGH_TRANS); + 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 = eq::MERGED_THROUGH_TRANS; + subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS; subTrans.d_node = pf->d_node; size_t i = 0; @@ -108,38 +106,38 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } // Handle congruence closures over equalities. - else if (pf->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { - Debug("gk::proof") << "Handling congruence over equalities" << std::endl; + else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + Debug("pf::uf") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. std::vector<const theory::eq::EqProof *> congruenceClosures; unsigned count; - Debug("gk::proof") << "Collecting congruence sequence" << std::endl; + Debug("pf::uf") << "Collecting congruence sequence" << std::endl; for (count = 0; i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==eq::MERGED_THROUGH_CONGRUENCE && + pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i + count]->d_node.isNull(); ++count) { - Debug("gk::proof") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("gk::proof"); + Debug("pf::uf") << "Found a congruence: " << std::endl; + pf->d_children[i+count]->debug_print("pf::uf"); congruenceClosures.push_back(pf->d_children[i+count]); } - Debug("gk::proof") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; + Debug("pf::uf") << "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("gk::proof") << "Target does not appear before" << std::endl; + Debug("pf::uf") << "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("gk::proof") << "Target does not appear after" << std::endl; + Debug("pf::uf") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -162,16 +160,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // 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 != eq::MERGED_THROUGH_REFLEXIVITY) + 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 != eq::MERGED_THROUGH_REFLEXIVITY) + 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 != eq::MERGED_THROUGH_REFLEXIVITY) + 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 != eq::MERGED_THROUGH_REFLEXIVITY) + 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]); } } @@ -197,22 +195,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Node n1; std::stringstream ss; //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); - Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; + Debug("pf::uf") << "\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; + Debug("pf::uf") << "\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); out << "(clausify_false (contra _ "; - Debug("mgdx") << "\nhave proven: " << n1 << std::endl; - Debug("mgdx") << "n2 is " << n2[0] << std::endl; + Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; + Debug("pf::uf") << "n2 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 (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } if(n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; @@ -232,44 +230,44 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } switch(pf->d_id) { - case eq::MERGED_THROUGH_CONGRUENCE: { - Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd"); + case theory::eq::MERGED_THROUGH_CONGRUENCE: { + Debug("pf::uf") << "\nok, looking at congruence:\n"; + pf->debug_print("pf::uf"); std::stack<const theory::eq::EqProof*> stk; - for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + 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::STORE); Assert(pf2->d_children.size() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); - Assert(pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE); + 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"); - Debug("mgd") << "looking at " << pf2->d_node << "\n"; - Debug("mgd") << " " << n1 << "\n"; - Debug("mgd") << " " << n2 << "\n"; + Debug("pf::uf") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; + pf2->debug_print("pf::uf"); + Debug("pf::uf") << "looking at " << pf2->d_node << "\n"; + Debug("pf::uf") << " " << n1 << "\n"; + Debug("pf::uf") << " " << n2 << "\n"; int side = 0; if(match(pf2->d_node, n1[0])) { //if(tb == 1) { - Debug("mgd") << "SIDE IS 0\n"; + Debug("pf::uf") << "SIDE IS 0\n"; //} side = 0; } else { //if(tb == 1) { - Debug("mgd") << "SIDE IS 1\n"; + Debug("pf::uf") << "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"); + Debug("pf::uf") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("pf::uf"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -294,11 +292,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } 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; - Debug("mgd") << "side " << side << std::endl; + Debug("pf::uf") << "pf2->d_node " << pf2->d_node << std::endl; + Debug("pf::uf") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl; + Debug("pf::uf") << "n1 " << n1 << std::endl; + Debug("pf::uf") << "n2 " << n2 << std::endl; + Debug("pf::uf") << "side " << side << std::endl; if(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) { b1 << n2[side]; b2 << n2[1-side]; @@ -312,20 +310,20 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << ")"; while(!stk.empty()) { if(tb == 1) { - Debug("mgd") << "\nMORE TO DO\n"; + Debug("pf::uf") << "\nMORE TO DO\n"; } pf2 = stk.top(); stk.pop(); - Assert(pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE); + 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"; + Debug("pf::uf") << "\nok, in cong[" << stk.size() << "]" << "\n"; + Debug("pf::uf") << "looking at " << pf2->d_node << "\n"; + Debug("pf::uf") << " " << n1 << "\n"; + Debug("pf::uf") << " " << n2 << "\n"; + Debug("pf::uf") << " " << b1 << "\n"; + Debug("pf::uf") << " " << b2 << "\n"; if(pf2->d_node[b1.getNumChildren()] == n2[side]) { b1 << n2[side]; b2 << n2[1-side]; @@ -340,7 +338,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } n1 = b1; n2 = b2; - Debug("mgd") << "at end assert, got " << pf2->d_node << " and " << n1 << std::endl; + Debug("pf::uf") << "at end assert, got " << pf2->d_node << " and " << n1 << std::endl; if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) { Assert(n1 == pf2->d_node); } @@ -353,7 +351,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } b1.append(n1.begin(), n1.end()); n1 = b1; - Debug("mgd") << "at[2] end assert, got " << pf2->d_node << " and " << n1 << std::endl; + Debug("pf::uf") << "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); } @@ -370,12 +368,12 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); if(tb == 1) { - Debug("mgdx") << "\ncong proved: " << n << "\n"; + Debug("pf::uf") << "\ncong proved: " << n << "\n"; } return n; } - case eq::MERGED_THROUGH_REFLEXIVITY: + case theory::eq::MERGED_THROUGH_REFLEXIVITY: Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); out << "(refl _ "; @@ -383,33 +381,44 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << ")"; return eqNode(pf->d_node, pf->d_node); - case eq::MERGED_THROUGH_EQUALITY: + case theory::eq::MERGED_THROUGH_EQUALITY: Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); out << ProofManager::getLitName(pf->d_node.negate()); return pf->d_node; - case eq::MERGED_THROUGH_TRANS: { + case theory::eq::MERGED_THROUGH_TRANS: { 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"; + Debug("pf::uf") << "\ndoing trans proof[[\n"; + pf->debug_print("pf::uf"); + Debug("pf::uf") << "\n"; Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); - Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; + Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { - Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; + Debug("pf::uf") << "\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(""); - Node n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + + // 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; + } // The following branch is dedicated to handling sequences of identical equalities, // i.e. trans[ a=b, a=b, a=b ]. @@ -425,13 +434,13 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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("gk::proof") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + Debug("pf::uf") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; if (!identicalEqualities) { // The sequence of identical equalities has started just now identicalEqualities = true; - Debug("gk::proof") << "The sequence is just beginning. Determining length..." << std::endl; + Debug("pf::uf") << "The sequence is just beginning. Determining length..." << std::endl; // Determine whether the length of this sequence is odd or even. evenLengthSequence = true; @@ -455,11 +464,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E if (evenLengthSequence) { // If the length is even, we need to apply transitivity for the "correct" hand of the equality. - Debug("gk::proof") << "Equality sequence of even length" << std::endl; - Debug("gk::proof") << "n1 is: " << n1 << std::endl; - Debug("gk::proof") << "n2 is: " << n2 << std::endl; - Debug("gk::proof") << "pf-d_node is: " << pf->d_node << std::endl; - Debug("gk::proof") << "Next node is: " << nodeAfterEqualitySequence << std::endl; + Debug("pf::uf") << "Equality sequence of even length" << std::endl; + Debug("pf::uf") << "n1 is: " << n1 << std::endl; + Debug("pf::uf") << "n2 is: " << n2 << std::endl; + Debug("pf::uf") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::uf") << "Next node is: " << nodeAfterEqualitySequence << std::endl; ss << "(trans _ _ _ _ "; @@ -472,7 +481,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E n1 = eqNode(n1[1], n1[1]); ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); } else { - Debug("gk::proof") << "Error: identical equalities over, but hands don't match what we're proving." + Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving." << std::endl; Assert(false); } @@ -495,7 +504,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E n1 = eqNode(n1[1], n1[1]); } else { - Debug("gk::proof") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; + Debug("pf::uf") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; Assert(false); } } @@ -503,11 +512,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ss << ")"; } else { - Debug("gk::proof") << "Equality sequence length is odd!" << std::endl; + Debug("pf::uf") << "Equality sequence length is odd!" << std::endl; ss.str(ss1.str()); } - Debug("gk::proof") << "Have proven: " << n1 << std::endl; + Debug("pf::uf") << "Have proven: " << n1 << std::endl; } else { ss.str(ss1.str()); } @@ -522,21 +531,21 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E identicalEqualities = false; } - Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; + Debug("pf::uf") << "\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"; + Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; + Debug("pf::uf") << (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"; + Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; + Debug("pf::uf") << n1[0].getId() << " " << n1[0] << "\n"; + Debug("pf::uf") << n1[1].getId() << " " << n1[1] << "\n"; + Debug("pf::uf") << n2[0].getId() << " " << n2[0] << "\n"; + Debug("pf::uf") << n2[1].getId() << " " << n2[1] << "\n"; + Debug("pf::uf") << (n1[0] == n2[0]) << "\n"; + Debug("pf::uf") << (n1[1] == n2[1]) << "\n"; + Debug("pf::uf") << (n1[0] == n2[1]) << "\n"; + Debug("pf::uf") << (n1[1] == n2[0]) << "\n"; } } ss << "(trans _ _ _ _ "; @@ -546,32 +555,32 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { - if(tb == 1) { Debug("mgdx") << "case 1\n"; } + if(tb == 1) { Debug("pf::uf") << "case 1\n"; } n1 = eqNode(n1[1], n2[1]); ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); } else if(n1[1] == n2[1]) { - if(tb == 1) { Debug("mgdx") << "case 2\n"; } + if(tb == 1) { Debug("pf::uf") << "case 2\n"; } n1 = eqNode(n1[0], n2[0]); ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")"; } else if(n1[0] == n2[1]) { - if(tb == 1) { Debug("mgdx") << "case 3\n"; } + if(tb == 1) { Debug("pf::uf") << "case 3\n"; } n1 = eqNode(n2[0], n1[1]); ss << ss2.str() << " " << ss1.str(); - if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } + if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; } } else if(n1[1] == n2[0]) { - if(tb == 1) { Debug("mgdx") << "case 4\n"; } + if(tb == 1) { Debug("pf::uf") << "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); + pf->debug_print("pf::uf",0); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); } - Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl; + Debug("pf::uf") << "++ 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) { @@ -602,12 +611,15 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ss << ")"; } out << ss.str(); - Debug("mgd") << "\n++ trans proof done, have proven " << n1 << std::endl; + Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl; return n1; } - case eq::MERGED_ARRAYS_ROW: { - Debug("mgd") << "row lemma: " << pf->d_node << std::endl; + case theory::eq::MERGED_ARRAYS_ROW: { + Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl; + Unreachable(); + + Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl; Assert(pf->d_node.getKind() == kind::EQUAL); TNode t1, t2, t3, t4; Node ret; @@ -621,7 +633,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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"; + Debug("pf::uf") << "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 && @@ -633,7 +645,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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"; + Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; } out << "(row _ _ "; tp->printTerm(t2.toExpr(), out, map); @@ -647,8 +659,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E return ret; } - case eq::MERGED_ARRAYS_ROW1: { - Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl; + case theory::eq::MERGED_ARRAYS_ROW1: { + Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl; + Unreachable(); + + Debug("pf::uf") << "row1 lemma: " << pf->d_node << std::endl; Assert(pf->d_node.getKind() == kind::EQUAL); TNode t1, t2, t3; Node ret; @@ -660,7 +675,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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"; + Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; } else { Assert(pf->d_node[0].getKind() == kind::SELECT && pf->d_node[0][0].getKind() == kind::STORE && @@ -670,7 +685,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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"; + Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; } out << "(row1 _ _ "; tp->printTerm(t1.toExpr(), out, map); @@ -685,7 +700,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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; + Debug("pf::uf") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; AlwaysAssert(false); return pf->d_node; } @@ -722,8 +737,10 @@ void UFProof::registerTerm(Expr term) { } } -void LFSCUFProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { - Assert (Theory::theoryOf(term) == THEORY_UF); +void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { + Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; + + Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF); if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM) { @@ -742,7 +759,7 @@ void LFSCUFProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { } os << func << " "; for (unsigned i = 0; i < term.getNumChildren(); ++i) { - printTerm(term[i], os, map); + d_proofEngine->printBoundTerm(term[i], os, map); os << ")"; } if(term.getType().isBoolean()) { @@ -750,7 +767,9 @@ void LFSCUFProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { } } -void LFSCUFProof::printSort(Type type, std::ostream& os) { +void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { + Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; + Assert (type.isSort()); os << type <<" "; } @@ -765,13 +784,17 @@ void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& UFProof::printTheoryLemmaProof( lemma, os, paren ); } -void LFSCUFProof::printDeclarations(std::ostream& os, std::ostream& paren) { - // declaring the sorts +void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { - os << "(% " << *it << " sort\n"; - paren << ")"; + if (!ProofManager::currentPM()->wasPrinted(*it)) { + os << "(% " << *it << " sort\n"; + paren << ")"; + ProofManager::currentPM()->markPrinted(*it); + } } +} +void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { Expr term = *it; @@ -802,3 +825,9 @@ void LFSCUFProof::printDeclarations(std::ostream& os, std::ostream& paren) { paren << ")"; } } + +void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + +} /* namespace CVC4 */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 121db1fcd..5f6d4203a 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -37,7 +37,7 @@ public: static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map); }; - + namespace theory { namespace uf { class TheoryUF; @@ -51,7 +51,7 @@ class UFProof : public TheoryProof { protected: TypeSet d_sorts; // all the uninterpreted sorts in this theory ExprSet d_declarations; // all the variable/function declarations - + public: UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine); @@ -63,10 +63,12 @@ public: LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) : UFProof(uf, proofEngine) {} - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); - virtual void printSort(Type type, std::ostream& os); + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); }; |