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