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    * Called by the provided inference manager to process this inference. This
  42    * method should make call(s) to inference manager to process this
  43    * inference, as well as processing any specific side effects. This method
  44    * typically makes a single call to the provided inference manager e.g.
  45    * d_im->trustedLemma or d_im->assertInternalFact. Notice it is the sole
  46    * responsibility of this class to make this call; the inference manager
  47    * does not call itself otherwise when processing pending inferences.
  48    *
  49    * @param im The inference manager to use
  50    * @param asLemma Whether this inference is being processed as a lemma
  51    * during doPendingLemmas (otherwise it is being processed in doPendingFacts).
  52    * Typically, this method calls lemma or conflict when asLemma is
  53    * true, and assertInternalFact when this flag is false, although this
  54    * behavior is (intentionally) not strictly enforced. In particular, the
  55    * choice to send a conflict, lemma or fact may depend on local state of the
  56    * theory, which may change while the inference is pending. Hence the
  57    * implementation of this method may choose to implement any call to the
  58    * inference manager. This flag simply serves to track whether the inference
  59    * initially was added a pending lemma or not.
  60    * @return true if the inference was successfully processed by the inference
  61    * manager. This method for instance returns false if it corresponds to a
  62    * lemma that was already cached by im and hence was discarded.
  63    */
  64   virtual bool process(TheoryInferenceManager* im, bool asLemma) = 0;
  65
  66   /** Get the InferenceId of this theory inference. */
  67   InferenceId getId() const { return d_id; }
  68   /** Set the InferenceId of this theory inference. */
  69   void setId(InferenceId id) { d_id = id; }
  70
  71  private:
  72   InferenceId d_id;
  73 };
  74
  75 /**
  76  * A simple theory lemma with no side effects. Makes a single call to
  77  * trustedLemma in its process method.
  78  */
  79 class SimpleTheoryLemma : public TheoryInference
  80 {
  81  public:
  82   SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
  83   virtual ~SimpleTheoryLemma() {}
  84   /**
  85    * Send the lemma using inference manager im, return true if the lemma was
  86    * sent. It should be the case that asLemma = true or an assertion failure
  87    * is thrown.
  88    */
  89   virtual bool process(TheoryInferenceManager* im, bool asLemma) override;
  90   /** The lemma to send */
  91   Node d_node;
  92   /** The lemma property (see OutputChannel::lemma) */
  93   LemmaProperty d_property;
  94   /**
  95    * The proof generator for this lemma, which if non-null, is wrapped in a
  96    * TrustNode to be set on the output channel via trustedLemma at the time
  97    * the lemma is sent. This proof generator must be able to provide a proof
  98    * for d_node in the remainder of the user context.
  99    */
 100   ProofGenerator* d_pg;
 101 };
 102
 103 /**
 104  * A simple internal fact with no side effects. Makes a single call to
 105  * assertInternalFact in its process method.
 106  */
 107 class SimpleTheoryInternalFact : public TheoryInference
 108 {
 109  public:
 110   SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
 111   virtual ~SimpleTheoryInternalFact() {}
 112   /**
 113    * Send the lemma using inference manager im, return true if the lemma was
 114    * sent. It should be the case that asLemma = false or an assertion failure
 115    * is thrown.
 116    */
 117   virtual bool process(TheoryInferenceManager* im, bool asLemma) override;
 118   /** The lemma to send */
 119   Node d_conc;
 120   /** The explanation */
 121   Node d_exp;
 122   /** The proof generator */
 123   ProofGenerator* d_pg;
 124 };
 125
 126 }  // namespace theory
 127 }  // namespace CVC4
 128
 129 #endif