From a99f5aaa46702a4894aaddeed3a7ff5cbf69bdfd Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 22 Oct 2020 01:19:24 +0200 Subject: [PATCH] (proof-new) Make circuit propagator proof producing (#5318) This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator. --- src/preprocessing/passes/non_clausal_simp.cpp | 12 +- src/theory/booleans/circuit_propagator.cpp | 912 +++++++++++++----- src/theory/booleans/circuit_propagator.h | 105 +- 3 files changed, 712 insertions(+), 317 deletions(-) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index a3650c988..2b788098a 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -93,7 +93,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } Trace("non-clausal-simplify") << "propagating" << std::endl; - if (propagator->propagate()) + TrustNode conf = propagator->propagate(); + if (!conf.isNull()) { // If in conflict, just return false Trace("non-clausal-simplify") @@ -122,11 +123,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal( SubstitutionMap& newSubstitutions = tnewSubstituions.get(); SubstitutionMap::iterator pos; size_t j = 0; - std::vector& learned_literals = propagator->getLearnedLiterals(); + std::vector& learned_literals = propagator->getLearnedLiterals(); for (size_t i = 0, size = learned_literals.size(); i < size; ++i) { // Simplify the literal we learned wrt previous substitutions - Node learnedLiteral = learned_literals[i]; + Node learnedLiteral = learned_literals[i].getNode(); Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral); Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral); Trace("non-clausal-simplify") @@ -164,7 +165,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { // If the learned literal simplifies to false, we're in conflict Trace("non-clausal-simplify") - << "conflict with " << learned_literals[i] << std::endl; + << "conflict with " << learned_literals[i].getNode() << std::endl; Assert(!options::unsatCores()); assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst(false); @@ -385,7 +386,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0; i < learned_literals.size(); ++i) { - Node learned = learned_literals[i]; + Node learned = learned_literals[i].getNode(); Assert(top_level_substs.apply(learned) == learned); Node learnedNew = newSubstitutions.apply(learned); if (learned != learnedNew) @@ -452,7 +453,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } // namespace passes - /* -------------------------------------------------------------------------- */ } // namespace passes diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index f49c41346..270c0b9a9 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -16,11 +16,12 @@ #include "theory/booleans/circuit_propagator.h" +#include #include #include -#include #include "expr/node_algorithm.h" +#include "theory/booleans/proof_circuit_propagator.h" #include "util/utility.h" using namespace std; @@ -29,29 +30,167 @@ namespace CVC4 { namespace theory { namespace booleans { +CircuitPropagator::CircuitPropagator(bool enableForward, bool enableBackward) + : d_context(), + d_propagationQueue(), + d_propagationQueueClearer(&d_context, d_propagationQueue), + d_conflict(&d_context, TrustNode()), + d_learnedLiterals(), + d_learnedLiteralClearer(&d_context, d_learnedLiterals), + d_backEdges(), + d_backEdgesClearer(&d_context, d_backEdges), + d_seen(&d_context), + d_state(&d_context), + d_forwardPropagation(enableForward), + d_backwardPropagation(enableBackward), + d_needsFinish(false), + d_pnm(nullptr), + d_epg(nullptr), + d_proofInternal(nullptr), + d_proofExternal(nullptr) +{ +} + +void CircuitPropagator::finish() +{ + Trace("circuit-prop") << "FINISH" << std::endl; + d_context.pop(); +} + void CircuitPropagator::assertTrue(TNode assertion) { - if (assertion.getKind() == kind::AND) { - for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) { - assertTrue(assertion[i]); + Trace("circuit-prop") << "TRUE: " << assertion << std::endl; + if (assertion.getKind() == kind::CONST_BOOLEAN && !assertion.getConst()) + { + makeConflict(assertion); + } + else if (assertion.getKind() == kind::AND) + { + ProofCircuitPropagatorBackward prover{d_pnm, assertion, true}; + if (isProofEnabled()) + { + addProof(assertion, prover.assume(assertion)); + } + for (auto it = assertion.begin(); it != assertion.end(); ++it) + { + addProof(*it, prover.andTrue(it)); + assertTrue(*it); } - } else { + } + else + { // Analyze the assertion for back-edges and all that computeBackEdges(assertion); // Assign the given assertion to true - assignAndEnqueue(assertion, true); + if (isProofEnabled()) + { + assignAndEnqueue(assertion, true, d_pnm->mkAssume(assertion)); + } + else + { + assignAndEnqueue(assertion, true, nullptr); + } } } -void CircuitPropagator::computeBackEdges(TNode node) { +void CircuitPropagator::assignAndEnqueue(TNode n, + bool value, + std::shared_ptr proof) +{ + Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " + << (value ? "true" : "false") << ")" << std::endl; + + if (n.getKind() == kind::CONST_BOOLEAN) + { + // Assigning a constant to the opposite value is dumb + if (value != n.getConst()) + { + makeConflict(n); + return; + } + } - Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl; + if (isProofEnabled()) + { + if (proof == nullptr) + { + Warning() << "CircuitPropagator: Proof is missing for " << n << std::endl; + Assert(false); + } + else + { + Assert(!proof->getResult().isNull()); + Node expected = value ? Node(n) : n.negate(); + if (proof->getResult() != expected) + { + Warning() << "CircuitPropagator: Incorrect proof: " << expected + << " vs. " << proof->getResult() << std::endl + << *proof << std::endl; + } + addProof(expected, std::move(proof)); + } + } + + // Get the current assignment + AssignmentStatus state = d_state[n]; + + if (state != UNASSIGNED) + { + // If the node is already assigned we might have a conflict + if (value != (state == ASSIGNED_TO_TRUE)) + { + makeConflict(n); + } + } + else + { + // If unassigned, mark it as assigned + d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; + // Add for further propagation + d_propagationQueue.push_back(n); + } +} + +void CircuitPropagator::makeConflict(Node n) +{ + auto bfalse = NodeManager::currentNM()->mkConst(false); + ProofGenerator* g = nullptr; + if (isProofEnabled()) + { + if (d_epg->hasProofFor(bfalse)) + { + return; + } + ProofCircuitPropagator pcp(d_pnm); + if (n == bfalse) + { + d_epg->setProofFor(bfalse, pcp.assume(bfalse)); + } + else + { + d_epg->setProofFor(bfalse, + pcp.conflict(pcp.assume(n), pcp.assume(n.negate()))); + } + g = d_proofInternal.get(); + Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse) + << std::endl; + Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse) + << std::endl; + } + d_conflict = TrustNode::mkTrustLemma(bfalse, g); +} + +void CircuitPropagator::computeBackEdges(TNode node) +{ + Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" + << endl; // Vector of nodes to visit vector toVisit; // Start with the top node - if (d_seen.find(node) == d_seen.end()) { + if (d_seen.find(node) == d_seen.end()) + { toVisit.push_back(node); d_seen.insert(node); } @@ -60,20 +199,28 @@ void CircuitPropagator::computeBackEdges(TNode node) { d_backEdges[node]; // Go through the visit list - for (unsigned i = 0; i < toVisit.size(); ++ i) { + for (unsigned i = 0; i < toVisit.size(); ++i) + { // Node we need to visit TNode current = toVisit[i]; - Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl; + Debug("circuit-prop") + << "CircuitPropagator::computeBackEdges(): processing " << current + << endl; Assert(d_seen.find(current) != d_seen.end()); // If this not an atom visit all the children and compute the back edges - if (Theory::theoryOf(current) == THEORY_BOOL) { - for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) { + if (Theory::theoryOf(current) == THEORY_BOOL) + { + for (unsigned child = 0, child_end = current.getNumChildren(); + child < child_end; + ++child) + { TNode childNode = current[child]; // Add the back edge d_backEdges[childNode].push_back(current); // Add to the queue if not seen yet - if (d_seen.find(childNode) == d_seen.end()) { + if (d_seen.find(childNode) == d_seen.end()) + { toVisit.push_back(childNode); d_seen.insert(childNode); } @@ -82,124 +229,204 @@ void CircuitPropagator::computeBackEdges(TNode node) { } } -void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { - - Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl; +void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) +{ + Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent + << ", " << parentAssignment << ")" << endl; + ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment}; // backward rules - switch(parent.getKind()) { - case kind::AND: - if (parentAssignment) { - // AND = TRUE: forall children c, assign(c = TRUE) - for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { - assignAndEnqueue(*i, true); + switch (parent.getKind()) + { + case kind::AND: + if (parentAssignment) + { + // AND = TRUE: forall children c, assign(c = TRUE) + for (TNode::iterator i = parent.begin(), i_end = parent.end(); + i != i_end; + ++i) + { + assignAndEnqueue(*i, true, prover.andTrue(i)); + } } - } else { - // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) - TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); - if (holdout != parent.end()) { - assignAndEnqueue(*holdout, false); + else + { + // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) + TNode::iterator holdout = find_if_unique( + parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout != parent.end()) + { + assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout)); + } } - } - break; - case kind::OR: - if (parentAssignment) { - // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) - TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); - if (holdout != parent.end()) { - assignAndEnqueue(*holdout, true); + break; + case kind::OR: + if (parentAssignment) + { + // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) + TNode::iterator holdout = find_if_unique( + parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout != parent.end()) + { + assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); + } } - } else { - // OR = FALSE: forall children c, assign(c = FALSE) - for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { - assignAndEnqueue(*i, false); + else + { + // OR = FALSE: forall children c, assign(c = FALSE) + for (TNode::iterator i = parent.begin(), i_end = parent.end(); + i != i_end; + ++i) + { + assignAndEnqueue(*i, false, prover.orFalse(i)); + } } - } - break; - case kind::NOT: - // NOT = b: assign(c = !b) - assignAndEnqueue(parent[0], !parentAssignment); - break; - case kind::ITE: - if (isAssignedTo(parent[0], true)) { - // ITE c x y = v: if c is assigned and TRUE, assign(x = v) - assignAndEnqueue(parent[1], parentAssignment); - } else if (isAssignedTo(parent[0], false)) { - // ITE c x y = v: if c is assigned and FALSE, assign(y = v) - assignAndEnqueue(parent[2], parentAssignment); - } else if (isAssigned(parent[1]) && isAssigned(parent[2])) { - if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) - assignAndEnqueue(parent[0], true); - } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) - assignAndEnqueue(parent[0], false); + break; + case kind::NOT: + // NOT = b: assign(c = !b) + assignAndEnqueue( + parent[0], !parentAssignment, prover.Not(!parentAssignment, parent)); + break; + case kind::ITE: + if (isAssignedTo(parent[0], true)) + { + // ITE c x y = v: if c is assigned and TRUE, assign(x = v) + assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true)); } - } - break; - case kind::EQUAL: - Assert(parent[0].getType().isBoolean()); - if (parentAssignment) { - // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) - if (isAssigned(parent[0])) { - assignAndEnqueue(parent[1], getAssignment(parent[0])); - } else if (isAssigned(parent[1])) { - assignAndEnqueue(parent[0], getAssignment(parent[1])); + else if (isAssignedTo(parent[0], false)) + { + // ITE c x y = v: if c is assigned and FALSE, assign(y = v) + assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false)); } - } else { - // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) - if (isAssigned(parent[0])) { - assignAndEnqueue(parent[1], !getAssignment(parent[0])); - } else if (isAssigned(parent[1])) { - assignAndEnqueue(parent[0], !getAssignment(parent[1])); + else if (isAssigned(parent[1]) && isAssigned(parent[2])) + { + if (getAssignment(parent[1]) == parentAssignment + && getAssignment(parent[2]) != parentAssignment) + { + // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and + // y!=v, assign(c = TRUE) + assignAndEnqueue(parent[0], true, prover.iteIsCase(1)); + } + else if (getAssignment(parent[1]) != parentAssignment + && getAssignment(parent[2]) == parentAssignment) + { + // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and + // y==v, assign(c = FALSE) + assignAndEnqueue(parent[0], false, prover.iteIsCase(0)); + } } - } - break; - case kind::IMPLIES: - if (parentAssignment) { - if (isAssignedTo(parent[0], true)) { - // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) - assignAndEnqueue(parent[1], true); + break; + case kind::EQUAL: + Assert(parent[0].getType().isBoolean()); + if (parentAssignment) + { + // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment + // [resp x = y.assignment]) + if (isAssigned(parent[0])) + { + assignAndEnqueue(parent[1], + getAssignment(parent[0]), + prover.eqYFromX(getAssignment(parent[0]), parent)); + } + else if (isAssigned(parent[1])) + { + assignAndEnqueue(parent[0], + getAssignment(parent[1]), + prover.eqXFromY(getAssignment(parent[1]), parent)); + } } - if (isAssignedTo(parent[1], false)) { - // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) - assignAndEnqueue(parent[0], false); + else + { + // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment + // [resp x = !y.assignment]) + if (isAssigned(parent[0])) + { + assignAndEnqueue(parent[1], + !getAssignment(parent[0]), + prover.neqYFromX(getAssignment(parent[0]), parent)); + } + else if (isAssigned(parent[1])) + { + assignAndEnqueue(parent[0], + !getAssignment(parent[1]), + prover.neqXFromY(getAssignment(parent[1]), parent)); + } } - } else { - // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) - assignAndEnqueue(parent[0], true); - assignAndEnqueue(parent[1], false); - } - break; - case kind::XOR: - if (parentAssignment) { - if (isAssigned(parent[0])) { - // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) - assignAndEnqueue(parent[1], !getAssignment(parent[0])); - } else if (isAssigned(parent[1])) { - // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) - assignAndEnqueue(parent[0], !getAssignment(parent[1])); + break; + case kind::IMPLIES: + if (parentAssignment) + { + if (isAssignedTo(parent[0], true)) + { + // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) + assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent)); + } + if (isAssignedTo(parent[1], false)) + { + // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) + assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent)); + } } - } else { - if (isAssigned(parent[0])) { - // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) - assignAndEnqueue(parent[1], getAssignment(parent[0])); - } else if (isAssigned(parent[1])) { - // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) - assignAndEnqueue(parent[0], getAssignment(parent[1])); + else + { + // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) + assignAndEnqueue(parent[0], true, prover.impliesNegX()); + assignAndEnqueue(parent[1], false, prover.impliesNegY()); } - } - break; - default: - Unhandled(); + break; + case kind::XOR: + if (parentAssignment) + { + if (isAssigned(parent[0])) + { + // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) + assignAndEnqueue( + parent[1], + !getAssignment(parent[0]), + prover.xorYFromX( + !parentAssignment, getAssignment(parent[0]), parent)); + } + else if (isAssigned(parent[1])) + { + // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) + assignAndEnqueue( + parent[0], + !getAssignment(parent[1]), + prover.xorXFromY( + !parentAssignment, getAssignment(parent[1]), parent)); + } + } + else + { + if (isAssigned(parent[0])) + { + // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) + assignAndEnqueue( + parent[1], + getAssignment(parent[0]), + prover.xorYFromX( + !parentAssignment, getAssignment(parent[0]), parent)); + } + else if (isAssigned(parent[1])) + { + // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) + assignAndEnqueue( + parent[0], + getAssignment(parent[1]), + prover.xorXFromY( + !parentAssignment, getAssignment(parent[1]), parent)); + } + } + break; + default: Unhandled(); } } - -void CircuitPropagator::propagateForward(TNode child, bool childAssignment) { - +void CircuitPropagator::propagateForward(TNode child, bool childAssignment) +{ // The assignment we have - Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl; + Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child + << ", " << childAssignment << ")" << endl; // Get the back any nodes where this is child const vector& parents = d_backEdges.find(child)->second; @@ -207,165 +434,265 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) { // Go through the parents and see if there is anything to propagate vector::const_iterator parent_it = parents.begin(); vector::const_iterator parent_it_end = parents.end(); - for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) { + for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it) + { // The current parent of the child TNode parent = *parent_it; + Debug("circuit-prop") << "Parent: " << parent << endl; Assert(expr::hasSubterm(parent, child)); + ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent}; + // Forward rules - switch(parent.getKind()) { - case kind::AND: - if (childAssignment) { - TNode::iterator holdout; - holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); - if (holdout == parent.end()) { // all children are assigned TRUE - // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) - assignAndEnqueue(parent, true); - } else if (isAssignedTo(parent, false)) {// the AND is FALSE - // is the holdout unique ? - TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); - if (other == parent.end()) { // the holdout is unique - // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) - assignAndEnqueue(*holdout, false); + switch (parent.getKind()) + { + case kind::AND: + if (childAssignment) + { + TNode::iterator holdout; + holdout = find_if( + parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout == parent.end()) + { // all children are assigned TRUE + // AND ...(x=TRUE)...: if all children now assigned to TRUE, + // assign(AND = TRUE) + assignAndEnqueue(parent, true, prover.andAllTrue()); + } + else if (isAssignedTo(parent, false)) + { // the AND is FALSE + // is the holdout unique ? + TNode::iterator other = find_if( + holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); + if (other == parent.end()) + { // the holdout is unique + // AND ...(x=TRUE)...: if all children BUT ONE now assigned to + // TRUE, and AND == FALSE, assign(last_holdout = FALSE) + assignAndEnqueue( + *holdout, false, prover.andFalse(parent, holdout)); + } } } - } else { - // AND ...(x=FALSE)...: assign(AND = FALSE) - assignAndEnqueue(parent, false); - } - break; - case kind::OR: - if (childAssignment) { - // OR ...(x=TRUE)...: assign(OR = TRUE) - assignAndEnqueue(parent, true); - } else { - TNode::iterator holdout; - holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); - if (holdout == parent.end()) { // all children are assigned FALSE - // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) - assignAndEnqueue(parent, false); - } else if (isAssignedTo(parent, true)) {// the OR is TRUE - // is the holdout unique ? - TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); - if (other == parent.end()) { // the holdout is unique - // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) - assignAndEnqueue(*holdout, true); + else + { + // AND ...(x=FALSE)...: assign(AND = FALSE) + assignAndEnqueue(parent, false, prover.andOneFalse()); + } + break; + case kind::OR: + if (childAssignment) + { + // OR ...(x=TRUE)...: assign(OR = TRUE) + assignAndEnqueue(parent, true, prover.orOneTrue()); + } + else + { + TNode::iterator holdout; + holdout = find_if( + parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout == parent.end()) + { // all children are assigned FALSE + // OR ...(x=FALSE)...: if all children now assigned to FALSE, + // assign(OR = FALSE) + assignAndEnqueue(parent, false, prover.orFalse()); + } + else if (isAssignedTo(parent, true)) + { // the OR is TRUE + // is the holdout unique ? + TNode::iterator other = find_if( + holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); + if (other == parent.end()) + { // the holdout is unique + // OR ...(x=FALSE)...: if all children BUT ONE now assigned to + // FALSE, and OR == TRUE, assign(last_holdout = TRUE) + assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); + } } } - } - break; - - case kind::NOT: - // NOT (x=b): assign(NOT = !b) - assignAndEnqueue(parent, !childAssignment); - break; - - case kind::ITE: - if (child == parent[0]) { - if (childAssignment) { - if (isAssigned(parent[1])) { - // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) - assignAndEnqueue(parent, getAssignment(parent[1])); + break; + + case kind::NOT: + // NOT (x=b): assign(NOT = !b) + assignAndEnqueue( + parent, !childAssignment, prover.Not(childAssignment, parent)); + break; + + case kind::ITE: + if (child == parent[0]) + { + if (childAssignment) + { + if (isAssigned(parent[1])) + { + // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) + assignAndEnqueue(parent, + getAssignment(parent[1]), + prover.iteEvalThen(getAssignment(parent[1]))); + } } - } else { - if (isAssigned(parent[2])) { - // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) - assignAndEnqueue(parent, getAssignment(parent[2])); + else + { + if (isAssigned(parent[2])) + { + // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) + assignAndEnqueue(parent, + getAssignment(parent[2]), + prover.iteEvalElse(getAssignment(parent[2]))); + } } } - } - if (child == parent[1]) { - if (isAssignedTo(parent[0], true)) { - // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) - assignAndEnqueue(parent, childAssignment); + if (child == parent[1]) + { + if (isAssignedTo(parent[0], true)) + { + // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) + assignAndEnqueue( + parent, childAssignment, prover.iteEvalThen(childAssignment)); + } } - } - if (child == parent[2]) { - Assert(child == parent[2]); - if (isAssignedTo(parent[0], false)) { - // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) - assignAndEnqueue(parent, childAssignment); + if (child == parent[2]) + { + Assert(child == parent[2]); + if (isAssignedTo(parent[0], false)) + { + // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) + assignAndEnqueue( + parent, childAssignment, prover.iteEvalElse(childAssignment)); + } } - } - break; - case kind::EQUAL: - Assert(parent[0].getType().isBoolean()); - if (isAssigned(parent[0]) && isAssigned(parent[1])) { - // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment)) - assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1])); - } else { - if (isAssigned(parent)) { - if (child == parent[0]) { - if (getAssignment(parent)) { - // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b) - assignAndEnqueue(parent[1], childAssignment); - } else { - // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b) - assignAndEnqueue(parent[1], !childAssignment); + break; + case kind::EQUAL: + Assert(parent[0].getType().isBoolean()); + if (isAssigned(parent[0]) && isAssigned(parent[1])) + { + // IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=> + // y.assignment)) + assignAndEnqueue(parent, + getAssignment(parent[0]) == getAssignment(parent[1]), + prover.eqEval(getAssignment(parent[0]), + getAssignment(parent[1]))); + } + else + { + if (isAssigned(parent)) + { + if (child == parent[0]) + { + if (getAssignment(parent)) + { + // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b) + assignAndEnqueue(parent[1], + childAssignment, + prover.eqYFromX(childAssignment, parent)); + } + else + { + // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b) + assignAndEnqueue(parent[1], + !childAssignment, + prover.neqYFromX(childAssignment, parent)); + } } - } else { - Assert(child == parent[1]); - if (getAssignment(parent)) { - // IFF x y = b: if IFF is assigned to TRUE, assign(x = b) - assignAndEnqueue(parent[0], childAssignment); - } else { - // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b) - assignAndEnqueue(parent[0], !childAssignment); + else + { + Assert(child == parent[1]); + if (getAssignment(parent)) + { + // IFF x y = b: if IFF is assigned to TRUE, assign(x = b) + assignAndEnqueue(parent[0], + childAssignment, + prover.eqXFromY(childAssignment, parent)); + } + else + { + // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b) + assignAndEnqueue(parent[0], + !childAssignment, + prover.neqXFromY(childAssignment, parent)); + } } } } - } - break; - case kind::IMPLIES: - if (isAssigned(parent[0]) && isAssigned(parent[1])) { - // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) - assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1])); - } else { - if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) { - // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) - assignAndEnqueue(parent[1], true); - } - if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) { - // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) - assignAndEnqueue(parent[0], false); - } - // Note that IMPLIES == FALSE doesn't need any cases here - // because if that assignment has been done, we've already - // propagated all the children (in back-propagation). - } - break; - case kind::XOR: - if (isAssigned(parent)) { - if (child == parent[0]) { - // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) - assignAndEnqueue(parent[1], childAssignment != getAssignment(parent)); - } else { - Assert(child == parent[1]); - // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) - assignAndEnqueue(parent[0], childAssignment != getAssignment(parent)); + break; + case kind::IMPLIES: + if (isAssigned(parent[0]) && isAssigned(parent[1])) + { + // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) + assignAndEnqueue( + parent, + !getAssignment(parent[0]) || getAssignment(parent[1]), + prover.impliesEval(getAssignment(parent[0]), + getAssignment(parent[1]))); } - } - if (isAssigned(parent[0]) && isAssigned(parent[1])) { - assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1])); - } - break; - default: - Unhandled(); + else + { + if (child == parent[0] && childAssignment + && isAssignedTo(parent, true)) + { + // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) + assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent)); + } + if (child == parent[1] && !childAssignment + && isAssignedTo(parent, true)) + { + // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) + assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent)); + } + // Note that IMPLIES == FALSE doesn't need any cases here + // because if that assignment has been done, we've already + // propagated all the children (in back-propagation). + } + break; + case kind::XOR: + if (isAssigned(parent)) + { + if (child == parent[0]) + { + // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) + assignAndEnqueue( + parent[1], + childAssignment != getAssignment(parent), + prover.xorYFromX( + !getAssignment(parent), childAssignment, parent)); + } + else + { + Assert(child == parent[1]); + // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) + assignAndEnqueue( + parent[0], + childAssignment != getAssignment(parent), + prover.xorXFromY( + !getAssignment(parent), childAssignment, parent)); + } + } + if (isAssigned(parent[0]) && isAssigned(parent[1])) + { + assignAndEnqueue(parent, + getAssignment(parent[0]) != getAssignment(parent[1]), + prover.xorEval(getAssignment(parent[0]), + getAssignment(parent[1]))); + } + break; + default: Unhandled(); } } } -bool CircuitPropagator::propagate() { - +TrustNode CircuitPropagator::propagate() +{ Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl; - for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) { - + for (unsigned i = 0; + i < d_propagationQueue.size() && d_conflict.get().isNull(); + ++i) + { // The current node we are propagating TNode current = d_propagationQueue[i]; - Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl; + Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " + << current << std::endl; bool assignment = getAssignment(current); - Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl; + Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " + << (assignment ? "true" : "false") << std::endl; // Is this an atom bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar() @@ -373,17 +700,52 @@ bool CircuitPropagator::propagate() { && (current[0].isVar() && current[1].isVar())); // If an atom, add to the list for simplification - if (atom) { - Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl; - d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode()); + if (atom) + { + Debug("circuit-prop") + << "CircuitPropagator::propagate(): adding to learned: " + << (assignment ? (Node)current : current.notNode()) << std::endl; + Node lit = assignment ? Node(current) : current.notNode(); + + if (isProofEnabled()) + { + if (d_epg->hasProofFor(lit)) + { + // if we have a parent proof generator that provides proofs of the + // inputs to this class, we must use the lazy proof chain + ProofGenerator* pg = d_proofInternal.get(); + if (d_proofExternal != nullptr) + { + d_proofExternal->addLazyStep(lit, pg); + pg = d_proofExternal.get(); + } + TrustNode tlit = TrustNode::mkTrustLemma(lit, pg); + d_learnedLiterals.push_back(tlit); + } + else + { + Warning() << "CircuitPropagator: Proof is missing for " << lit + << std::endl; + TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr); + d_learnedLiterals.push_back(tlit); + } + } + else + { + TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr); + d_learnedLiterals.push_back(tlit); + } + Trace("circuit-prop") << "Added proof for " << lit << std::endl; } // Propagate this value to the children (if not an atom or a constant) - if (d_backwardPropagation && !atom && !current.isConst()) { + if (d_backwardPropagation && !atom && !current.isConst()) + { propagateBackward(current, assignment); } // Propagate this value to the parents - if (d_forwardPropagation) { + if (d_forwardPropagation) + { propagateForward(current, assignment); } } @@ -392,6 +754,48 @@ bool CircuitPropagator::propagate() { return d_conflict; } -}/* CVC4::theory::booleans namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +void CircuitPropagator::setProof(ProofNodeManager* pnm, + context::Context* ctx, + ProofGenerator* defParent) +{ + d_pnm = pnm; + d_epg.reset(new EagerProofGenerator(pnm, ctx)); + d_proofInternal.reset( + new LazyCDProofChain(pnm, true, ctx, d_epg.get(), true)); + if (defParent != nullptr) + { + // If we provide a parent proof generator (defParent), we want the ASSUME + // leafs of proofs provided by this class to call the getProofFor method on + // the parent. To do this, we use a LazyCDProofChain. + d_proofExternal.reset( + new LazyCDProofChain(pnm, true, ctx, defParent, false)); + } +} + +bool CircuitPropagator::isProofEnabled() const +{ + return d_proofInternal != nullptr; +} + +void CircuitPropagator::addProof(TNode f, std::shared_ptr pf) +{ + if (isProofEnabled()) + { + if (!d_epg->hasProofFor(f)) + { + Trace("circuit-prop") << "Adding proof for " << f << std::endl + << "\t" << *pf << std::endl; + d_epg->setProofFor(f, std::move(pf)); + } + else + { + auto prf = d_epg->getProofFor(f); + Trace("circuit-prop") << "Ignoring proof, we already have" << std::endl + << "\t" << *prf << std::endl; + } + } +} + +} // namespace booleans +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 3d22b0015..4c7c2d124 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #include +#include #include #include @@ -27,8 +28,13 @@ #include "context/cdhashset.h" #include "context/cdo.h" #include "context/context.h" +#include "expr/lazy_proof_chain.h" #include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node.h" +#include "theory/eager_proof_generator.h" #include "theory/theory.h" +#include "theory/trust_node.h" #include "util/hash.h" namespace CVC4 { @@ -63,22 +69,7 @@ class CircuitPropagator /** * Construct a new CircuitPropagator. */ - CircuitPropagator(bool enableForward = true, bool enableBackward = true) - : d_context(), - d_propagationQueue(), - d_propagationQueueClearer(&d_context, d_propagationQueue), - d_conflict(&d_context, false), - d_learnedLiterals(), - d_learnedLiteralClearer(&d_context, d_learnedLiterals), - d_backEdges(), - d_backEdgesClearer(&d_context, d_backEdges), - d_seen(&d_context), - d_state(&d_context), - d_forwardPropagation(enableForward), - d_backwardPropagation(enableBackward), - d_needsFinish(false) - { - } + CircuitPropagator(bool enableForward = true, bool enableBackward = true); /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ bool getAssignment(TNode n) const @@ -95,9 +86,10 @@ class CircuitPropagator bool getNeedsFinish() { return d_needsFinish; } - std::vector& getLearnedLiterals() { return d_learnedLiterals; } + std::vector& getLearnedLiterals() { return d_learnedLiterals; } - void finish() { d_context.pop(); } + /** Finish the computation and pop the internal context */ + void finish(); /** Assert for propagation */ void assertTrue(TNode assertion); @@ -107,9 +99,10 @@ class CircuitPropagator * discovered by the propagator are put in the substitutions vector used in * construction. * - * @return true iff conflict found + * @return a trust node encapsulating the proof for a conflict as a lemma that + * proves false, or the null trust node otherwise */ - bool propagate() CVC4_WARN_UNUSED_RESULT; + TrustNode propagate() CVC4_WARN_UNUSED_RESULT; /** * Get the back edges of this circuit. @@ -142,6 +135,15 @@ class CircuitPropagator if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true; return false; } + /** + * Set proof node manager, context and parent proof generator. + * + * If parent is non-null, then it is responsible for the proofs provided + * to this class. + */ + void setProof(ProofNodeManager* pnm, + context::Context* ctx, + ProofGenerator* defParent); private: /** A context-notify object that clears out stale data. */ @@ -206,40 +208,15 @@ class CircuitPropagator * Assign Node in circuit with the value and add it to the queue; note * conflicts. */ - void assignAndEnqueue(TNode n, bool value) - { - Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " - << (value ? "true" : "false") << ")" << std::endl; - - if (n.getKind() == kind::CONST_BOOLEAN) - { - // Assigning a constant to the opposite value is dumb - if (value != n.getConst()) - { - d_conflict = true; - return; - } - } - - // Get the current assignment - AssignmentStatus state = d_state[n]; + void assignAndEnqueue(TNode n, + bool value, + std::shared_ptr proof = nullptr); - if (state != UNASSIGNED) - { - // If the node is already assigned we might have a conflict - if (value != (state == ASSIGNED_TO_TRUE)) - { - d_conflict = true; - } - } - else - { - // If unassigned, mark it as assigned - d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; - // Add for further propagation - d_propagationQueue.push_back(n); - } - } + /** + * Store a conflict for the case that we have derived both n and n.negate() + * to be true. + */ + void makeConflict(Node n); /** * Compute the map from nodes to the nodes that use it. @@ -258,6 +235,9 @@ class CircuitPropagator */ void propagateBackward(TNode parent, bool assignment); + /** Are proofs enabled? */ + bool isProofEnabled() const; + context::Context d_context; /** The propagation queue */ @@ -269,18 +249,18 @@ class CircuitPropagator * but this keeps us safe in case there's still some rubbish around * on the queue. */ - DataClearer > d_propagationQueueClearer; + DataClearer> d_propagationQueueClearer; /** Are we in conflict? */ - context::CDO d_conflict; + context::CDO d_conflict; /** Map of substitutions */ - std::vector d_learnedLiterals; + std::vector d_learnedLiterals; /** * Similar data clearer for learned literals. */ - DataClearer> d_learnedLiteralClearer; + DataClearer> d_learnedLiteralClearer; /** * Back edges from nodes to where they are used. @@ -307,6 +287,17 @@ class CircuitPropagator /* Does the current state require a call to finish()? */ bool d_needsFinish; + /** Adds a new proof for f, or drops it if we already have a proof */ + void addProof(TNode f, std::shared_ptr pf); + + /** A pointer to the proof manager */ + ProofNodeManager* d_pnm; + /** Eager proof generator that actually stores the proofs */ + std::unique_ptr d_epg; + /** Connects the proofs to subproofs internally */ + std::unique_ptr d_proofInternal; + /** Connects the proofs to assumptions externally */ + std::unique_ptr d_proofExternal; }; /* class CircuitPropagator */ } // namespace booleans -- 2.30.2