From: Andrew Reynolds Date: Fri, 28 Aug 2020 02:24:16 +0000 (-0500) Subject: Add the buffered inference manager (#4954) X-Git-Tag: cvc5-1.0.0~2947 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0a969d7d65a778f2230ee920339541fdf380234;p=cvc5.git Add the buffered inference manager (#4954) This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class. This PR adds basic calls to add lemmas on the output channel from InferenceManager. It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from. This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e86f3e491..06bc9917f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -510,6 +510,8 @@ libcvc4_add_sources( theory/fp/theory_fp_type_rules.h theory/fp/type_enumerator.h theory/interrupted.h + theory/inference_manager_buffered.cpp + theory/inference_manager_buffered.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp new file mode 100644 index 000000000..adbcc3033 --- /dev/null +++ b/src/theory/inference_manager_buffered.cpp @@ -0,0 +1,122 @@ +/********************* */ +/*! \file inference_manager_buffered.cpp + ** \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 A buffered inference manager + **/ + +#include "theory/inference_manager_buffered.h" + +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, + TheoryState& state, + ProofNodeManager* pnm) + : TheoryInferenceManager(t, state, pnm) +{ +} + +bool InferenceManagerBuffered::hasProcessed() const +{ + return d_theoryState.isInConflict() || !d_pendingLem.empty() + || !d_pendingFact.empty(); +} + +bool InferenceManagerBuffered::hasPendingFact() const +{ + return !d_pendingFact.empty(); +} + +bool InferenceManagerBuffered::hasPendingLemma() const +{ + return !d_pendingLem.empty(); +} + +void InferenceManagerBuffered::addPendingLemma(Node lem, + LemmaProperty p, + ProofGenerator* pg) +{ + d_pendingLem.push_back(std::make_shared(lem, p, pg)); +} + +void InferenceManagerBuffered::addPendingLemma(std::shared_ptr lemma) +{ + d_pendingLem.emplace_back(std::move(lemma)); +} + +void InferenceManagerBuffered::addPendingFact(Node fact, Node exp) +{ + Assert(fact.getKind() != AND && fact.getKind() != OR); + d_pendingFact.push_back(std::pair(fact, exp)); +} + +void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol) +{ + // must ensure rewritten + lit = Rewriter::rewrite(lit); + d_pendingReqPhase[lit] = pol; +} + +void InferenceManagerBuffered::doPendingFacts() +{ + size_t i = 0; + while (!d_theoryState.isInConflict() && i < d_pendingFact.size()) + { + std::pair& pfact = d_pendingFact[i]; + Node fact = pfact.first; + Node exp = pfact.second; + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + // no double negation or conjunctive conclusions + Assert(atom.getKind() != NOT && atom.getKind() != AND); + assertInternalFact(atom, polarity, exp); + i++; + } + d_pendingFact.clear(); +} + +void InferenceManagerBuffered::doPendingLemmas() +{ + // process all the pending lemmas + for (const std::shared_ptr& plem : d_pendingLem) + { + if (!plem->notifySend()) + { + // the lemma indicated that it should not be sent after all + continue; + } + Node lem = plem->d_node; + LemmaProperty p = plem->d_property; + ProofGenerator* pg = plem->d_pg; + Assert(!lem.isNull()); + // send (trusted) lemma on the output channel with property p + trustedLemma(TrustNode::mkTrustLemma(lem, pg), p); + } + d_pendingLem.clear(); +} + +void InferenceManagerBuffered::doPendingPhaseRequirements() +{ + // process the pending require phase calls + for (const std::pair& prp : d_pendingReqPhase) + { + d_out.requirePhase(prp.first, prp.second); + } + d_pendingReqPhase.clear(); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h new file mode 100644 index 000000000..bb46ef566 --- /dev/null +++ b/src/theory/inference_manager_buffered.h @@ -0,0 +1,161 @@ +/********************* */ +/*! \file inference_manager_buffered.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 A buffered inference manager + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H +#define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "theory/theory_inference_manager.h" + +namespace CVC4 { +namespace theory { + +/** + * A lemma base class. This class is an abstract data structure for storing + * pending lemmas in the inference manager below. + */ +class Lemma +{ + public: + Lemma(Node n, LemmaProperty p, ProofGenerator* pg) + : d_node(n), d_property(p), d_pg(pg) + { + } + virtual ~Lemma() {} + /** + * Called just before this lemma is sent on the output channel. The purpose + * of this callback is to do any specific process of the lemma, e.g. take + * debug statistics, cache, etc. + * + * @return true if the lemma should be sent on the output channel. + */ + virtual bool notifySend() { return true; } + /** The lemma to send */ + Node d_node; + /** The lemma property (see OutputChannel::lemma) */ + LemmaProperty d_property; + /** + * The proof generator for this lemma, which if non-null, is wrapped in a + * TrustNode to be set on the output channel via trustedLemma at the time + * the lemma is sent. This proof generator must be able to provide a proof + * for d_node in the remainder of the user context. + */ + ProofGenerator* d_pg; +}; + +/** + * The buffered inference manager. This class implements standard methods + * for buffering facts, lemmas and phase requirements. + */ +class InferenceManagerBuffered : public TheoryInferenceManager +{ + public: + InferenceManagerBuffered(Theory& t, + TheoryState& state, + ProofNodeManager* pnm); + ~InferenceManagerBuffered() {} + /** + * Have we processed an inference during this call to check? In particular, + * this returns true if we have a pending fact or lemma, or have encountered + * a conflict. + */ + bool hasProcessed() const; + /** + * Do we have a pending fact to add as an internal fact to the equality + * engine? + */ + bool hasPendingFact() const; + /** Do we have a pending lemma to send on the output channel? */ + bool hasPendingLemma() const; + /** + * Add pending lemma lem with property p, with proof generator pg. If + * non-null, pg must be able to provide a proof for lem for the remainder + * of the user context. Pending lemmas are sent to the output channel using + * doPendingLemmas. + */ + void addPendingLemma(Node lem, + LemmaProperty p = LemmaProperty::NONE, + ProofGenerator* pg = nullptr); + /** + * Add pending lemma, where lemma can be a (derived) class of the + * above one. Pending lemmas are sent to the output channel using + * doPendingLemmas. + */ + void addPendingLemma(std::shared_ptr lemma); + /** + * Add pending fact, which adds a fact on the pending fact queue. It must + * be the case that: + * (1) exp => fact is valid, + * (2) exp is a literal (or conjunction of literals) that holds in the + * equality engine of the theory. + * + * Pending facts are sent to the equality engine of this class using + * doPendingFacts. + */ + void addPendingFact(Node fact, Node exp); + /** Add pending phase requirement + * + * This method is called to indicate this class should send a phase + * requirement request to the output channel for literal lit to be + * decided with polarity pol. The literal lit should be a SAT literal + * by the time that doPendingPhaseRequirements is called. Typically, + * lit is a literal that is a subformula of a pending lemma that is processed + * prior to sending the phase requirement. + */ + void addPendingPhaseRequirement(Node lit, bool pol); + /** Do pending facts + * + * This method asserts pending facts (d_pendingFact) with explanations + * to the equality engine of the theory via calls + * to assertInternalFact. + * + * It terminates early if a conflict is encountered, for instance, by + * equality reasoning within the equality engine. + * + * Regardless of whether a conflict is encountered, the vector d_pendingFact + * is cleared after this call. + */ + void doPendingFacts(); + /** Do pending lemmas + * + * This method send all pending lemmas (d_pendingLem) on the output + * channel of the theory. + * + * Unlike doPendingFacts, this function will not terminate early if a conflict + * has already been encountered by the theory. The vector d_pendingLem is + * cleared after this call. + */ + void doPendingLemmas(); + /** + * Do pending phase requirements. Calls the output channel for all pending + * phase requirements and clears d_pendingReqPhase. + */ + void doPendingPhaseRequirements(); + + protected: + /** A set of pending lemmas */ + std::vector> d_pendingLem; + /** A set of pending facts, paired with their explanations */ + std::vector> d_pendingFact; + /** A map from literals to their pending phase requirement */ + std::map d_pendingReqPhase; +}; + +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 54f33f6e7..b2da91e16 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -111,6 +111,17 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a, << " mkTrustedConflictEqConstantMerge"; } +LemmaStatus TheoryInferenceManager::lemma(TNode lem, LemmaProperty p) +{ + return d_out.lemma(lem, p); +} + +LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem, + LemmaProperty p) +{ + return d_out.trustedLemma(tlem, p); +} + void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode fact) diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 914c87d19..e52afe124 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -105,6 +105,11 @@ class TheoryInferenceManager * been provided in a custom way. */ void trustedConflict(TrustNode tconf); + /** Send lemma lem with property p on the output channel. */ + LemmaStatus lemma(TNode lem, LemmaProperty p = LemmaProperty::NONE); + /** Send (trusted) lemma lem with property p on the output channel. */ + LemmaStatus trustedLemma(const TrustNode& tlem, + LemmaProperty p = LemmaProperty::NONE); /** * Assert internal fact. This is recommended method for asserting "internal" * facts into the equality engine of the theory. In particular, this method