Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A buffered inference manager.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
      16                 :            : #define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
      17                 :            : 
      18                 :            : #include "expr/node.h"
      19                 :            : #include "theory/theory_inference.h"
      20                 :            : #include "theory/theory_inference_manager.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : 
      25                 :            : /**
      26                 :            :  * The buffered inference manager.  This class implements standard methods
      27                 :            :  * for buffering facts, lemmas and phase requirements.
      28                 :            :  */
      29                 :            : class InferenceManagerBuffered : public TheoryInferenceManager
      30                 :            : {
      31                 :            :  public:
      32                 :            :   InferenceManagerBuffered(Env& env,
      33                 :            :                            Theory& t,
      34                 :            :                            TheoryState& state,
      35                 :            :                            const std::string& statsName,
      36                 :            :                            bool cacheLemmas = true);
      37                 :     200557 :   virtual ~InferenceManagerBuffered() {}
      38                 :            :   /**
      39                 :            :    * Do we have a pending fact or lemma?
      40                 :            :    */
      41                 :            :   bool hasPending() const;
      42                 :            :   /**
      43                 :            :    * Do we have a pending fact to add as an internal fact to the equality
      44                 :            :    * engine?
      45                 :            :    */
      46                 :            :   bool hasPendingFact() const;
      47                 :            :   /** Do we have a pending lemma to send on the output channel? */
      48                 :            :   bool hasPendingLemma() const;
      49                 :            :   /**
      50                 :            :    * Add pending lemma lem with property p, with proof generator pg. If
      51                 :            :    * non-null, pg must be able to provide a proof for lem for the remainder
      52                 :            :    * of the user context. Pending lemmas are sent to the output channel using
      53                 :            :    * doPendingLemmas.
      54                 :            :    *
      55                 :            :    * @param lem The lemma to send
      56                 :            :    * @param id The identifier of the inference
      57                 :            :    * @param p The property of the lemma
      58                 :            :    * @param pg The proof generator which can provide a proof for lem
      59                 :            :    * @param checkCache Whether we want to check that the lemma is already in
      60                 :            :    * the cache.
      61                 :            :    * @return true if the lemma was added to the list of pending lemmas and
      62                 :            :    * false if the lemma is already cached.
      63                 :            :    */
      64                 :            :   bool addPendingLemma(Node lem,
      65                 :            :                        InferenceId id,
      66                 :            :                        LemmaProperty p = LemmaProperty::NONE,
      67                 :            :                        ProofGenerator* pg = nullptr,
      68                 :            :                        bool checkCache = true);
      69                 :            :   /**
      70                 :            :    * Add pending lemma, where lemma can be a (derived) class of the
      71                 :            :    * theory inference base class.
      72                 :            :    */
      73                 :            :   void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
      74                 :            :   /**
      75                 :            :    * Add pending fact, which adds a fact on the pending fact queue. It must
      76                 :            :    * be the case that:
      77                 :            :    * (1) exp => conc is valid,
      78                 :            :    * (2) exp is a literal (or conjunction of literals) that holds in the
      79                 :            :    * equality engine of the theory.
      80                 :            :    *
      81                 :            :    * Pending facts are sent to the equality engine of this class using
      82                 :            :    * doPendingFacts.
      83                 :            :    * @param conc The conclustion
      84                 :            :    * @param id The identifier of the inference
      85                 :            :    * @param exp The explanation in the equality engine of the theory
      86                 :            :    * @param pg The proof generator which can provide a proof for conc
      87                 :            :    */
      88                 :            :   void addPendingFact(Node conc,
      89                 :            :                       InferenceId id,
      90                 :            :                       Node exp,
      91                 :            :                       ProofGenerator* pg = nullptr);
      92                 :            :   /**
      93                 :            :    * Add pending fact, where fact can be a (derived) class of the
      94                 :            :    * theory inference base class.
      95                 :            :    */
      96                 :            :   void addPendingFact(std::unique_ptr<TheoryInference> fact);
      97                 :            :   /** Add pending phase requirement
      98                 :            :    *
      99                 :            :    * This method is called to indicate this class should send a phase
     100                 :            :    * requirement request to the output channel for literal lit to be
     101                 :            :    * decided with polarity pol. The literal lit should be a SAT literal
     102                 :            :    * by the time that doPendingPhaseRequirements is called. Typically,
     103                 :            :    * lit is a literal that is a subformula of a pending lemma that is processed
     104                 :            :    * prior to sending the phase requirement.
     105                 :            :    */
     106                 :            :   void addPendingPhaseRequirement(Node lit, bool pol);
     107                 :            :   /** Do pending facts
     108                 :            :    *
     109                 :            :    * This method asserts pending facts (d_pendingFact) with explanations
     110                 :            :    * to the equality engine of the theory via calls
     111                 :            :    * to assertInternalFact.
     112                 :            :    *
     113                 :            :    * It terminates early if a conflict is encountered, for instance, by
     114                 :            :    * equality reasoning within the equality engine.
     115                 :            :    *
     116                 :            :    * Regardless of whether a conflict is encountered, the vector d_pendingFact
     117                 :            :    * is cleared after this call.
     118                 :            :    */
     119                 :            :   void doPendingFacts();
     120                 :            :   /** Do pending lemmas
     121                 :            :    *
     122                 :            :    * This method send all pending lemmas (d_pendingLem) on the output
     123                 :            :    * channel of the theory.
     124                 :            :    *
     125                 :            :    * Unlike doPendingFacts, this function will not terminate early if a conflict
     126                 :            :    * has already been encountered by the theory. The vector d_pendingLem is
     127                 :            :    * cleared after this call.
     128                 :            :    */
     129                 :            :   void doPendingLemmas();
     130                 :            :   /**
     131                 :            :    * Do pending method. This processes all pending facts, lemmas and pending
     132                 :            :    * phase requests based on the policy of this manager. This means that
     133                 :            :    * we process the pending facts first and abort if in conflict. Otherwise, we
     134                 :            :    * process the pending lemmas and then the pending phase requirements.
     135                 :            :    * Notice that we process the pending lemmas even if there were facts.
     136                 :            :    */
     137                 :            :   void doPending();
     138                 :            :   /**
     139                 :            :    * Have we processed an inference during this call to check? In particular,
     140                 :            :    * this returns true if we have a pending fact or lemma, or have encountered
     141                 :            :    * a conflict.
     142                 :            :    */
     143                 :            :   bool hasProcessed() const;
     144                 :            :   /**
     145                 :            :    * Do pending phase requirements. Calls the output channel for all pending
     146                 :            :    * phase requirements and clears d_pendingReqPhase.
     147                 :            :    */
     148                 :            :   void doPendingPhaseRequirements();
     149                 :            :   /** Clear pending facts, lemmas, and phase requirements without processing */
     150                 :            :   void clearPending();
     151                 :            :   /** Clear pending facts, without processing */
     152                 :            :   void clearPendingFacts();
     153                 :            :   /** Clear pending lemmas, without processing */
     154                 :            :   void clearPendingLemmas();
     155                 :            :   /** Clear pending phase requirements, without processing */
     156                 :            :   void clearPendingPhaseRequirements();
     157                 :            : 
     158                 :            :   /** Returns the number of pending lemmas. */
     159                 :            :   std::size_t numPendingLemmas() const;
     160                 :            :   /** Returns the number of pending facts. */
     161                 :            :   std::size_t numPendingFacts() const;
     162                 :            : 
     163                 :            :   /**
     164                 :            :    * Send the given theory inference as a lemma on the output channel of this
     165                 :            :    * inference manager. This calls TheoryInferenceManager::trustedLemma based
     166                 :            :    * on the provided theory inference, and returns true if the lemma was
     167                 :            :    * successfully sent.
     168                 :            :    */
     169                 :            :   bool lemmaTheoryInference(TheoryInference* lem);
     170                 :            :   /**
     171                 :            :    * Add the given theory inference as an internal fact. This calls
     172                 :            :    * TheoryInferenceManager::assertInternalFact based on the provided theory
     173                 :            :    * inference.
     174                 :            :    */
     175                 :            :   void assertInternalFactTheoryInference(TheoryInference* fact);
     176                 :            : 
     177                 :            :   /**
     178                 :            :    * Notify this inference manager that a conflict was sent in this SAT context.
     179                 :            :    * This method is called via TheoryEngine when a conflict is sent. This
     180                 :            :    * method will clear all pending facts, lemmas, and phase requirements, as
     181                 :            :    * these will be stale after the solver backtracks.
     182                 :            :    */
     183                 :            :   void notifyInConflict() override;
     184                 :            : 
     185                 :            :   /**
     186                 :            :    * Returns the associated node manager
     187                 :            :    */
     188                 :      77910 :   NodeManager* getNodeManager() const { return nodeManager(); }
     189                 :            : 
     190                 :            :  protected:
     191                 :            :   /** A set of pending inferences to be processed as lemmas */
     192                 :            :   std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
     193                 :            :   /** A set of pending inferences to be processed as facts */
     194                 :            :   std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
     195                 :            :   /** A map from literals to their pending phase requirement */
     196                 :            :   std::map<Node, bool> d_pendingReqPhase;
     197                 :            :   /**
     198                 :            :    * Whether we are currently processing pending lemmas. This flag ensures
     199                 :            :    * that we do not call pending lemmas recursively, which may lead to
     200                 :            :    * segfaults.
     201                 :            :    */
     202                 :            :   bool d_processingPendingLemmas;
     203                 :            : };
     204                 :            : 
     205                 :            : }  // namespace theory
     206                 :            : }  // namespace cvc5::internal
     207                 :            : 
     208                 :            : #endif