From: Andrew Reynolds Date: Thu, 9 Jul 2020 05:41:47 +0000 (-0500) Subject: (proof-new) Theory engine proof generator (#4657) X-Git-Tag: cvc5-1.0.0~3140 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c64575b7c65a9822955efbf7711736068394899a;p=cvc5.git (proof-new) Theory engine proof generator (#4657) This adds the proof generator used by TheoryEngine for generating proofs for explanations. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9c95163bc..1b7236d3a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -751,6 +751,8 @@ libcvc4_add_sources( theory/theory.h theory/theory_engine.cpp theory/theory_engine.h + theory/theory_engine_proof_generator.cpp + theory/theory_engine_proof_generator.h theory/theory_id.cpp theory/theory_id.h theory/theory_model.cpp diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp new file mode 100644 index 000000000..2ac1236f8 --- /dev/null +++ b/src/theory/theory_engine_proof_generator.cpp @@ -0,0 +1,80 @@ +/********************* */ +/*! \file theory_engine_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 theory engine proof generator + **/ + +#include "theory/theory_engine_proof_generator.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, + context::UserContext* u) + : d_pnm(pnm), d_proofs(u) +{ +} + +theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( + TNode lit, Node exp, std::shared_ptr lpf) +{ + theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); + Node p = trn.getProven(); + Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); + // should not already be proven + NodeLazyCDProofMap::iterator it = d_proofs.find(p); + if (it == d_proofs.end()) + { + // we will prove the fact p using the proof from lpf. + d_proofs.insert(p, lpf); + } + return trn; +} + +std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) +{ + // should only ask this generator for proofs of implications + Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2); + NodeLazyCDProofMap::iterator it = d_proofs.find(f); + if (it == d_proofs.end()) + { + return nullptr; + } + std::shared_ptr lcp = (*it).second; + // finalize it via scope + std::vector scopeAssumps; + if (f[0].getKind() == AND) + { + for (const Node& fc : f[0]) + { + scopeAssumps.push_back(fc); + } + } + else + { + scopeAssumps.push_back(f[0]); + } + Node conclusion = f[1]; + + // get the proof for conclusion + std::shared_ptr pfb = lcp->getProofFor(conclusion); + // call the scope method of proof node manager + std::shared_ptr pf = d_pnm->mkScope(pfb, scopeAssumps); + return pf; +} + +std::string TheoryEngineProofGenerator::identify() const +{ + return "TheoryEngineProofGenerator"; +} + +} // namespace CVC4 diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h new file mode 100644 index 000000000..a551e79b2 --- /dev/null +++ b/src/theory/theory_engine_proof_generator.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file theory_engine.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 theory engine proof generator + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H +#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H + +#include + +#include "context/cdhashmap.h" +#include "context/context.h" +#include "expr/lazy_proof.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "theory/trust_node.h" + +namespace CVC4 { + +/** + * A simple proof generator class used by the theory engine. This class + * stores proofs for TheoryEngine::getExplanation. + * + * Notice that this class could be made general purpose. Its main feature is + * storing lazy proofs for facts in a context-dependent manner. + */ +class TheoryEngineProofGenerator : public ProofGenerator +{ + typedef context:: + CDHashMap, NodeHashFunction> + NodeLazyCDProofMap; + + public: + TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); + ~TheoryEngineProofGenerator() {} + /** + * Make trust explanation. Called when lpf has a proof of lit from free + * assumptions in exp. + * + * This stores lpf in the map d_proofs below and returns the trust node for + * this propagation, which has TrustNodeKind TrustNodeKind::PROP_EXP. If this + * explanation already exists, then the previous explanation is taken, which + * also suffices for proving the implication. + */ + theory::TrustNode mkTrustExplain(TNode lit, + Node exp, + std::shared_ptr lpf); + /** + * Get proof for, which expects implications corresponding to explained + * propagations (=> exp lit) registered by the above method. This currently + * involves calling the mkScope method of ProofNodeManager internally, which + * returns a closed proof. + */ + std::shared_ptr getProofFor(Node f) override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override; + + private: + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_pnm; + /** Map from formulas to lazy CD proofs */ + NodeLazyCDProofMap d_proofs; +}; + +} // namespace CVC4 + +#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */