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 <memory>
  21
  22 #include "context/cdhashset.h"
  23 #include "expr/node.h"
  24 #include "theory/output_channel.h"
  25 #include "theory/theory_state.h"
  26 #include "theory/trust_node.h"
  27 #include "theory/uf/proof_equality_engine.h"
  28
  29 namespace CVC4 {
  30
  31 class ProofNodeManager;
  32
  33 namespace theory {
  34
  35 class Theory;
  36 namespace eq {
  37 class EqualityEngine;
  38 }
  39
  40 /**
  41  * The base class for inference manager. An inference manager is a wrapper
  42  * around the output channel and the official equality engine of a Theory.
  43  * It is used for ensuring that the equality engine and output channel
  44  * are used properly. This includes the following invariants:
  45  *
  46  * (1) The state tracks conflicts.
  47  * In particular, TheoryState::isInConflict returns true whenever we have
  48  * called OutputChannel::conflict in the current context, which we enforce
  49  * by always setting d_state.notifyInConflict at the same time we send
  50  * conflicts on the output channel.
  51  *
  52  * (2) The theory is notified of (internal) facts.
  53  * In particular, Theory::preNotifyFact and Theory::notifyFact are called
  54  * (with isInternal = true) whenever we assert internal facts using
  55  * assertFactInernal below, mirroring what is done for facts from the fact
  56  * queue (where isInternal = false).
  57  *
  58  * (3) The proof equality engine is used whenever proofs are enabled (when
  59  * the proof node manager provided to this class is non-null). Notice this
  60  * class automatically will construct a proof equality engine during
  61  * setEqualityEngine, and use it for handling variants of assertInternalFact
  62  * below that involve proofs.
  63  */
  64 class TheoryInferenceManager
  65 {
  66   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  67
  68  public:
  69   /**
  70    * Constructor, note that state should be the official state of theory t.
  71    */
  72   TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
  73   virtual ~TheoryInferenceManager() {}
  74   /**
  75    * Set equality engine, ee is a pointer to the official equality engine
  76    * of theory.
  77    */
  78   void setEqualityEngine(eq::EqualityEngine* ee);
  79   /**
  80    * Reset, which resets counters regarding the number of added lemmas and
  81    * internal facts. This method should be manually called by the theory at
  82    * the appropriate time for the purpose of tracking the usage of this
  83    * inference manager.
  84    *
  85    * For example, some theories implement an internal checking loop that
  86    * repeats while new facts are added. The theory should call reset at the
  87    * beginning of this loop and repeat its strategy while hasAddedFact is true.
  88    */
  89   void reset();
  90   //--------------------------------------- propagations
  91   /**
  92    * T-propagate literal lit, possibly encountered by equality engine,
  93    * returns false if we are in conflict.
  94    *
  95    * Note that this is the preferred method to call on
  96    * EqualityEngineNotify::eqNotifyTriggerPredicate and
  97    * EqualityEngineNotify::eqNotifyTriggerTermEquality.
  98    */
  99   bool propagateLit(TNode lit);
 100   /**
 101    * Return an explanation for the literal represented by parameter lit
 102    * (which was previously propagated by this theory). By default, this
 103    * returns the explanation given by the official equality engine of the
 104    * Theory, if it exists.
 105    */
 106   virtual TrustNode explainLit(TNode lit);
 107   //--------------------------------------- conflicts
 108   /**
 109    * Raise conflict, called when constants a and b merge. Sends the conflict
 110    * on the output channel corresponding to the equality engine's explanation
 111    * of (= a b). The proof equality engine (if it exists) will be used as the
 112    * proof generator.
 113    *
 114    * Note that this is the preferred method to call on
 115    * EqualityEngineNotify::eqNotifyConstantTermMerge.
 116    */
 117   void conflictEqConstantMerge(TNode a, TNode b);
 118   /**
 119    * Raise conflict conf (of any form), without proofs. This method should
 120    * only be called if there is not yet proof support in the given theory.
 121    */
 122   void conflict(TNode conf);
 123   /**
 124    * Raise trusted conflict tconf (of any form) where a proof generator has
 125    * been provided in a custom way.
 126    */
 127   void trustedConflict(TrustNode tconf);
 128   /**
 129    * Explain and send conflict from contradictory facts. This method is called
 130    * when the proof rule id with premises exp and arguments args concludes
 131    * false. This method sends a trusted conflict corresponding to the official
 132    * equality engine's explanation of literals in exp, with the proof equality
 133    * engine as the proof generator (if it exists).
 134    */
 135   void conflictExp(PfRule id,
 136                    const std::vector<Node>& exp,
 137                    const std::vector<Node>& args);
 138   //--------------------------------------- lemmas
 139   /**
 140    * Send (trusted) lemma lem with property p on the output channel.
 141    *
 142    * @param tlem The trust node containing the lemma and its proof generator.
 143    * @param p The property of the lemma
 144    * @param doCache If true, we send the lemma only if it has not already been
 145    * cached (see cacheLemma), and add it to the cache during this call.
 146    * @return true if the lemma was sent on the output channel.
 147    */
 148   bool trustedLemma(const TrustNode& tlem,
 149                     LemmaProperty p = LemmaProperty::NONE,
 150                     bool doCache = true);
 151   /**
 152    * Send lemma lem with property p on the output channel. Same as above, with
 153    * a node instead of a trust node.
 154    */
 155   bool lemma(TNode lem,
 156              LemmaProperty p = LemmaProperty::NONE,
 157              bool doCache = true);
 158   /**
 159    * Explained lemma. This should be called when
 160    *   ( exp => conc )
 161    * is a valid theory lemma. This method adds a lemma where part of exp
 162    * is replaced by its explanation according to the official equality engine
 163    * of the theory.
 164    *
 165    * In particular, this method adds a lemma on the output channel of the form
 166    *   ( ^_{e in exp \ noExplain} EXPLAIN(e) ^ noExplain ) => conc
 167    * where EXPLAIN(e) returns the explanation of literal e according to the
 168    * official equality engine of the theory. Note that noExplain is the *subset*
 169    * of exp that should not be explained.
 170    *
 171    * @param conc The conclusion of the lemma
 172    * @param id The proof rule concluding conc
 173    * @param exp The set of (all) literals that imply conc
 174    * @param noExplain The subset of exp that should not be explained by the
 175    * equality engine
 176    * @param args The arguments to the proof step concluding conc
 177    * @param p The property of the lemma
 178    * @param doCache Whether to check and add the lemma to the cache
 179    * @return true if the lemma was sent on the output channel.
 180    */
 181   bool lemmaExp(Node conc,
 182                 PfRule id,
 183                 const std::vector<Node>& exp,
 184                 const std::vector<Node>& noExplain,
 185                 const std::vector<Node>& args,
 186                 LemmaProperty p = LemmaProperty::NONE,
 187                 bool doCache = true);
 188   /**
 189    * Same as above, but where pg can provide a proof of conc from free
 190    * assumptions in exp. It is required to do so in the remainder of the user
 191    * context when this method returns true.
 192    *
 193    * @param conc The conclusion of the lemma
 194    * @param exp The set of (all) literals that imply conc
 195    * @param noExplain The subset of exp that should not be explained by the
 196    * equality engine
 197    * @param pg If non-null, the proof generator who can provide a proof of conc.
 198    * @param p The property of the lemma
 199    * @param doCache Whether to check and add the lemma to the cache
 200    * @return true if the lemma was sent on the output channel.
 201    */
 202   bool lemmaExp(Node conc,
 203                 const std::vector<Node>& exp,
 204                 const std::vector<Node>& noExplain,
 205                 ProofGenerator* pg = nullptr,
 206                 LemmaProperty p = LemmaProperty::NONE,
 207                 bool doCache = true);
 208   /**
 209    * Has this inference manager cached and sent the given lemma (in this user
 210    * context)? This method can be overridden by the particular manager. If not,
 211    * this returns true if lem is in the cache d_lemmasSent maintained by this
 212    * class. Notice that the default cache in this base class is not dependent
 213    * on the lemma property.
 214    */
 215   virtual bool hasCachedLemma(TNode lem, LemmaProperty p);
 216   /** The number of lemmas we have sent since the last call to reset */
 217   uint32_t numAddedLemmas() const;
 218   /** Have we added a lemma since the last call to reset? */
 219   bool hasAddedLemma() const;
 220   //--------------------------------------- internal facts
 221   /**
 222    * Assert internal fact. This is recommended method for asserting "internal"
 223    * facts into the equality engine of the theory. In particular, this method
 224    * should be used for anything the theory infers that is not sent on the
 225    * output channel as a propagation or lemma. This method ensures that the
 226    * Theory's preNotifyFact and notifyFact method have been called with
 227    * isInternal = true.
 228    *
 229    * @param atom The atom of the fact to assert
 230    * @param pol Its polarity
 231    * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.
 232    */
 233   void assertInternalFact(TNode atom, bool pol, TNode exp);
 234   /**
 235    * Assert internal fact, with a proof step justification. Notice that if
 236    * proofs are not enabled in this inference manager, then this asserts
 237    * a fact to the equality engine in the normal way.
 238    *
 239    * @param atom The atom of the fact to assert
 240    * @param pol Its polarity
 241    * @param id The proof rule identifier of the proof step
 242    * @param exp Its explanation, interpreted as a conjunction
 243    * @param args The arguments of the proof step
 244    */
 245   void assertInternalFact(TNode atom,
 246                           bool pol,
 247                           PfRule id,
 248                           const std::vector<Node>& exp,
 249                           const std::vector<Node>& args);
 250   /**
 251    * Assert internal fact, with a proof generator justification. Same as above,
 252    * but with a proof generator instead of an explicit step.
 253    *
 254    * @param atom The atom of the fact to assert
 255    * @param pol Its polarity
 256    * @param exp Its explanation, interpreted as a conjunction
 257    * @param pg The proof generator for this step. If non-null, pg must be able
 258    * to provide a proof concluding (~) atom from free asumptions in exp in
 259    * the remainder of the current SAT context.
 260    */
 261   void assertInternalFact(TNode atom,
 262                           bool pol,
 263                           const std::vector<Node>& exp,
 264                           ProofGenerator* pg);
 265   /** The number of internal facts we have added since the last call to reset */
 266   uint32_t numAddedFacts() const;
 267   /** Have we added a internal fact since the last call to reset? */
 268   bool hasAddedFact() const;
 269
 270  protected:
 271   /**
 272    * Process internal fact. This is a common helper method for the
 273    * assertInternalFact variants above.
 274    */
 275   void processInternalFact(TNode atom,
 276                            bool pol,
 277                            PfRule id,
 278                            const std::vector<Node>& exp,
 279                            const std::vector<Node>& args,
 280                            ProofGenerator* pg);
 281   /**
 282    * Explain conflict from constants merging in the equality engine. This
 283    * method is called by conflictEqConstantMerge. By default, it returns
 284    * the explanation of the official equality engine of the theory, if it
 285    * exists.
 286    */
 287   virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
 288   /**
 289    * Explain formula n (which is possibly a conjunction with no nested
 290    * conjunctions), add its explanation to assumptions.
 291    */
 292   void explain(TNode n, std::vector<TNode>& assumptions);
 293   /**
 294    * Explain formula n (which is possibly a conjunction with no nested
 295    * conjunctions), return the explanation as a conjunction.
 296    */
 297   Node mkExplain(TNode n);
 298   /**
 299    * Explain the set of formulas in exp using the official equality engine of
 300    * the theory. We ask the equality engine to explain literals in exp
 301    * that do not occur in noExplain, and return unchanged those that occur in
 302    * noExplain. Note the vector noExplain should be a subset of exp.
 303    */
 304   Node mkExplainPartial(const std::vector<Node>& exp,
 305                         const std::vector<Node>& noExplain);
 306   /**
 307    * Cache that lemma lem is being sent with property p. Return true if it
 308    * did not already exist in the cache maintained by this class. If this
 309    * method is not overridden, then we use the d_lemmasSent cache maintained
 310    * by this class, which notice is not dependent on lemma property. If
 311    * the lemma property should be taken into account, the manager should
 312    * override this method to take the lemma property into account as needed.
 313    */
 314   virtual bool cacheLemma(TNode lem, LemmaProperty p);
 315   /** The theory object */
 316   Theory& d_theory;
 317   /** Reference to the state of theory */
 318   TheoryState& d_theoryState;
 319   /** Reference to the output channel of the theory */
 320   OutputChannel& d_out;
 321   /** Pointer to equality engine of the theory. */
 322   eq::EqualityEngine* d_ee;
 323   /** A proof equality engine */
 324   std::unique_ptr<eq::ProofEqEngine> d_pfee;
 325   /** The proof node manager of the theory */
 326   ProofNodeManager* d_pnm;
 327   /**
 328    * The keep set of this class. This set is maintained to ensure that
 329    * facts and their explanations are ref-counted. Since facts and their
 330    * explanations are SAT-context-dependent, this set is also
 331    * SAT-context-dependent.
 332    */
 333   NodeSet d_keep;
 334   /**
 335    * A cache of all lemmas sent, which is a user-context-dependent set of
 336    * nodes. Notice that this cache does not depedent on lemma property.
 337    */
 338   NodeSet d_lemmasSent;
 339   /** The number of lemmas sent since the last call to reset. */
 340   uint32_t d_numCurrentLemmas;
 341   /** The number of internal facts added since the last call to reset. */
 342   uint32_t d_numCurrentFacts;
 343 };
 344
 345 }  // namespace theory
 346 }  // namespace CVC4
 347
 348 #endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */