From 00583622160a91cc2aedc58d00a690bd57306bdc Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 20 Oct 2020 23:32:31 +0200 Subject: [PATCH] (proof-new) Add proofs for circuit propagator (#5301) This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator. It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required. A second PR will use these rules within the circuit propagator class. --- src/CMakeLists.txt | 2 + .../booleans/proof_circuit_propagator.cpp | 587 ++++++++++++++++++ .../booleans/proof_circuit_propagator.h | 213 +++++++ 3 files changed, 802 insertions(+) create mode 100644 src/theory/booleans/proof_circuit_propagator.cpp create mode 100644 src/theory/booleans/proof_circuit_propagator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 29f5a57d4..4d96fa0b3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -444,6 +444,8 @@ libcvc4_add_sources( theory/bags/theory_bags_type_rules.h theory/booleans/circuit_propagator.cpp theory/booleans/circuit_propagator.h + theory/booleans/proof_circuit_propagator.cpp + theory/booleans/proof_circuit_propagator.h theory/booleans/proof_checker.cpp theory/booleans/proof_checker.h theory/booleans/theory_bool.cpp diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp new file mode 100644 index 000000000..bc4e0c8ae --- /dev/null +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -0,0 +1,587 @@ +/********************* */ +/*! \file proof_circuit_propagator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Proofs for the non-clausal circuit propagator. + ** + ** Proofs for the non-clausal circuit propagator. + **/ + +#include "theory/booleans/proof_circuit_propagator.h" + +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +namespace { + +/** Shorthand to create a Node from a constant number */ +template +Node mkRat(T val) +{ + return NodeManager::currentNM()->mkConst(val); +} + +/** + * Collect all children from parent except for one particular child (the + * "holdout"). The holdout is given as iterator, and should be an iterator into + * the [parent.begin(),parent.end()] range. + */ +inline std::vector collectButHoldout(TNode parent, + TNode::iterator holdout) +{ + std::vector lits; + for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; + ++i) + { + if (i != holdout) + { + lits.emplace_back(*i); + } + } + return lits; +} + +} // namespace + +ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm) + : d_pnm(pnm) +{ +} + +bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; } + +std::shared_ptr ProofCircuitPropagator::assume(Node n) +{ + return d_pnm->mkAssume(n); +} + +std::shared_ptr ProofCircuitPropagator::conflict( + const std::shared_ptr& a, const std::shared_ptr& b) +{ + if (a->getResult().notNode() == b->getResult()) + { + return mkProof(PfRule::CONTRA, {a, b}); + } + Assert(a->getResult() == b->getResult().notNode()); + return mkProof(PfRule::CONTRA, {b, a}); +} + +std::shared_ptr ProofCircuitPropagator::andFalse( + Node parent, TNode::iterator holdout) +{ + if (disabled()) + { + return nullptr; + } + return mkNot( + mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}), + collectButHoldout(parent, holdout), + false)); +} + +std::shared_ptr ProofCircuitPropagator::orTrue( + Node parent, TNode::iterator holdout) +{ + if (disabled()) + { + return nullptr; + } + return mkCResolution( + assume(parent), collectButHoldout(parent, holdout), true); +} + +std::shared_ptr ProofCircuitPropagator::Not(bool negate, Node parent) +{ + if (disabled()) + { + return nullptr; + } + return mkNot(assume(negate ? Node(parent[0]) : parent)); +} + +std::shared_ptr ProofCircuitPropagator::impliesXFromY(Node parent) +{ + if (disabled()) + { + return nullptr; + } + return mkNot(mkResolution( + mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true)); +} + +std::shared_ptr ProofCircuitPropagator::impliesYFromX(Node parent) +{ + if (disabled()) + { + return nullptr; + } + return mkResolution( + mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false); +} + +std::shared_ptr ProofCircuitPropagator::eqXFromY(bool y, Node parent) +{ + if (disabled()) + { + return nullptr; + } + if (y) + { + return mkProof( + PfRule::EQ_RESOLVE, + {assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})}); + } + return mkNot(mkResolution( + mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true)); +} + +std::shared_ptr ProofCircuitPropagator::eqYFromX(bool x, Node parent) +{ + if (disabled()) + { + return nullptr; + } + if (x) + { + return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)}); + } + return mkNot(mkResolution( + mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true)); +} + +std::shared_ptr ProofCircuitPropagator::neqXFromY(bool y, + Node parent) +{ + if (disabled()) + { + return nullptr; + } + return mkResolution( + mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, + {assume(parent.notNode())}), + parent[1], + !y); +} + +std::shared_ptr ProofCircuitPropagator::neqYFromX(bool x, + Node parent) +{ + if (disabled()) + { + return nullptr; + } + return mkResolution( + mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, + {assume(parent.notNode())}), + parent[0], + !x); +} + +std::shared_ptr ProofCircuitPropagator::xorXFromY(bool negated, + bool y, + Node parent) +{ + if (disabled()) + { + return nullptr; + } + if (y) + { + return mkNot(mkResolution( + mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2, + {assume(negated ? parent.notNode() : Node(parent))}), + parent[1], + false)); + } + return mkResolution( + mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1, + {assume(negated ? parent.notNode() : Node(parent))}), + parent[1], + true); +} + +std::shared_ptr ProofCircuitPropagator::xorYFromX(bool negated, + bool x, + Node parent) +{ + if (disabled()) + { + return nullptr; + } + if (x) + { + return mkResolution( + mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2, + {assume(negated ? parent.notNode() : Node(parent))}), + parent[0], + false); + } + return mkNot( + mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1, + {assume(negated ? parent.notNode() : Node(parent))}), + parent[0], + true)); +} + +std::shared_ptr ProofCircuitPropagator::mkProof( + PfRule rule, + const std::vector>& children, + const std::vector& args) +{ + if (Trace.isOn("circuit-prop")) + { + std::stringstream ss; + ss << "Constructing (" << rule; + for (const auto& c : children) + { + ss << " " << *c; + } + if (!args.empty()) + { + ss << " :args"; + for (const auto& a : args) + { + ss << " " << a; + } + } + ss << ")"; + Trace("circuit-prop") << ss.str() << std::endl; + } + return d_pnm->mkNode(rule, children, args); +} + +std::shared_ptr ProofCircuitPropagator::mkCResolution( + const std::shared_ptr& clause, + const std::vector& lits, + const std::vector& polarity) +{ + auto* nm = NodeManager::currentNM(); + std::vector> children = {clause}; + std::vector args; + Assert(lits.size() == polarity.size()); + for (std::size_t i = 0, n = lits.size(); i < n; ++i) + { + bool pol = polarity[i]; + Node lit = lits[i]; + if (polarity[i]) + { + if (lit.getKind() == Kind::NOT) + { + lit = lit[0]; + pol = !pol; + children.emplace_back(assume(lit)); + } + else + { + children.emplace_back(assume(lit.notNode())); + } + } + else + { + children.emplace_back(assume(lit)); + } + args.emplace_back(nm->mkConst(pol)); + args.emplace_back(lit); + } + return mkProof(PfRule::CHAIN_RESOLUTION, children, args); +} + +std::shared_ptr ProofCircuitPropagator::mkCResolution( + const std::shared_ptr& clause, + const std::vector& lits, + bool polarity) +{ + return mkCResolution(clause, lits, std::vector(lits.size(), polarity)); +} + +std::shared_ptr ProofCircuitPropagator::mkResolution( + const std::shared_ptr& clause, const Node& lit, bool polarity) +{ + auto* nm = NodeManager::currentNM(); + if (polarity) + { + if (lit.getKind() == Kind::NOT) + { + return mkProof(PfRule::RESOLUTION, + {clause, assume(lit[0])}, + {nm->mkConst(false), lit[0]}); + } + return mkProof(PfRule::RESOLUTION, + {clause, assume(lit.notNode())}, + {nm->mkConst(true), lit}); + } + return mkProof( + PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit}); +} + +std::shared_ptr ProofCircuitPropagator::mkNot( + const std::shared_ptr& n) +{ + Node m = n->getResult(); + if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT) + { + return mkProof(PfRule::NOT_NOT_ELIM, {n}); + } + return n; +} + +ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward( + ProofNodeManager* pnm, TNode parent, bool parentAssignment) + : ProofCircuitPropagator(pnm), + d_parent(parent), + d_parentAssignment(parentAssignment) +{ +} + +std::shared_ptr ProofCircuitPropagatorBackward::andTrue( + TNode::iterator i) +{ + if (disabled()) + { + return nullptr; + } + return mkProof( + PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())}); +} + +std::shared_ptr ProofCircuitPropagatorBackward::orFalse( + TNode::iterator i) +{ + if (disabled()) + { + return nullptr; + } + return mkNot(mkProof(PfRule::NOT_OR_ELIM, + {assume(d_parent.notNode())}, + {mkRat(i - d_parent.begin())})); +} + +std::shared_ptr ProofCircuitPropagatorBackward::iteC(bool c) +{ + if (disabled()) + { + return nullptr; + } + if (d_parentAssignment) + { + return mkResolution( + mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}), + d_parent[0], + !c); + } + return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, + {assume(d_parent.notNode())}), + d_parent[0], + !c); +} + +std::shared_ptr ProofCircuitPropagatorBackward::iteIsCase(unsigned c) +{ + if (disabled()) + { + return nullptr; + } + if (d_parentAssignment) + { + return mkResolution( + mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false); + } + return mkResolution( + mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}), + d_parent[c + 1], + false); +} + +std::shared_ptr ProofCircuitPropagatorBackward::impliesNegX() +{ + if (disabled()) + { + return nullptr; + } + return mkNot( + mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())})); +} + +std::shared_ptr ProofCircuitPropagatorBackward::impliesNegY() +{ + if (disabled()) + { + return nullptr; + } + return mkNot( + mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())})); +} + +ProofCircuitPropagatorForward::ProofCircuitPropagatorForward( + ProofNodeManager* pnm, Node child, bool childAssignment, Node parent) + : ProofCircuitPropagator{pnm}, + d_child(child), + d_childAssignment(childAssignment), + d_parent(parent) +{ +} + +std::shared_ptr ProofCircuitPropagatorForward::andAllTrue() +{ + if (disabled()) + { + return nullptr; + } + std::vector> children; + for (const auto& child : d_parent) + { + children.emplace_back(assume(child)); + } + return mkProof(PfRule::AND_INTRO, children); +} + +std::shared_ptr ProofCircuitPropagatorForward::andOneFalse() +{ + if (disabled()) + { + return nullptr; + } + auto it = std::find(d_parent.begin(), d_parent.end(), d_child); + return mkResolution( + mkProof( + PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}), + d_child, + true); +} + +std::shared_ptr ProofCircuitPropagatorForward::orOneTrue() +{ + if (disabled()) + { + return nullptr; + } + auto it = std::find(d_parent.begin(), d_parent.end(), d_child); + return mkNot(mkResolution( + mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}), + d_child, + false)); +} + +std::shared_ptr ProofCircuitPropagatorForward::orFalse() +{ + if (disabled()) + { + return nullptr; + } + std::vector children(d_parent.begin(), d_parent.end()); + return mkCResolution( + mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true); +} + +std::shared_ptr ProofCircuitPropagatorForward::iteEvalThen(bool x) +{ + if (disabled()) + { + return nullptr; + } + return mkCResolution( + mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {false, !x}); +} + +std::shared_ptr ProofCircuitPropagatorForward::iteEvalElse(bool y) +{ + if (disabled()) + { + return nullptr; + } + return mkCResolution( + mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}), + {d_parent[0], d_parent[2]}, + {true, !y}); +} + +std::shared_ptr ProofCircuitPropagatorForward::eqEval(bool x, bool y) +{ + if (disabled()) + { + return nullptr; + } + if (x == y) + { + return mkCResolution( + mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1, + {}, + {d_parent}), + {d_parent[0], d_parent[1]}, + {!x, !y}); + } + return mkCResolution( + mkProof( + x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {!x, !y}); +} + +std::shared_ptr ProofCircuitPropagatorForward::impliesEval( + bool premise, bool conclusion) +{ + if (disabled()) + { + return nullptr; + } + if (!premise) + { + return mkResolution( + mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true); + } + if (conclusion) + { + return mkResolution( + mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false); + } + return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {false, true}); +} + +std::shared_ptr ProofCircuitPropagatorForward::xorEval(bool x, + bool y) +{ + if (disabled()) + { + return nullptr; + } + if (x && y) + { + return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {false, false}); + } + else if (x && !y) + { + return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {false, true}); + } + else if (!x && y) + { + return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {true, false}); + } + Assert(!x && !y); + return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}), + {d_parent[0], d_parent[1]}, + {true, true}); +} + +} // namespace booleans +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h new file mode 100644 index 000000000..cc0aaad36 --- /dev/null +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -0,0 +1,213 @@ +/********************* */ +/*! \file proof_circuit_propagator.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Proofs for the non-clausal circuit propagator. + ** + ** Proofs for the non-clausal circuit propagator. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H +#define CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H + +#include + +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +/** + * Base class for for CircuitPropagatorProofs. + * This class collects common functionality for proofs of backward and forward + * propagation. + */ +class ProofCircuitPropagator +{ + public: + ProofCircuitPropagator(ProofNodeManager* pnm); + + /** Assuming the given node */ + std::shared_ptr assume(Node n); + /** Apply CONTRA rule. Takes care of switching a and b if necessary */ + std::shared_ptr conflict(const std::shared_ptr& a, + const std::shared_ptr& b); + + /** (and true ... holdout true ...) --> holdout */ + std::shared_ptr andFalse(Node parent, TNode::iterator holdout); + + /** (or false ... holdout false ...) -> holdout */ + std::shared_ptr orTrue(Node parent, TNode::iterator holdout); + + /** (not x) is true --> x is false (and vice versa) */ + std::shared_ptr Not(bool negate, Node parent); + + /** (=> X false) --> (not X) */ + std::shared_ptr impliesXFromY(Node parent); + /** (=> true Y) --> Y */ + std::shared_ptr impliesYFromX(Node parent); + + /** Derive X from (= X Y) */ + std::shared_ptr eqXFromY(bool y, Node parent); + /** Derive Y from (= X Y) */ + std::shared_ptr eqYFromX(bool x, Node parent); + /** Derive X from (not (= X Y)) */ + std::shared_ptr neqXFromY(bool y, Node parent); + /** Derive Y from (not (= X Y)) */ + std::shared_ptr neqYFromX(bool x, Node parent); + + /** + * Uses (xor X Y) to derive the value of X. + * (xor X false) --> X + * (xor X true) --> (not X) + * (not (xor X false)) --> (not X) + * (not (xor X true)) --> X + */ + std::shared_ptr xorXFromY(bool negated, bool y, Node parent); + /** + * Uses (xor X Y) to derive the value of Y. + * (xor false Y) --> Y + * (xor true Y) --> (not Y) + * (not (xor false Y)) --> (not Y) + * (not (xor true Y)) --> Y + */ + std::shared_ptr xorYFromX(bool negated, bool x, Node parent); + + protected: + /** Shorthand to check whether proof generation is disabled */ + bool disabled() const; + + /** Construct proof using the given rule, children and args */ + std::shared_ptr mkProof( + PfRule rule, + const std::vector>& children, + const std::vector& args = {}); + /** + * Apply CHAIN_RESOLUTION rule. + * Constructs the args from the given literals and polarities (called ids in + * the proof rule). Automatically adds the clauses to resolve with as + * assumptions, depending on their polarity. + */ + std::shared_ptr mkCResolution( + const std::shared_ptr& clause, + const std::vector& lits, + const std::vector& polarity); + /** Shorthand for mkCResolution(clause, lits, {polarity, ...}) */ + std::shared_ptr mkCResolution( + const std::shared_ptr& clause, + const std::vector& lits, + bool polarity); + /** Apply RESOLUTION rule */ + std::shared_ptr mkResolution( + const std::shared_ptr& clause, const Node& lit, bool polarity); + /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */ + std::shared_ptr mkNot(const std::shared_ptr& n); + + /** The proof node manager */ + ProofNodeManager* d_pnm; +}; + +/** + * Proof generator for backward propagation + * A backward propagation is triggered by the assignment of the parent node. + */ +class ProofCircuitPropagatorBackward : public ProofCircuitPropagator +{ + public: + ProofCircuitPropagatorBackward(ProofNodeManager* pnm, + TNode parent, + bool parentAssignment); + + /** and true --> child is true */ + std::shared_ptr andTrue(TNode::iterator i); + + /** or false --> child is false */ + std::shared_ptr orFalse(TNode::iterator i); + + /** + * Propagate on ite with evaluate condition + * (ite true t e) --> t + * (not (ite true t e)) --> (not t) + * (ite false t e) --> e + * (not (ite false t e)) --> (not e) + */ + std::shared_ptr iteC(bool c); + /** + * For (ite c t e), we can derive the value for c + * c = 1: c = true + * c = 0: c = false + */ + std::shared_ptr iteIsCase(unsigned c); + + /** (not (=> X Y)) --> X */ + std::shared_ptr impliesNegX(); + /** (not (=> X Y)) --> (not Y) */ + std::shared_ptr impliesNegY(); + + private: + /** The parent node */ + TNode d_parent; + /** The assignment of d_parent */ + bool d_parentAssignment; +}; + +/** + * Proof generator for forward propagation + * A forward propagation is triggered by the assignment of a child node. + */ +class ProofCircuitPropagatorForward : public ProofCircuitPropagator +{ + public: + ProofCircuitPropagatorForward(ProofNodeManager* pnm, + Node child, + bool childAssignment, + Node parent); + + /** All children are true --> and is true */ + std::shared_ptr andAllTrue(); + /** One child is false --> and is false */ + std::shared_ptr andOneFalse(); + + /** One child is true --> or is true */ + std::shared_ptr orOneTrue(); + /** or false --> all children are false */ + std::shared_ptr orFalse(); + + /** Evaluate (ite true X _) from X */ + std::shared_ptr iteEvalThen(bool x); + /** Evaluate (ite false _ Y) from Y */ + std::shared_ptr iteEvalElse(bool y); + + /** Evaluate (= X Y) from X,Y */ + std::shared_ptr eqEval(bool x, bool y); + + /** Evaluate (=> X Y) from X,Y */ + std::shared_ptr impliesEval(bool premise, bool conclusion); + /** Evaluate (xor X Y) from X,Y */ + std::shared_ptr xorEval(bool x, bool y); + + private: + /** The current child that triggered the propagations */ + Node d_child; + /** The assignment of d_child */ + bool d_childAssignment; + /** The parent node used for propagation */ + Node d_parent; +}; + +} // namespace booleans +} // namespace theory +} // namespace CVC4 + +#endif -- 2.30.2