From: Gereon Kremer Date: Mon, 22 Feb 2021 17:37:47 +0000 (+0100) Subject: Add the LazyTreeProofGenerator. (#5948) X-Git-Tag: cvc5-1.0.0~2250 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1700089e7ba96a883836eddcf2a8b88824aaa3e6;p=cvc5.git Add the LazyTreeProofGenerator. (#5948) This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion. The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished. We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3bfb248a4..5a44df141 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -612,6 +612,8 @@ libcvc4_add_sources( theory/inference_id.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h + theory/lazy_tree_proof_generator.cpp + theory/lazy_tree_proof_generator.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp new file mode 100644 index 000000000..126ce60b9 --- /dev/null +++ b/src/theory/lazy_tree_proof_generator.cpp @@ -0,0 +1,144 @@ +/********************* */ +/*! \file lazy_tree_proof_generator.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 Implementation of the lazy tree proof generator class + **/ + +#include "theory/lazy_tree_proof_generator.h" + +#include + +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace theory { + +LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, + const std::string& name) + : d_pnm(pnm), d_name(name) +{ + d_stack.emplace_back(&d_proof); +} +void LazyTreeProofGenerator::openChild() +{ + detail::TreeProofNode& pn = getCurrent(); + pn.d_children.emplace_back(); + d_stack.emplace_back(&pn.d_children.back()); +} +void LazyTreeProofGenerator::closeChild() +{ + Assert(getCurrent().d_rule != PfRule::UNKNOWN); + d_stack.pop_back(); +} +detail::TreeProofNode& LazyTreeProofGenerator::getCurrent() +{ + Assert(!d_stack.empty()) << "Proof construction has already been finished."; + return *d_stack.back(); +} +void LazyTreeProofGenerator::setCurrent(PfRule rule, + const std::vector& premise, + std::vector args, + Node proven) +{ + detail::TreeProofNode& pn = getCurrent(); + pn.d_rule = rule; + pn.d_premise = premise; + pn.d_args = args; + pn.d_proven = proven; +} +std::shared_ptr LazyTreeProofGenerator::getProof() const +{ + // Check cache + if (d_cached) return d_cached; + Assert(d_stack.empty()) << "Proof construction has not yet been finished."; + std::vector> scope; + d_cached = getProof(scope, d_proof); + return d_cached; +} + +std::shared_ptr LazyTreeProofGenerator::getProofFor(Node f) +{ + Assert(hasProofFor(f)); + return getProof(); +} + +bool LazyTreeProofGenerator::hasProofFor(Node f) +{ + return f == getProof()->getResult(); +} + +std::shared_ptr LazyTreeProofGenerator::getProof( + std::vector>& scope, + const detail::TreeProofNode& pn) const +{ + // Store scope size to reset scope afterwards + std::size_t before = scope.size(); + std::vector> children; + if (pn.d_rule == PfRule::SCOPE) + { + // Extend scope for all but the root node + if (&pn != &d_proof) + { + for (const auto& a : pn.d_args) + { + scope.emplace_back(d_pnm->mkAssume(a)); + } + } + } + else + { + // Initialize the children with the scope + children = scope; + } + for (auto& c : pn.d_children) + { + // Recurse into tree + children.emplace_back(getProof(scope, c)); + } + for (const auto& p : pn.d_premise) + { + // Add premises as assumptions + children.emplace_back(d_pnm->mkAssume(p)); + } + // Reset scope + scope.resize(before); + return d_pnm->mkNode(pn.d_rule, children, pn.d_args); +} + +void LazyTreeProofGenerator::print(std::ostream& os, + const std::string& prefix, + const detail::TreeProofNode& pn) const +{ + os << prefix << pn.d_rule << ": "; + container_to_stream(os, pn.d_premise); + os << " ==> " << pn.d_proven << std::endl; + if (!pn.d_args.empty()) + { + os << prefix << ":args "; + container_to_stream(os, pn.d_args); + std::cout << std::endl; + } + for (const auto& c : pn.d_children) + { + print(os, prefix + '\t', c); + } +} + +std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg) +{ + ltpg.print(os, "", ltpg.d_proof); + return os; +} + +} // namespace theory +} // namespace CVC4 \ No newline at end of file diff --git a/src/theory/lazy_tree_proof_generator.h b/src/theory/lazy_tree_proof_generator.h new file mode 100644 index 000000000..980d6d6bb --- /dev/null +++ b/src/theory/lazy_tree_proof_generator.h @@ -0,0 +1,222 @@ +/********************* */ +/*! \file lazy_tree_proof_generator.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 The lazy tree proof generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H +#define CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H + +#include + +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace theory { +namespace detail { +/** + * A single node in the proof tree created by the LazyTreeProofGenerator. + * A node directly represents a ProofNode that is eventually constructed from + * it. The Nodes of the additional field d_premise are added to d_children as + * new assumptions via ASSUME. + */ +struct TreeProofNode +{ + /** The proof rule */ + PfRule d_rule = PfRule::UNKNOWN; + /** Assumptions used as premise for this proof step */ + std::vector d_premise; + /** Arguments for this proof step */ + std::vector d_args; + /** Conclusion of this proof step */ + Node d_proven; + /** Children of this proof step */ + std::vector d_children; +}; +} // namespace detail + +/** + * This class supports the lazy creation of a tree-shaped proof. + * The core idea is that the lazy creation is necessary because proof rules + * depend on assumptions that are only known after the whole subtree has been + * finished. + * + * We indend to argue about proofs that roughly go as follows: + * - we assume a set of assumptions + * - we do a case split + * - for every case, we derive false, possibly by nested case splits + * + * Every case is represented by a SCOPE whose child derives false. When + * composing the final proof, we explicitly extend the premise of every proof + * step with the scope (the currently selected case) that this proof step lives + * in. When doing this, we ignore the outermost scope (which assumes the + * assertion set) to allow for having conflicts that are only a subset of the + * assertion set. + * + * Consider the example x*x<1 and x>2 and the intended proof + * (SCOPE + * (ARITH_NL_CAD_SPLIT + * (SCOPE + * (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false) + * :args [x<=2] + * ) + * (SCOPE + * (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false) + * :args [x>=1] + * ) + * ) + * :args [ x*x<1, x>2 ] + * ) + * We obtain this proof in a way that (in general) gives us the assumptions + * for the scopes (x<=2, x>=1) only when the scope children have been fully + * computed. Thus, we store the proof in an intermediate form and add the scope + * arguments when we learn them. Once we have completed the proof, we can easily + * transform it into proper ProofNodes. + * + * This class is stateful in the sense that the interface (in particular + * openChild() and closeChild()) navigates the proof tree (and creating it + * on-the-fly). Initially, and after reset() has been called, the proof consists + * of one empty proof node (with proof rule UNKNOWN). It stores the current + * position in the proof tree internally to make the interface easier to use. + * + * THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE! + * + * To construct the above proof, use this class roughly as follows: + * setCurrent(SCOPE, {}, assertions, false); + * openChild(); + * // First nested scope + * openChild(); + * setCurrent(SCOPE, {}, {}, false); + * openChild(); + * setCurrent(CAD_DIRECT, {x>2}, {}, false); + * closeChild(); + * getCurrent().args = {x<=2}; + * closeChild(); + * // Second nested scope + * openChild(); + * setCurrent(SCOPE, {}, {}, false); + * openChild(); + * setCurrent(CAD_DIRECT, {x*x<1}, {}, false); + * closeChild(); + * getCurrent().args = {x>=1}; + * closeChild(); + * // Finish split + * setCurrent(CAD_SPLIT, {}, {}, false); + * closeChild(); + * closeChild(); + * + * To explicitly finish proof construction, we need to call closeChild() one + * additional time. + */ +class LazyTreeProofGenerator : public ProofGenerator +{ + public: + friend std::ostream& operator<<(std::ostream& os, + const LazyTreeProofGenerator& ltpg); + + LazyTreeProofGenerator(ProofNodeManager* pnm, + const std::string& name = "LazyTreeProofGenerator"); + + std::string identify() const override { return d_name; } + /** Create a new child and make it the current node */ + void openChild(); + /** + * Finish the current node and return to its parent + * Checks that the current node has a proof rule different from UNKNOWN. + * When called on the root node, this finishes the proof construction: we can + * no longer call getCurrent(), setCurrent() openChild() and closeChild(), but + * instead can call getProof() now. + */ + void closeChild(); + /** + * Return a reference to the current node + */ + detail::TreeProofNode& getCurrent(); + /** Set the current node / proof step */ + void setCurrent(PfRule rule, + const std::vector& premise, + std::vector args, + Node proven); + /** Construct the proof as a ProofNode */ + std::shared_ptr getProof() const; + /** Return the constructed proof. Checks that we have proven f */ + std::shared_ptr getProofFor(Node f) override; + /** Checks whether we have proven f */ + bool hasProofFor(Node f) override; + + /** + * Removes children from the current node based on the given predicate. + * It can be used for cases where facts (and their proofs) are eagerly + * generated and then later pruned, for example to produce smaller conflicts. + * The predicate is given as a Callable f that is called for every child with + * the id of the child and the child itself. + * f should return true if the child should be kept, fals if the child should + * be removed. + * @param f a Callable bool(std::size_t, const detail::TreeProofNode&) + */ + template + void pruneChildren(F&& f) + { + auto& children = getCurrent().d_children; + std::size_t cur = 0; + std::size_t pos = 0; + for (std::size_t size = children.size(); cur < size; ++cur) + { + if (f(cur, children[pos])) + { + if (cur != pos) + { + children[pos] = std::move(children[cur]); + } + ++pos; + } + } + children.resize(pos); + } + + private: + /** recursive proof construction used by getProof() */ + std::shared_ptr getProof( + std::vector>& scope, + const detail::TreeProofNode& pn) const; + + /** recursive debug printing used by operator<<() */ + void print(std::ostream& os, + const std::string& prefix, + const detail::TreeProofNode& pn) const; + + /** The ProofNodeManager used for constructing ProofNodes */ + ProofNodeManager* d_pnm; + /** The trace to the current node */ + std::vector d_stack; + /** The root node of the proof tree */ + detail::TreeProofNode d_proof; + /** Caches the result of getProof() */ + mutable std::shared_ptr d_cached; + /** Name of this proof generator */ + std::string d_name; +}; + +/** + * Prints the current state of a LazyTreeProofGenerator. Can also be used on a + * partially constructed proof. It is intended for debugging only and attempts + * to pretty-print itself using indentation. + */ +std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); + +} // namespace theory +} // namespace CVC4 + +#endif