src/theory/theory_inference.h

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