summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
authorPaulMeng <baolmeng@gmail.com>2016-04-20 14:43:18 -0500
committerPaulMeng <baolmeng@gmail.com>2016-04-20 14:43:18 -0500
commit904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch)
treed96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/proof
parenta0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff)
update from the master
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/arith_proof.cpp833
-rw-r--r--src/proof/arith_proof.h82
-rw-r--r--src/proof/array_proof.cpp1269
-rw-r--r--src/proof/array_proof.h91
-rw-r--r--src/proof/bitvector_proof.cpp94
-rw-r--r--src/proof/bitvector_proof.h28
-rw-r--r--src/proof/clause_id.h33
-rw-r--r--src/proof/cnf_proof.cpp108
-rw-r--r--src/proof/cnf_proof.h45
-rw-r--r--src/proof/proof.h12
-rw-r--r--src/proof/proof_manager.cpp206
-rw-r--r--src/proof/proof_manager.h58
-rw-r--r--src/proof/proof_utils.cpp26
-rw-r--r--src/proof/proof_utils.h26
-rw-r--r--src/proof/sat_proof.h29
-rw-r--r--src/proof/sat_proof_implementation.h217
-rw-r--r--src/proof/skolemization_manager.cpp68
-rw-r--r--src/proof/skolemization_manager.h55
-rw-r--r--src/proof/theory_proof.cpp244
-rw-r--r--src/proof/theory_proof.h166
-rw-r--r--src/proof/uf_proof.cpp345
-rw-r--r--src/proof/uf_proof.h24
-rw-r--r--src/proof/unsat_core.cpp12
-rw-r--r--src/proof/unsat_core.h12
24 files changed, 3397 insertions, 686 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
new file mode 100644
index 000000000..a1287b667
--- /dev/null
+++ b/src/proof/arith_proof.cpp
@@ -0,0 +1,833 @@
+/********************* */
+/*! \file arith_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ 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..788e4bd86
--- /dev/null
+++ b/src/proof/arith_proof.h
@@ -0,0 +1,82 @@
+/********************* */
+/*! \file arith_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. 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..8aba8dce9
--- /dev/null
+++ b/src/proof/array_proof.cpp
@@ -0,0 +1,1269 @@
+/********************* */
+/*! \file array_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ 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::setRowMergeTag(unsigned tag) {
+ d_reasonRow = tag;
+}
+
+void ProofArray::setRow1MergeTag(unsigned tag) {
+ d_reasonRow1 = tag;
+}
+
+void ProofArray::setExtMergeTag(unsigned tag) {
+ d_reasonExt = tag;
+}
+
+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;
+}
+
+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 == d_reasonExt) {
+ // 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();
+ }
+
+ if (pf->d_id == 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;
+ }
+
+ else if (pf->d_id == 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);
+ }
+
+ else if (pf->d_id == 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;
+ }
+
+ else if (pf->d_id == 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;
+ }
+
+ else if (pf->d_id == d_reasonRow) {
+ 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;
+ }
+ }
+
+ else if (pf->d_id == d_reasonRow1) {
+ 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;
+ }
+
+ else if (pf->d_id == d_reasonExt) {
+ 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;
+ }
+
+ else {
+ 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..fb25c9433 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file array_proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Guy Katz, Liana Hadarean, Tim King
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Arrray proof
**
@@ -23,53 +23,74 @@
#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:
+ Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+ theory::eq::EqProof* pf,
+ unsigned tb,
+ const LetMap& map);
+
+ /** Merge tag for ROW applications */
+ unsigned d_reasonRow;
+ /** Merge tag for ROW1 applications */
+ unsigned d_reasonRow1;
+ /** Merge tag for EXT applications */
+ unsigned d_reasonExt;
+public:
+ ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
+ //it is simply an equality engine proof
+ theory::eq::EqProof *d_proof;
+ void toStream(std::ostream& out);
+ void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
+
+ void registerSkolem(Node equality, Node skolem);
+
+ void setRowMergeTag(unsigned tag);
+ void setRow1MergeTag(unsigned tag);
+ void setExtMergeTag(unsigned tag);
+};
+
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 e067f0bce..b63782226 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -1,23 +1,23 @@
/********************* */
/*! \file bitvector_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
-**/
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \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"
#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/bvminisat.h"
@@ -130,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();
@@ -144,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
@@ -232,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:
@@ -245,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) {
@@ -332,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<<")";
@@ -368,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) {
@@ -382,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
@@ -428,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 << ") ";
@@ -488,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..4a1f4015d 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file bitvector_proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Tim King
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Bitvector proof
**
@@ -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/clause_id.h b/src/proof/clause_id.h
new file mode 100644
index 000000000..c66f8c9f5
--- /dev/null
+++ b/src/proof/clause_id.h
@@ -0,0 +1,33 @@
+/********************* */
+/*! \file clause_id.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definition of ClauseId
+ **
+ ** A ClauseId is a shared identifier between the proofs module and the sat
+ ** solver for a clause.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__CLAUSE_ID_H
+#define __CVC4__PROOF__CLAUSE_ID_H
+
+namespace CVC4 {
+
+/**
+ * A ClauseId is a shared identifier between the proofs module and the sat
+ * solver for a clause.
+ */
+typedef unsigned ClauseId;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROOF__CLAUSE_ID_H */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 884a67856..19e9cbac9 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_proof.cpp
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters, Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
@@ -16,22 +16,23 @@
**/
#include "proof/cnf_proof.h"
-#include "proof/theory_proof.h"
+
+#include "proof/clause_id.h"
#include "proof/proof_manager.h"
-#include "prop/sat_solver_types.h"
-#include "prop/minisat/minisat.h"
+#include "proof/theory_proof.h"
#include "prop/cnf_stream.h"
-
-using namespace CVC4::prop;
+#include "prop/minisat/minisat.h"
+#include "prop/sat_solver_types.h"
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)
@@ -54,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);
@@ -94,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) {
@@ -112,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);
}
@@ -126,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;
@@ -140,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
@@ -158,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();
}
@@ -170,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;
@@ -179,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();
}
@@ -202,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());
@@ -245,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 ";
@@ -255,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 << ")))";
@@ -295,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
@@ -357,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() ){
@@ -377,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) << ") ";
@@ -391,6 +418,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
success = false;
}
}
+
if( success ){
if( base_assertion.getKind()==kind::IMPLIES ){
os_main << "(impl_elim _ _ ";
@@ -420,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;
@@ -431,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;
@@ -729,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 675bd9b9d..a21cb1c0e 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters, Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Morgan Deters
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A manager for CnfProofs.
**
@@ -21,14 +21,13 @@
#ifndef __CVC4__CNF_PROOF_H
#define __CVC4__CNF_PROOF_H
-#include <ext/hash_map>
+#include <ext/hash_map>
#include <ext/hash_set>
#include <iosfwd>
#include "context/cdhashmap.h"
+#include "proof/clause_id.h"
#include "proof/sat_proof.h"
-#include "proof/sat_proof.h"
-#include "util/proof.h"
#include "util/proof.h"
namespace CVC4 {
@@ -44,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:
@@ -55,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,
@@ -104,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();
@@ -116,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,
@@ -155,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.h b/src/proof/proof.h
index 97dad7150..af72ccfa8 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Tim King, Morgan Deters
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Proof macros
**
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index b90d589b8..a3689d746 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -1,34 +1,31 @@
/********************* */
/*! \file proof_manager.cpp
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Morgan Deters
** 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 ]]
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** [[ Add lengthier description here ]]
+
** \todo document this file
- **/
-#include "context/context.h"
+**/
#include "proof/proof_manager.h"
-#include "proof/cnf_proof.h"
-#include "proof/theory_proof.h"
+
+#include "base/cvc4_assert.h"
+#include "context/context.h"
+#include "options/bv_options.h"
#include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
#include "proof/proof_utils.h"
#include "proof/sat_proof_implementation.h"
-#include "options/bv_options.h"
-
-#include "util/proof.h"
-#include "util/hash.h"
-
-#include "base/cvc4_assert.h"
+#include "proof/theory_proof.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt_util/node_visitor.h"
@@ -38,7 +35,8 @@
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/valuation.h"
-
+#include "util/hash.h"
+#include "util/proof.h"
namespace CVC4 {
@@ -107,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);
@@ -119,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);
@@ -212,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)) ||
@@ -321,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);
@@ -336,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;
+
+ 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;
+ 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";
@@ -359,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
@@ -406,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();
@@ -422,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();
}
@@ -438,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) {
@@ -459,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 96c4e1d61..c74aac237 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file proof_manager.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Morgan Deters, Guy Katz
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A manager for Proofs
**
@@ -21,8 +21,11 @@
#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"
#include "theory/logic_info.h"
#include "theory/substitutions.h"
@@ -46,13 +49,12 @@ namespace prop {
class SmtEngine;
-typedef unsigned ClauseId;
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;
@@ -96,8 +99,6 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
typedef std::hash_set<ClauseId> IdHashSet;
-typedef unsigned ClauseId;
-
enum ProofRule {
RULE_GIVEN, /* input assertion */
RULE_DERIVED, /* a "macro" rule */
@@ -107,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 */
@@ -122,6 +123,8 @@ class ProofManager {
ExprSet d_inputCoreFormulas;
ExprSet d_outputCoreFormulas;
+ SkolemizationManager d_skolemizationManager;
+
int d_nextId;
Proof* d_fullProof;
@@ -131,6 +134,8 @@ class ProofManager {
// trace dependences back to unsat core
void traceDeps(TNode n);
+ std::set<Type> d_printedTypes;
+
protected:
LogicInfo d_logic;
@@ -155,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;
@@ -165,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 = "");
@@ -183,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 = "");
@@ -192,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);
@@ -214,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/proof_utils.cpp b/src/proof/proof_utils.cpp
index 47b8a235e..5b04c281d 100644
--- a/src/proof/proof_utils.cpp
+++ b/src/proof/proof_utils.cpp
@@ -1,18 +1,18 @@
/********************* */
/*! \file proof_utils.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
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
**/
#include "proof/proof_utils.h"
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index c27fbe5c2..da10c33a0 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -1,18 +1,18 @@
/********************* */
/*! \file proof_utils.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 [[ Add one-line brief description here ]]
-**
-** [[ Add lengthier description here ]]
-** \todo document this file
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
**/
#include "cvc4_private.h"
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index cd42ab85b..d94b61bf3 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Morgan Deters, Tim King
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Resolution proof
**
@@ -20,21 +20,22 @@
#define __CVC4__SAT__PROOF_H
#include <stdint.h>
+
#include <ext/hash_map>
#include <ext/hash_set>
#include <iosfwd>
#include <set>
#include <sstream>
#include <vector>
+
#include "expr/expr.h"
+#include "proof/clause_id.h"
#include "proof/proof_manager.h"
#include "util/proof.h"
#include "util/statistics_registry.h"
-
namespace CVC4 {
-
class CnfProof;
/**
@@ -123,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;
@@ -240,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.
@@ -296,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 {
@@ -320,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 92645e105..e773e4b47 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_proof_implementation.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Tim King
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Resolution proof
**
@@ -19,30 +19,31 @@
#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H
#define __CVC4__SAT__PROOF_IMPLEMENTATION_H
-#include "proof/sat_proof.h"
+#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
-#include "prop/minisat/minisat.h"
+#include "proof/sat_proof.h"
#include "prop/bvminisat/bvminisat.h"
-#include "prop/minisat/core/Solver.h"
#include "prop/bvminisat/core/Solver.h"
+#include "prop/minisat/core/Solver.h"
+#include "prop/minisat/minisat.h"
#include "prop/sat_solver_types.h"
#include "smt/smt_statistics_registry.h"
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 << " ";
@@ -50,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) {
@@ -61,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 << " ";
@@ -80,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)) {
@@ -94,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++) {
@@ -114,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) {
@@ -133,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);
}
@@ -149,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);
}
@@ -158,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);
@@ -182,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)
@@ -217,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()
@@ -227,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();
@@ -256,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;
@@ -270,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;
@@ -299,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]);
@@ -334,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";
@@ -343,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<<" "
@@ -359,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]);
@@ -385,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;
@@ -436,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();
@@ -467,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());
@@ -483,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);
}
}
@@ -496,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;
@@ -512,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
@@ -564,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;
@@ -578,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)) {
@@ -605,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) {
@@ -636,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);
@@ -661,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);
@@ -676,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);
@@ -684,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);
@@ -694,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);
@@ -703,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);
@@ -715,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();
@@ -730,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)) {
@@ -771,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;
@@ -786,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);
@@ -828,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()) {
@@ -840,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();
@@ -848,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);
@@ -866,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)) {
@@ -893,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);
@@ -915,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() ||
@@ -948,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;
@@ -959,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)
@@ -985,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);
@@ -999,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 _ _ _ ";
@@ -1029,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
@@ -1037,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) {
@@ -1045,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();
@@ -1073,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..12fea82ad
--- /dev/null
+++ b/src/proof/skolemization_manager.cpp
@@ -0,0 +1,68 @@
+/********************* */
+/*! \file skolemization_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
+ **/
+
+#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..de510e514
--- /dev/null
+++ b/src/proof/skolemization_manager.h
@@ -0,0 +1,55 @@
+/********************* */
+/*! \file skolemization_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
+ **/
+
+#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 6679cf896..088275b3f 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1,31 +1,32 @@
/********************* */
/*! \file theory_proof.cpp
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Morgan Deters
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. 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 "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/cnf_proof.h"
+#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
#include "proof/proof_utils.h"
#include "proof/sat_proof.h"
-#include "proof/theory_proof.h"
#include "proof/uf_proof.h"
#include "prop/sat_solver_types.h"
#include "smt/smt_engine.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::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->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::printDeclarations(std::ostream& os, std::ostream& paren) {
+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->printDeclarations(os, paren);
+ 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 d997d6e23..54c86f3f3 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -1,19 +1,18 @@
/********************* */
/*! \file theory_proof.h
-** \verbatim
-** Original author: Liana Hadarean
-** Major contributors: Morgan Deters
-** 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 A manager for UfProofs.
-**
-** A manager for UfProofs.
-**
-**
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
**/
#include "cvc4_private.h"
@@ -21,33 +20,32 @@
#ifndef __CVC4__THEORY_PROOF_H
#define __CVC4__THEORY_PROOF_H
-#include "util/proof.h"
-#include "expr/expr.h"
-#include "prop/sat_solver_types.h"
#include <ext/hash_set>
#include <iosfwd>
+#include "expr/expr.h"
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+#include "util/proof.h"
namespace CVC4 {
namespace theory {
class Theory;
-}
-
-typedef unsigned ClauseId;
+} /* namespace CVC4::theory */
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)
@@ -66,7 +64,7 @@ struct LetCount {
count = rhs.count;
return *this;
}
-};
+};
struct LetOrderElement {
Expr expr;
@@ -85,10 +83,9 @@ 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;
-typedef unsigned ClauseId;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
@@ -126,6 +123,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)
*
@@ -133,6 +138,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
@@ -170,11 +183,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);
@@ -191,41 +207,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 printSort(Type type, std::ostream& os) = 0;
- /**
+ 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
+ */
+ 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 {
@@ -235,12 +284,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 {
@@ -248,13 +299,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..32ca122b0 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -1,18 +1,18 @@
/********************* */
/*! \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
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ ** \todo document this file
+
**/
#include "proof/theory_proof.h"
@@ -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,90 +611,14 @@ 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;
- Assert(pf->d_node.getKind() == kind::EQUAL);
- 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";
- }
- 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 << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")";
- return ret;
- }
-
- case 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;
- }
-
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 +655,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 +677,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 +685,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 +702,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 +743,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..e359eaebd 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file uf_proof.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Guy Katz, Tim King
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief UF proof
**
@@ -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);
};
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 2b559d117..4c940e4be 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file unsat_core.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Clark Barrett
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Representation of unsat cores
**
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 8e92fe3d1..a238f0a6a 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file unsat_core.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Liana Hadarean
** 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback