src/theory/theory_inference_manager.h

   1 /*********************                                                        */
   2 /*! \file theory_inference_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
   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    * Are proofs enabled in this inference manager? Returns true if the proof
  81    * node manager pnm provided to the constructor of this class was non-null.
  82    */
  83   bool isProofEnabled() const;
  84   /**
  85    * Reset, which resets counters regarding the number of added lemmas and
  86    * internal facts. This method should be manually called by the theory at
  87    * the appropriate time for the purpose of tracking the usage of this
  88    * inference manager.
  89    *
  90    * For example, some theories implement an internal checking loop that
  91    * repeats while new facts are added. The theory should call reset at the
  92    * beginning of this loop and repeat its strategy while hasAddedFact is true.
  93    */
  94   void reset();
  95   /**
  96    * Returns true if we are in conflict, or if we have sent a lemma or fact
  97    * since the last call to reset.
  98    */
  99   bool hasSent() const;
 100   /** Get the underlying proof equality engine */
 101   eq::ProofEqEngine* getProofEqEngine();
 102   //--------------------------------------- propagations
 103   /**
 104    * T-propagate literal lit, possibly encountered by equality engine,
 105    * returns false if we are in conflict.
 106    *
 107    * Note that this is the preferred method to call on
 108    * EqualityEngineNotify::eqNotifyTriggerPredicate and
 109    * EqualityEngineNotify::eqNotifyTriggerTermEquality.
 110    */
 111   bool propagateLit(TNode lit);
 112   /**
 113    * Return an explanation for the literal represented by parameter lit
 114    * (which was previously propagated by this theory). By default, this
 115    * returns the explanation given by the official equality engine of the
 116    * Theory, if it exists.
 117    */
 118   virtual TrustNode explainLit(TNode lit);
 119   //--------------------------------------- conflicts
 120   /**
 121    * Raise conflict, called when constants a and b merge. Sends the conflict
 122    * on the output channel corresponding to the equality engine's explanation
 123    * of (= a b). The proof equality engine (if it exists) will be used as the
 124    * proof generator.
 125    *
 126    * Note that this is the preferred method to call on
 127    * EqualityEngineNotify::eqNotifyConstantTermMerge.
 128    */
 129   void conflictEqConstantMerge(TNode a, TNode b);
 130   /**
 131    * Raise conflict conf (of any form), without proofs. This method should
 132    * only be called if there is not yet proof support in the given theory.
 133    */
 134   void conflict(TNode conf);
 135   /**
 136    * Raise trusted conflict tconf (of any form) where a proof generator has
 137    * been provided (as part of the trust node) in a custom way.
 138    */
 139   void trustedConflict(TrustNode tconf);
 140   /**
 141    * Explain and send conflict from contradictory facts. This method is called
 142    * when the proof rule id with premises exp and arguments args concludes
 143    * false. This method sends a trusted conflict corresponding to the official
 144    * equality engine's explanation of literals in exp, with the proof equality
 145    * engine as the proof generator (if it exists).
 146    */
 147   void conflictExp(PfRule id,
 148                    const std::vector<Node>& exp,
 149                    const std::vector<Node>& args);
 150   /**
 151    * Make the trust node corresponding to the conflict of the above form. It is
 152    * the responsibility of the caller to subsequently call trustedConflict with
 153    * the returned trust node.
 154    */
 155   TrustNode mkConflictExp(PfRule id,
 156                           const std::vector<Node>& exp,
 157                           const std::vector<Node>& args);
 158   /**
 159    * Explain and send conflict from contradictory facts. This method is called
 160    * when proof generator pg has a proof of false from free assumptions exp.
 161    * This method sends a trusted conflict corresponding to the official
 162    * equality engine's explanation of literals in exp, with the proof equality
 163    * engine as the proof generator (if it exists), where pg provides the
 164    * final step(s) of this proof during this call.
 165    */
 166   void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
 167   /**
 168    * Make the trust node corresponding to the conflict of the above form. It is
 169    * the responsibility of the caller to subsequently call trustedConflict with
 170    * the returned trust node.
 171    */
 172   TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
 173   //--------------------------------------- lemmas
 174   /**
 175    * Send (trusted) lemma lem with property p on the output channel.
 176    *
 177    * @param tlem The trust node containing the lemma and its proof generator.
 178    * @param p The property of the lemma
 179    * @param doCache If true, we send the lemma only if it has not already been
 180    * cached (see cacheLemma), and add it to the cache during this call.
 181    * @return true if the lemma was sent on the output channel.
 182    */
 183   bool trustedLemma(const TrustNode& tlem,
 184                     LemmaProperty p = LemmaProperty::NONE,
 185                     bool doCache = true);
 186   /**
 187    * Send lemma lem with property p on the output channel. Same as above, with
 188    * a node instead of a trust node.
 189    */
 190   bool lemma(TNode lem,
 191              LemmaProperty p = LemmaProperty::NONE,
 192              bool doCache = true);
 193   /**
 194    * Explained lemma. This should be called when
 195    *   ( exp => conc )
 196    * is a valid theory lemma. This method adds a lemma where part of exp
 197    * is replaced by its explanation according to the official equality engine
 198    * of the theory.
 199    *
 200    * In particular, this method adds a lemma on the output channel of the form
 201    *   ( ^_{e in exp \ noExplain} EXPLAIN(e) ^ noExplain ) => conc
 202    * where EXPLAIN(e) returns the explanation of literal e according to the
 203    * official equality engine of the theory. Note that noExplain is the *subset*
 204    * of exp that should not be explained.
 205    *
 206    * @param conc The conclusion of the lemma
 207    * @param id The proof rule concluding conc
 208    * @param exp The set of (all) literals that imply conc
 209    * @param noExplain The subset of exp that should not be explained by the
 210    * equality engine
 211    * @param args The arguments to the proof step concluding conc
 212    * @param p The property of the lemma
 213    * @param doCache Whether to check and add the lemma to the cache
 214    * @return true if the lemma was sent on the output channel.
 215    */
 216   bool lemmaExp(Node conc,
 217                 PfRule id,
 218                 const std::vector<Node>& exp,
 219                 const std::vector<Node>& noExplain,
 220                 const std::vector<Node>& args,
 221                 LemmaProperty p = LemmaProperty::NONE,
 222                 bool doCache = true);
 223   /**
 224    * Make the trust node for the above method. It is responsibility of the
 225    * caller to subsequently call trustedLemma with the returned trust node.
 226    */
 227   TrustNode mkLemmaExp(Node conc,
 228                        PfRule id,
 229                        const std::vector<Node>& exp,
 230                        const std::vector<Node>& noExplain,
 231                        const std::vector<Node>& args);
 232   /**
 233    * Same as above, but where pg can provide a proof of conc from free
 234    * assumptions in exp. This sends a trusted lemma on the output channel where
 235    * the proof equality engine is the proof generator. The generator pg
 236    * is asked to provide the final step(s) of this proof during this call.
 237    *
 238    * @param conc The conclusion of the lemma
 239    * @param exp The set of (all) literals that imply conc
 240    * @param noExplain The subset of exp that should not be explained by the
 241    * equality engine
 242    * @param pg If non-null, the proof generator who can provide a proof of conc.
 243    * @param p The property of the lemma
 244    * @param doCache Whether to check and add the lemma to the cache
 245    * @return true if the lemma was sent on the output channel.
 246    */
 247   bool lemmaExp(Node conc,
 248                 const std::vector<Node>& exp,
 249                 const std::vector<Node>& noExplain,
 250                 ProofGenerator* pg = nullptr,
 251                 LemmaProperty p = LemmaProperty::NONE,
 252                 bool doCache = true);
 253   /**
 254    * Make the trust node for the above method. It is responsibility of the
 255    * caller to subsequently call trustedLemma with the returned trust node.
 256    */
 257   TrustNode mkLemmaExp(Node conc,
 258                        const std::vector<Node>& exp,
 259                        const std::vector<Node>& noExplain,
 260                        ProofGenerator* pg = nullptr);
 261   /**
 262    * Has this inference manager cached and sent the given lemma (in this user
 263    * context)? This method can be overridden by the particular manager. If not,
 264    * this returns true if lem is in the cache d_lemmasSent maintained by this
 265    * class. Notice that the default cache in this base class is not dependent
 266    * on the lemma property.
 267    */
 268   virtual bool hasCachedLemma(TNode lem, LemmaProperty p);
 269   /** The number of lemmas we have sent since the last call to reset */
 270   uint32_t numSentLemmas() const;
 271   /** Have we added a lemma since the last call to reset? */
 272   bool hasSentLemma() const;
 273   //--------------------------------------- internal facts
 274   /**
 275    * Assert internal fact. This is recommended method for asserting "internal"
 276    * facts into the equality engine of the theory. In particular, this method
 277    * should be used for anything the theory infers that is not sent on the
 278    * output channel as a propagation or lemma. This method ensures that the
 279    * Theory's preNotifyFact and notifyFact method have been called with
 280    * isInternal = true.
 281    *
 282    * @param atom The atom of the fact to assert
 283    * @param pol Its polarity
 284    * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.
 285    * @return true if the fact was processed, i.e. it was asserted to the
 286    * equality engine or preNotifyFact returned true.
 287    */
 288   bool assertInternalFact(TNode atom, bool pol, TNode exp);
 289   /**
 290    * Assert internal fact, with a proof step justification. Notice that if
 291    * proofs are not enabled in this inference manager, then this asserts
 292    * a fact to the equality engine in the normal way.
 293    *
 294    * @param atom The atom of the fact to assert
 295    * @param pol Its polarity
 296    * @param id The proof rule identifier of the proof step
 297    * @param exp Its explanation, interpreted as a conjunction
 298    * @param args The arguments of the proof step
 299    * @return true if the fact was processed, i.e. it was asserted to the
 300    * equality engine or preNotifyFact returned true.
 301    */
 302   bool assertInternalFact(TNode atom,
 303                           bool pol,
 304                           PfRule id,
 305                           const std::vector<Node>& exp,
 306                           const std::vector<Node>& args);
 307   /**
 308    * Assert internal fact, with a proof generator justification. Same as above,
 309    * but with a proof generator instead of an explicit step.
 310    *
 311    * @param atom The atom of the fact to assert
 312    * @param pol Its polarity
 313    * @param exp Its explanation, interpreted as a conjunction
 314    * @param pg The proof generator for this step. If non-null, pg must be able
 315    * to provide a proof concluding (~) atom from free asumptions in exp in
 316    * the remainder of the current SAT context.
 317    * @return true if the fact was processed, i.e. it was asserted to the
 318    * equality engine or preNotifyFact returned true.
 319    */
 320   bool assertInternalFact(TNode atom,
 321                           bool pol,
 322                           const std::vector<Node>& exp,
 323                           ProofGenerator* pg);
 324   /** The number of internal facts we have added since the last call to reset */
 325   uint32_t numSentFacts() const;
 326   /** Have we added a internal fact since the last call to reset? */
 327   bool hasSentFact() const;
 328   //--------------------------------------- phase requirements
 329   /**
 330    * Set that literal n has SAT phase requirement pol, that is, it should be
 331    * decided with polarity pol, for details see OutputChannel::requirePhase.
 332    */
 333   void requirePhase(TNode n, bool pol);
 334
 335   /**
 336    * Forward to OutputChannel::spendResource() to spend resources.
 337    */
 338   void spendResource(ResourceManager::Resource r);
 339
 340   /**
 341    * Forward to OutputChannel::safePoint() to spend resources.
 342    */
 343   void safePoint(ResourceManager::Resource r);
 344   /**
 345    * Notification from a theory that it realizes it is incomplete at
 346    * this context level.
 347    */
 348   void setIncomplete();
 349
 350  protected:
 351   /**
 352    * Process internal fact. This is a common helper method for the
 353    * assertInternalFact variants above. Returns true if the fact was processed.
 354    */
 355   bool processInternalFact(TNode atom,
 356                            bool pol,
 357                            PfRule id,
 358                            const std::vector<Node>& exp,
 359                            const std::vector<Node>& args,
 360                            ProofGenerator* pg);
 361   /**
 362    * Explain conflict from constants merging in the equality engine. This
 363    * method is called by conflictEqConstantMerge. By default, it returns
 364    * the explanation of the official equality engine of the theory, if it
 365    * exists.
 366    */
 367   virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
 368   /**
 369    * Explain formula n (which is possibly a conjunction with no nested
 370    * conjunctions), add its explanation to assumptions.
 371    */
 372   void explain(TNode n, std::vector<TNode>& assumptions);
 373   /**
 374    * Explain formula n (which is possibly a conjunction with no nested
 375    * conjunctions), return the explanation as a conjunction.
 376    */
 377   Node mkExplain(TNode n);
 378   /**
 379    * Explain the set of formulas in exp using the official equality engine of
 380    * the theory. We ask the equality engine to explain literals in exp
 381    * that do not occur in noExplain, and return unchanged those that occur in
 382    * noExplain. Note the vector noExplain should be a subset of exp.
 383    */
 384   Node mkExplainPartial(const std::vector<Node>& exp,
 385                         const std::vector<Node>& noExplain);
 386   /**
 387    * Cache that lemma lem is being sent with property p. Return true if it
 388    * did not already exist in the cache maintained by this class. If this
 389    * method is not overridden, then we use the d_lemmasSent cache maintained
 390    * by this class, which notice is not dependent on lemma property. If
 391    * the lemma property should be taken into account, the manager should
 392    * override this method to take the lemma property into account as needed.
 393    */
 394   virtual bool cacheLemma(TNode lem, LemmaProperty p);
 395   /** The theory object */
 396   Theory& d_theory;
 397   /** Reference to the state of theory */
 398   TheoryState& d_theoryState;
 399   /** Reference to the output channel of the theory */
 400   OutputChannel& d_out;
 401   /** Pointer to equality engine of the theory. */
 402   eq::EqualityEngine* d_ee;
 403   /** A proof equality engine */
 404   std::unique_ptr<eq::ProofEqEngine> d_pfee;
 405   /** The proof node manager of the theory */
 406   ProofNodeManager* d_pnm;
 407   /**
 408    * The keep set of this class. This set is maintained to ensure that
 409    * facts and their explanations are ref-counted. Since facts and their
 410    * explanations are SAT-context-dependent, this set is also
 411    * SAT-context-dependent.
 412    */
 413   NodeSet d_keep;
 414   /**
 415    * A cache of all lemmas sent, which is a user-context-dependent set of
 416    * nodes. Notice that this cache does not depedent on lemma property.
 417    */
 418   NodeSet d_lemmasSent;
 419   /** The number of conflicts sent since the last call to reset. */
 420   uint32_t d_numConflicts;
 421   /** The number of lemmas sent since the last call to reset. */
 422   uint32_t d_numCurrentLemmas;
 423   /** The number of internal facts added since the last call to reset. */
 424   uint32_t d_numCurrentFacts;
 425 };
 426
 427 }  // namespace theory
 428 }  // namespace CVC4
 429
 430 #endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */