diff options
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/proof_engine_output_channel.cpp | 40 | ||||
-rw-r--r-- | src/theory/shared_terms_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 72 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 18 | ||||
-rw-r--r-- | src/theory/theory_engine_proof_generator.cpp | 81 | ||||
-rw-r--r-- | src/theory/theory_engine_proof_generator.h | 53 |
7 files changed, 209 insertions, 59 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2ac73f067..6deaea082 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -748,6 +748,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/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp index 20dbd4ef0..82363ff9b 100644 --- a/src/theory/proof_engine_output_channel.cpp +++ b/src/theory/proof_engine_output_channel.cpp @@ -30,25 +30,8 @@ ProofEngineOutputChannel::ProofEngineOutputChannel(TheoryEngine* engine, void ProofEngineOutputChannel::trustedConflict(TrustNode pconf) { Assert(pconf.getKind() == TrustNodeKind::CONFLICT); - Node conf = pconf.getNode(); - if (d_lazyPf != nullptr) - { - Node ckey = pconf.getProven(); - ProofGenerator* pfg = pconf.getGenerator(); - // may or may not have supplied a generator - if (pfg != nullptr) - { - ++d_statistics.trustedConflicts; - // if we have, add it to the lazy proof object - d_lazyPf->addLazyStep(ckey, pfg); - Assert(pfg->hasProofFor(ckey)); - } - else - { - // if none provided, do a very coarse-grained step - addTheoryLemmaStep(ckey); - } - } + d_engine->processTrustNode(pconf, d_theory); + TNode conf = pconf.getNode(); // now, call the normal interface to conflict conflict(conf); } @@ -59,25 +42,8 @@ LemmaStatus ProofEngineOutputChannel::trustedLemma(TrustNode plem, bool sendAtoms) { Assert(plem.getKind() == TrustNodeKind::LEMMA); + d_engine->processTrustNode(plem, d_theory); TNode lem = plem.getNode(); - if (d_lazyPf != nullptr) - { - Node lkey = plem.getProven(); - ProofGenerator* pfg = plem.getGenerator(); - // may or may not have supplied a generator - if (pfg != nullptr) - { - ++d_statistics.trustedLemmas; - // if we have, add it to the lazy proof object - d_lazyPf->addLazyStep(lkey, pfg); - Assert(pfg->hasProofFor(lkey)); - } - else - { - // if none provided, do a very coarse-grained step - addTheoryLemmaStep(lkey); - } - } // now, call the normal interface for lemma return OutputChannel::lemma(lem, removable, preprocess, sendAtoms); } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 723e20a16..ac27a5820 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -230,7 +230,7 @@ void SharedTermsDatabase::checkForConflict() { conflict = conflict.notNode(); } TrustNode trnc = d_pfee.assertConflict(conflict); - d_theoryEngine->processTrustNode(trnc); + d_theoryEngine->processTrustNode(trnc, THEORY_BUILTIN); d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 93a3f286d..7a1e34bef 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,6 +52,7 @@ #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" #include "util/resource_manager.h" +#include "theory/theory_engine_proof_generator.h" using namespace std; @@ -201,6 +202,7 @@ TheoryEngine::TheoryEngine(context::Context* context, options::proofNew() ? new LazyCDProof(d_pNodeManager.get(), nullptr, d_userContext) : nullptr), + d_tepg(new TheoryEngineProofGenerator(d_pNodeManager.get(), d_userContext)), d_sharedTerms( this, context, userContext, d_pNodeManager.get(), d_lazyProof.get()), d_masterEqualityEngine(nullptr), @@ -1605,8 +1607,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( proofRecipe->addStep(proofStep); } }); - // it came directly from the theory, it is ready to be processed - processTrustNode(texplanation); return texplanation; } @@ -1639,7 +1639,6 @@ theory::TrustNode TheoryEngine::getExplanationAndRecipe( Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; - // the trust node was processed within getExplanation return texplanation; } @@ -1848,7 +1847,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } -void TheoryEngine::processTrustNode(theory::TrustNode trn) +void TheoryEngine::processTrustNode(theory::TrustNode trn, + theory::TheoryId from) { if (d_lazyProof == nullptr) { @@ -1856,15 +1856,29 @@ void TheoryEngine::processTrustNode(theory::TrustNode trn) return; } ProofGenerator* pfg = trn.getGenerator(); + Node p = trn.getProven(); // may or may not have supplied a generator if (pfg != nullptr) { - Node p = trn.getProven(); // if we have, add it to the lazy proof object d_lazyProof->addLazyStep(p, pfg); // generator should have a proof for p Assert(pfg->hasProofFor(p)); } + else + { + // all BUILTIN should be handled + Assert (from!=THEORY_BUILTIN); + // untrusted theory lemma + std::vector<Node> children; + std::vector<Node> args; + args.push_back(p); + unsigned tid = static_cast<unsigned>(from); + Node tidn = NodeManager::currentNM()->mkConst(Rational(tid)); + args.push_back(tidn); + // add the step, should always succeed; + d_lazyProof->addStep(p, PfRule::THEORY_LEMMA, children, args); + } } void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { @@ -1913,8 +1927,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { TrustNode tnc = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); - // FIXME: have ~( l1 ^ ... ^ ln ) and ( E1 ^ ... ^ En ) => l1 ^ ... ^ ln - // Prove ~( E1 ^ ... ^ En ) + // FIXME: have ~( F ) and E => F, prove ~( E ) Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; @@ -2009,7 +2022,9 @@ theory::TrustNode TheoryEngine::getExplanation( Assert(explanationVector.size() == 1); Node conclusion = explanationVector[0].d_node; - std::unique_ptr<LazyCDProof> lcp; + std::shared_ptr<LazyCDProof> lcp; + bool simpleExplain = true; + TrustNode simpleTrn; if (d_lazyProof != nullptr) { Trace("te-proof-exp") << "TheoryEngine::getExplanation " << conclusion << std::endl; @@ -2053,6 +2068,7 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(toExplain.d_node); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + simpleExplain = false; } continue; } @@ -2096,6 +2112,7 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + simpleExplain = false; } ++ i; continue; @@ -2138,6 +2155,7 @@ theory::TrustNode TheoryEngine::getExplanation( Trace("te-proof-exp") << "- t-explained cached: " << toExplain.d_node << " by " << (*find).second.d_node << std::endl; // does this ever happen? Assert(false); + simpleExplain = false; } } continue; @@ -2196,6 +2214,20 @@ theory::TrustNode TheoryEngine::getExplanation( args.push_back(mkMethodId(MethodId::SB_PREDICATE)); lcp->addStep( toExplain.d_node, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + if (simpleExplain) + { + if (simpleTrn.isNull()) + { + // as an optimization, it may be a simple explanation, so we + // remember the trust node for now + simpleTrn = texplanation; + } + else + { + // multiple theories involved, not simple + simpleExplain = false; + } + } } } Node explanation = texplanation.getNode(); @@ -2269,18 +2301,20 @@ theory::TrustNode TheoryEngine::getExplanation( if (lcp != nullptr) { - Assert(lcp != nullptr); - // FIXME - // get the proof for conclusion - std::shared_ptr<ProofNode> pfConc = lcp->mkProof(conclusion); - std::vector<Node> scopeAssumps; - for (size_t k = 0, esize = explanationVector.size(); k < esize; ++k) + // doesn't work currently due to reordering of assumptions + /* + if (simpleExplain) { - scopeAssumps.push_back(explanationVector[k].d_node); - } - // call the scope method of proof node manager - std::shared_ptr<ProofNode> pf = - d_pNodeManager->mkScope(pfConc, scopeAssumps); + // single call to a theory's explain method, skip the proof generator + Assert (!simpleTrn.isNull()); + Trace("te-proof-exp") << "...simple explain " << simpleTrn.getNode() << std::endl; + return simpleTrn; + } + */ + // store in the proof generator + TrustNode trn = d_tepg->mkTrustExplain(conclusion,exp,lcp); + // return the trust node + return trn; } return theory::TrustNode::mkTrustLemma(exp, nullptr); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c3759ca52..de4b17f8c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -58,6 +58,7 @@ namespace CVC4 { class ResourceManager; class LemmaProofRecipe; class LazyCDProof; +class TheoryEngineProofGenerator; /** * A pair of a theory and a node. This is used to mark the flow of @@ -156,6 +157,8 @@ class TheoryEngine { * This stores instructions for how to construct proofs for all theory lemmas. */ std::shared_ptr<LazyCDProof> d_lazyProof; + /** The proof generator */ + std::shared_ptr<TheoryEngineProofGenerator> d_tepg; //--------------------------------- end new proofs /** @@ -361,8 +364,19 @@ class TheoryEngine { bool preprocess, theory::TheoryId atomsTo); - /** Process trust node */ - void processTrustNode(theory::TrustNode trn); + /** + * Process trust node. This method ensures that the proof for the proven node + * of trn is stored as a lazy step in the lazy proof (d_lazyProof) maintained + * by this class, referencing the proof generator of the trust node. The + * argument from specifies the theory responsible for this trust node. If + * no generator is provided, then a (eager) THEORY_LEMMA step is added to + * the lazy proof. + * + * @param trn The trust node to process + * @param from The id of the theory responsible for the trust node. + */ + void processTrustNode(theory::TrustNode trn, + theory::TheoryId from); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp new file mode 100644 index 000000000..af737e53b --- /dev/null +++ b/src/theory/theory_engine_proof_generator.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \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<LazyCDProof> lpf) +{ + theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit,exp,this); + Node p = trn.getProven(); + // should not already be proven + NodeLazyCDProofMap::iterator it = d_proofs.find(p); + if (it!=d_proofs.end()) + { + Assert(false); + } + else + { + // we will prove this + d_proofs.insert(p, lpf); + } + return trn; +} + +std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f) +{ + Assert (f.getKind()==IMPLIES && f.getNumChildren()==2); + NodeLazyCDProofMap::iterator it = d_proofs.find(f); + if (it==d_proofs.end()) + { + return nullptr; + } + std::shared_ptr<LazyCDProof> lcp = (*it).second; + // finalize it via scope + std::vector<Node> scopeAssumps; + if (f[0].getKind()==AND) + { + for (const Node& fc : f[0]) + { + scopeAssumps.push_back(fc); + } + } + else + { + scopeAssumps.push_back(f[1]); + } + Node conclusion = f[1]; + + // get the proof for conclusion + std::shared_ptr<ProofNode> pfb = lcp->mkProof(conclusion); + // call the scope method of proof node manager + std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps); + return pf; +} + +std::string TheoryEngineProofGenerator::identify() const +{ + return "TheoryEngineProofGenerator"; +} + +} diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h new file mode 100644 index 000000000..0dd6e0dd8 --- /dev/null +++ b/src/theory/theory_engine_proof_generator.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file theory_engine.h + ** \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 "cvc4_private.h" + +#ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H +#define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H + +#include <memory> + +#include "expr/lazy_proof.h" +#include "expr/proof_node_manager.h" +#include "expr/proof_generator.h" +#include "context/cdhashmap.h" +#include "context/context.h" +#include "theory/trust_node.h" + +namespace CVC4 { + +class TheoryEngineProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction> + NodeLazyCDProofMap; + public: + TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); + ~TheoryEngineProofGenerator(){} + /** Set proof */ + theory::TrustNode mkTrustExplain(TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf); + /** Get proof for */ + std::shared_ptr<ProofNode> 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; +}; + +} + +#endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */ |