From: Haniel Barbosa Date: Wed, 16 Sep 2020 02:36:21 +0000 (-0300) Subject: [proof-new] A simple proof generator for buffered proof steps (#5069) X-Git-Tag: cvc5-1.0.0~2858 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a126d59141d2889e3b10b07ece4b10f48511a71;p=cvc5.git [proof-new] A simple proof generator for buffered proof steps (#5069) This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based. Co-authored-by: Andrew Reynolds --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index aed7a866c..3e3b569af 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -7,6 +7,8 @@ libcvc4_add_sources( attribute.cpp attribute_internals.h attribute_unique_id.h + buffered_proof_generator.cpp + buffered_proof_generator.h emptyset.cpp emptyset.h expr_iomanip.cpp diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp new file mode 100644 index 000000000..aa0fe19bd --- /dev/null +++ b/src/expr/buffered_proof_generator.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file buffered_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa + ** 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 a proof generator for buffered proof steps + **/ + +#include "expr/buffered_proof_generator.h" + +#include "expr/proof.h" + +namespace CVC4 { + +BufferedProofGenerator::BufferedProofGenerator(context::Context* c, + ProofNodeManager* pnm) + : ProofGenerator(), d_facts(c), d_pnm(pnm) +{ +} + +bool BufferedProofGenerator::addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy) +{ + // check duplicates if we are not always overwriting + if (opolicy != CDPOverwrite::ALWAYS) + { + if (d_facts.find(fact) != d_facts.end()) + { + // duplicate + return false; + } + Node symFact = CDProof::getSymmFact(fact); + if (!symFact.isNull()) + { + if (d_facts.find(symFact) != d_facts.end()) + { + // duplicate due to symmetry + return false; + } + } + } + // note that this replaces the value fact is mapped to if there is already one + d_facts.insert(fact, std::make_shared(ps)); + return true; +} + +std::shared_ptr BufferedProofGenerator::getProofFor(Node fact) +{ + Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact + << std::endl; + NodeProofStepMap::iterator it = d_facts.find(fact); + if (it == d_facts.end()) + { + Node symFact = CDProof::getSymmFact(fact); + if (symFact.isNull()) + { + Trace("pfee-fact-gen") << "...cannot find step" << std::endl; + Assert(false); + return nullptr; + } + it = d_facts.find(symFact); + if (it == d_facts.end()) + { + Assert(false); + Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; + return nullptr; + } + } + Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; + CDProof cdp(d_pnm); + cdp.addStep(fact, *(*it).second); + return cdp.getProofFor(fact); +} + +} // namespace CVC4 diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h new file mode 100644 index 000000000..987bd2465 --- /dev/null +++ b/src/expr/buffered_proof_generator.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file buffered_proof_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa + ** 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 A proof generator for buffered proof steps + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H +#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H + +#include +#include + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "expr/proof_step_buffer.h" + +namespace CVC4 { + +/** + * The proof generator for buffered steps. This class is a context-dependent + * mapping from formulas to proof steps. It does not generate ProofNodes until it + * is asked to provide a proof for a given fact. + */ +class BufferedProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap, NodeHashFunction> + NodeProofStepMap; + + public: + BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); + ~BufferedProofGenerator() {} + /** add step + * Unless the overwrite policy is ALWAYS it does not replace previously + * registered steps (modulo (dis)equality symmetry). + */ + bool addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy = CDPOverwrite::NEVER); + /** Get proof for. It is robust to (dis)equality symmetry. */ + std::shared_ptr getProofFor(Node f) override; + /** identify */ + std::string identify() const override { return "BufferedProofGenerator"; } + + private: + /** maps expected to ProofStep */ + NodeProofStepMap d_facts; + /** the proof node manager */ + ProofNodeManager* d_pnm; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index c8f5ebb4d..5811257ed 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -573,62 +573,6 @@ void ProofEqEngine::explainWithProof(Node lit, Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl; } - -ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c, - ProofNodeManager* pnm) - : ProofGenerator(), d_facts(c), d_pnm(pnm) -{ -} - -bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps) -{ - if (d_facts.find(fact) != d_facts.end()) - { - // duplicate - return false; - } - Node symFact = CDProof::getSymmFact(fact); - if (!symFact.isNull()) - { - if (d_facts.find(symFact) != d_facts.end()) - { - // duplicate due to symmetry - return false; - } - } - d_facts.insert(fact, std::make_shared(ps)); - return true; -} - -std::shared_ptr ProofEqEngine::FactProofGenerator::getProofFor( - Node fact) -{ - Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact - << std::endl; - NodeProofStepMap::iterator it = d_facts.find(fact); - if (it == d_facts.end()) - { - Node symFact = CDProof::getSymmFact(fact); - if (symFact.isNull()) - { - Trace("pfee-fact-gen") << "...cannot find step" << std::endl; - Assert(false); - return nullptr; - } - it = d_facts.find(symFact); - if (it == d_facts.end()) - { - Assert(false); - Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; - return nullptr; - } - } - Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; - CDProof cdp(d_pnm); - cdp.addStep(fact, *(*it).second); - return cdp.getProofFor(fact); -} - } // namespace eq } // namespace theory } // namespace CVC4 diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 49fde759e..67740d51f 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -22,11 +22,11 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "expr/buffered_proof_generator.h" #include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof_node.h" #include "expr/proof_node_manager.h" -#include "expr/proof_step_buffer.h" #include "theory/eager_proof_generator.h" #include "theory/uf/equality_engine.h" @@ -243,33 +243,6 @@ class ProofEqEngine : public EagerProofGenerator TrustNode explain(Node conc); private: - /** - * The default proof generator (for simple facts). This class is a context - * dependent mapping from formulas to proof steps. It does not generate - * ProofNode until it is asked to provide a proof for a given fact. - */ - class FactProofGenerator : public ProofGenerator - { - typedef context:: - CDHashMap, NodeHashFunction> - NodeProofStepMap; - - public: - FactProofGenerator(context::Context* c, ProofNodeManager* pnm); - ~FactProofGenerator() {} - /** add step */ - bool addStep(Node fact, ProofStep ps); - /** Get proof for */ - std::shared_ptr getProofFor(Node f) override; - /** identify */ - std::string identify() const override { return "FactProofGenerator"; } - - private: - /** maps expected to ProofStep */ - NodeProofStepMap d_facts; - /** the proof node manager */ - ProofNodeManager* d_pnm; - }; /** Assert internal */ bool assertFactInternal(TNode pred, bool polarity, TNode reason); /** holds */ @@ -302,7 +275,7 @@ class ProofEqEngine : public EagerProofGenerator /** Reference to the equality engine */ eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ - FactProofGenerator d_factPg; + BufferedProofGenerator d_factPg; /** common nodes */ Node d_true; Node d_false;