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                 :            :  * The theory inference utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__THEORY_INFERENCE_H
      16                 :            : #define CVC5__THEORY__THEORY_INFERENCE_H
      17                 :            : 
      18                 :            : #include "expr/node.h"
      19                 :            : #include "theory/inference_id.h"
      20                 :            : #include "theory/output_channel.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : 
      25                 :            : class TheoryInferenceManager;
      26                 :            : 
      27                 :            : /**
      28                 :            :  * A theory inference base class. This class is an abstract data structure for
      29                 :            :  * storing pending lemmas or facts in the buffered inference manager. It can
      30                 :            :  * be seen a single use object capturing instructions for making a single
      31                 :            :  * call to TheoryInferenceManager for lemmas or facts.
      32                 :            :  */
      33                 :            : class TheoryInference
      34                 :            : {
      35                 :            :  public:
      36                 :    1086294 :   TheoryInference(InferenceId id) : d_id(id) {}
      37                 :    1347854 :   virtual ~TheoryInference() {}
      38                 :            : 
      39                 :            :   /**
      40                 :            :    * Process lemma, return the trust node to pass to
      41                 :            :    * TheoryInferenceManager::trustedLemma. In addition, the inference should
      42                 :            :    * process any internal side effects of the lemma.
      43                 :            :    *
      44                 :            :    * @param p The property of the lemma which will be passed to trustedLemma
      45                 :            :    * for this inference. If this call does not update p, the default value will
      46                 :            :    * be used.
      47                 :            :    * @return The trust node (of kind TrustNodeKind::LEMMA) corresponding to the
      48                 :            :    * lemma and its proof generator.
      49                 :            :    */
      50                 :          0 :   virtual TrustNode processLemma(CVC5_UNUSED LemmaProperty& p)
      51                 :            :   {
      52                 :          0 :     return TrustNode::null();
      53                 :            :   }
      54                 :            :   /**
      55                 :            :    * Process internal fact, return the conclusion to pass to
      56                 :            :    * TheoryInferenceManager::assertInternalFact. In addition, the inference
      57                 :            :    * should process any internal side effects of the fact.
      58                 :            :    *
      59                 :            :    * @param exp The explanation for the returned conclusion. Each node added to
      60                 :            :    * exp should be a (conjunction of) literals that hold in the current equality
      61                 :            :    * engine.
      62                 :            :    * @return The (possibly negated) conclusion.
      63                 :            :    */
      64                 :          0 :   virtual Node processFact(CVC5_UNUSED std::vector<Node>& exp,
      65                 :            :                            CVC5_UNUSED ProofGenerator*& pg)
      66                 :            :   {
      67                 :          0 :     return Node::null();
      68                 :            :   }
      69                 :            : 
      70                 :            :   /** Get the InferenceId of this theory inference. */
      71                 :    1501698 :   InferenceId getId() const { return d_id; }
      72                 :            :   /** Set the InferenceId of this theory inference. */
      73                 :      26440 :   void setId(InferenceId id) { d_id = id; }
      74                 :            : 
      75                 :            :  private:
      76                 :            :   InferenceId d_id;
      77                 :            : };
      78                 :            : 
      79                 :            : /**
      80                 :            :  * A simple theory lemma with no side effects. Makes a single call to
      81                 :            :  * trustedLemma in its process method.
      82                 :            :  */
      83                 :            : class SimpleTheoryLemma : public TheoryInference
      84                 :            : {
      85                 :            :  public:
      86                 :            :   SimpleTheoryLemma(InferenceId id,
      87                 :            :                     Node n,
      88                 :            :                     LemmaProperty p,
      89                 :            :                     ProofGenerator* pg);
      90                 :     577958 :   virtual ~SimpleTheoryLemma() {}
      91                 :            :   /** Process lemma */
      92                 :            :   TrustNode processLemma(LemmaProperty& p) override;
      93                 :            :   /** The lemma to send */
      94                 :            :   Node d_node;
      95                 :            :   /** The lemma property (see OutputChannel::lemma) */
      96                 :            :   LemmaProperty d_property;
      97                 :            :   /**
      98                 :            :    * The proof generator for this lemma, which if non-null, is wrapped in a
      99                 :            :    * TrustNode to be set on the output channel via trustedLemma at the time
     100                 :            :    * the lemma is sent. This proof generator must be able to provide a proof
     101                 :            :    * for d_node in the remainder of the user context.
     102                 :            :    */
     103                 :            :   ProofGenerator* d_pg;
     104                 :            : };
     105                 :            : 
     106                 :            : /**
     107                 :            :  * A simple internal fact with no side effects. Makes a single call to
     108                 :            :  * assertInternalFact in its process method.
     109                 :            :  */
     110                 :            : class SimpleTheoryInternalFact : public TheoryInference
     111                 :            : {
     112                 :            :  public:
     113                 :            :   SimpleTheoryInternalFact(InferenceId id,
     114                 :            :                            Node conc,
     115                 :            :                            Node exp,
     116                 :            :                            ProofGenerator* pg);
     117                 :     525779 :   virtual ~SimpleTheoryInternalFact() {}
     118                 :            :   /** Process internal fact */
     119                 :            :   Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
     120                 :            :   /** The lemma to send */
     121                 :            :   Node d_conc;
     122                 :            :   /** The explanation */
     123                 :            :   Node d_exp;
     124                 :            :   /** The proof generator */
     125                 :            :   ProofGenerator* d_pg;
     126                 :            : };
     127                 :            : 
     128                 :            : }  // namespace theory
     129                 :            : }  // namespace cvc5::internal
     130                 :            : 
     131                 :            : #endif