src/theory/theory_inference_manager.h

   1 /*********************                                                        */
   2 /*! \file theory_inference_manager.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 An inference manager for Theory
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
  18 #define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
  19
  20 #include "context/cdhashset.h"
  21 #include "expr/node.h"
  22 #include "theory/output_channel.h"
  23 #include "theory/theory_state.h"
  24 #include "theory/trust_node.h"
  25
  26 namespace CVC4 {
  27
  28 class ProofNodeManager;
  29
  30 namespace theory {
  31
  32 class Theory;
  33 namespace eq {
  34 class EqualityEngine;
  35 }
  36
  37 /**
  38  * The base class for inference manager. An inference manager is a wrapper
  39  * around the output channel and the official equality engine of a Theory.
  40  * It is used for ensuring that the equality engine and output channel
  41  * are used properly. This includes the following invariants:
  42  *
  43  * (1) The state tracks conflicts.
  44  * In particular, TheoryState::isInConflict returns true whenever we have
  45  * called OutputChannel::conflict in the current context, which we enforce
  46  * by always setting d_state.notifyInConflict at the same time we send
  47  * conflicts on the output channel.
  48  *
  49  * (2) The theory is notified of (internal) facts.
  50  * In particular, Theory::preNotifyFact and Theory::notifyFact are called
  51  * (with isInternal = true) whenever we assert internal facts using
  52  * assertFactInernal below, mirroring what is done for facts from the fact
  53  * queue (where isInternal = false).
  54  */
  55 class TheoryInferenceManager
  56 {
  57   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  58
  59  public:
  60   /**
  61    * Constructor, note that state should be the official state of theory t.
  62    */
  63   TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
  64   virtual ~TheoryInferenceManager() {}
  65   //--------------------------------------- initialization
  66   /**
  67    * Set equality engine, ee is a pointer to the official equality engine
  68    * of theory.
  69    */
  70   void setEqualityEngine(eq::EqualityEngine* ee);
  71   //--------------------------------------- end initialization
  72   /**
  73    * T-propagate literal lit, possibly encountered by equality engine,
  74    * returns false if we are in conflict.
  75    *
  76    * Note that this is the preferred method to call on
  77    * EqualityEngineNotify::eqNotifyTriggerPredicate and
  78    * EqualityEngineNotify::eqNotifyTriggerTermEquality.
  79    */
  80   bool propagateLit(TNode lit);
  81   /**
  82    * Return an explanation for the literal represented by parameter lit
  83    * (which was previously propagated by this theory). By default, this
  84    * returns the explanation given by the official equality engine of the
  85    * Theory, if it exists.
  86    */
  87   virtual TrustNode explainLit(TNode lit);
  88   /**
  89    * Raise conflict, called when constants a and b merge. Sends the conflict
  90    * on the output channel corresponding to the equality engine's explanation
  91    * of (= a b). The proof equality engine (if it exists) will be used as the
  92    * proof generator.
  93    *
  94    * Note that this is the preferred method to call on
  95    * EqualityEngineNotify::eqNotifyConstantTermMerge.
  96    */
  97   void conflictEqConstantMerge(TNode a, TNode b);
  98   /**
  99    * Raise conflict conf (of any form), without proofs. This method should
 100    * only be called if there is not yet proof support in the given theory.
 101    */
 102   void conflict(TNode conf);
 103   /**
 104    * Raise trusted conflict tconf (of any form) where a proof generator has
 105    * been provided in a custom way.
 106    */
 107   void trustedConflict(TrustNode tconf);
 108   /** Send lemma lem with property p on the output channel. */
 109   LemmaStatus lemma(TNode lem, LemmaProperty p = LemmaProperty::NONE);
 110   /** Send (trusted) lemma lem with property p on the output channel. */
 111   LemmaStatus trustedLemma(const TrustNode& tlem,
 112                            LemmaProperty p = LemmaProperty::NONE);
 113   /**
 114    * Assert internal fact. This is recommended method for asserting "internal"
 115    * facts into the equality engine of the theory. In particular, this method
 116    * should be used for anything the theory infers that is not sent on the
 117    * output channel as a propagation or lemma. This method ensures that the
 118    * Theory's preNotifyFact and notifyFact method have been called with
 119    * isInternal = true.
 120    */
 121   void assertInternalFact(TNode atom, bool pol, TNode fact);
 122
 123  protected:
 124   /**
 125    * Explain conflict from constants merging in the equality engine. This
 126    * method is called by conflictEqConstantMerge. By default, it returns
 127    * the explanation of the official equality engine of the theory, if it
 128    * exists.
 129    */
 130   virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
 131   /** The theory object */
 132   Theory& d_theory;
 133   /** Reference to the state of theory */
 134   TheoryState& d_theoryState;
 135   /** Reference to the output channel of the theory */
 136   OutputChannel& d_out;
 137   /** Pointer to equality engine of the theory. */
 138   eq::EqualityEngine* d_ee;
 139   /** The proof node manager of the theory */
 140   ProofNodeManager* d_pnm;
 141   /**
 142    * The keep set of this class. This set is maintained to ensure that
 143    * facts and their explanations are ref-counted. Since facts and their
 144    * explanations are SAT-context-dependent, this set is also
 145    * SAT-context-dependent.
 146    */
 147   NodeSet d_keep;
 148 };
 149
 150 }  // namespace theory
 151 }  // namespace CVC4
 152
 153 #endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */