Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * The theory inference utility.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__THEORY_INFERENCE_H
      19                 :            : #define CVC5__THEORY__THEORY_INFERENCE_H
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : #include "theory/inference_id.h"
      23                 :            : #include "theory/output_channel.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace theory {
      27                 :            : 
      28                 :            : class TheoryInferenceManager;
      29                 :            : 
      30                 :            : /**
      31                 :            :  * A theory inference base class. This class is an abstract data structure for
      32                 :            :  * storing pending lemmas or facts in the buffered inference manager. It can
      33                 :            :  * be seen a single use object capturing instructions for making a single
      34                 :            :  * call to TheoryInferenceManager for lemmas or facts.
      35                 :            :  */
      36                 :            : class TheoryInference
      37                 :            : {
      38                 :            :  public:
      39                 :     768510 :   TheoryInference(InferenceId id) : d_id(id) {}
      40                 :     920407 :   virtual ~TheoryInference() {}
      41                 :            : 
      42                 :            :   /**
      43                 :            :    * Process lemma, return the trust node to pass to
      44                 :            :    * TheoryInferenceManager::trustedLemma. In addition, the inference should
      45                 :            :    * process any internal side effects of the lemma.
      46                 :            :    *
      47                 :            :    * @param p The property of the lemma which will be passed to trustedLemma
      48                 :            :    * for this inference. If this call does not update p, the default value will
      49                 :            :    * be used.
      50                 :            :    * @return The trust node (of kind TrustNodeKind::LEMMA) corresponding to the
      51                 :            :    * lemma and its proof generator.
      52                 :            :    */
      53                 :          0 :   virtual TrustNode processLemma(LemmaProperty& p) { return TrustNode::null(); }
      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(std::vector<Node>& exp, ProofGenerator*& pg)
      65                 :            :   {
      66                 :          0 :     return Node::null();
      67                 :            :   }
      68                 :            : 
      69                 :            :   /** Get the InferenceId of this theory inference. */
      70                 :    1130660 :   InferenceId getId() const { return d_id; }
      71                 :            :   /** Set the InferenceId of this theory inference. */
      72                 :      18291 :   void setId(InferenceId id) { d_id = id; }
      73                 :            : 
      74                 :            :  private:
      75                 :            :   InferenceId d_id;
      76                 :            : };
      77                 :            : 
      78                 :            : /**
      79                 :            :  * A simple theory lemma with no side effects. Makes a single call to
      80                 :            :  * trustedLemma in its process method.
      81                 :            :  */
      82                 :            : class SimpleTheoryLemma : public TheoryInference
      83                 :            : {
      84                 :            :  public:
      85                 :            :   SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
      86                 :     419821 :   virtual ~SimpleTheoryLemma() {}
      87                 :            :   /** Process lemma */
      88                 :            :   TrustNode processLemma(LemmaProperty& p) override;
      89                 :            :   /** The lemma to send */
      90                 :            :   Node d_node;
      91                 :            :   /** The lemma property (see OutputChannel::lemma) */
      92                 :            :   LemmaProperty d_property;
      93                 :            :   /**
      94                 :            :    * The proof generator for this lemma, which if non-null, is wrapped in a
      95                 :            :    * TrustNode to be set on the output channel via trustedLemma at the time
      96                 :            :    * the lemma is sent. This proof generator must be able to provide a proof
      97                 :            :    * for d_node in the remainder of the user context.
      98                 :            :    */
      99                 :            :   ProofGenerator* d_pg;
     100                 :            : };
     101                 :            : 
     102                 :            : /**
     103                 :            :  * A simple internal fact with no side effects. Makes a single call to
     104                 :            :  * assertInternalFact in its process method.
     105                 :            :  */
     106                 :            : class SimpleTheoryInternalFact : public TheoryInference
     107                 :            : {
     108                 :            :  public:
     109                 :            :   SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
     110                 :     343151 :   virtual ~SimpleTheoryInternalFact() {}
     111                 :            :   /** Process internal fact */
     112                 :            :   Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
     113                 :            :   /** The lemma to send */
     114                 :            :   Node d_conc;
     115                 :            :   /** The explanation */
     116                 :            :   Node d_exp;
     117                 :            :   /** The proof generator */
     118                 :            :   ProofGenerator* d_pg;
     119                 :            : };
     120                 :            : 
     121                 :            : }  // namespace theory
     122                 :            : }  // namespace cvc5::internal
     123                 :            : 
     124                 :            : #endif