src/theory/theory_inference_manager.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * An inference manager for Theory.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
  19 #define CVC5__THEORY__THEORY_INFERENCE_MANAGER_H
  20
  21 #include <memory>
  22
  23 #include "context/cdhashset.h"
  24 #include "expr/node.h"
  25 #include "expr/proof_rule.h"
  26 #include "theory/inference_id.h"
  27 #include "theory/output_channel.h"
  28 #include "theory/trust_node.h"
  29 #include "util/statistics_stats.h"
  30
  31 namespace cvc5 {
  32
  33 class ProofNodeManager;
  34
  35 namespace theory {
  36
  37 class Theory;
  38 class TheoryState;
  39 class DecisionManager;
  40 namespace eq {
  41 class EqualityEngine;
  42 class ProofEqEngine;
  43 }
  44
  45 /**
  46  * The base class for inference manager. An inference manager is a wrapper
  47  * around the output channel and the official equality engine of a Theory.
  48  * It is used for ensuring that the equality engine and output channel
  49  * are used properly. This includes the following invariants:
  50  *
  51  * (1) The state tracks conflicts.
  52  * In particular, TheoryState::isInConflict returns true whenever we have
  53  * called OutputChannel::conflict in the current context, which we enforce
  54  * by always setting d_state.notifyInConflict at the same time we send
  55  * conflicts on the output channel.
  56  *
  57  * (2) The theory is notified of (internal) facts.
  58  * In particular, Theory::preNotifyFact and Theory::notifyFact are called
  59  * (with isInternal = true) whenever we assert internal facts using
  60  * assertFactInernal below, mirroring what is done for facts from the fact
  61  * queue (where isInternal = false).
  62  *
  63  * (3) The proof equality engine is used whenever proofs are enabled (when
  64  * the proof node manager provided to this class is non-null). Notice this
  65  * class automatically will construct a proof equality engine during
  66  * setEqualityEngine, and use it for handling variants of assertInternalFact
  67  * below that involve proofs.
  68  */
  69 class TheoryInferenceManager
  70 {
  71   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  72
  73  public:
  74   /**
  75    * Constructor, note that state should be the official state of theory t.
  76    *
  77    * @param t The theory this inference manager is for
  78    * @param state The state of the theory
  79    * @param pnm The proof node manager, which if non-null, enables proofs for
  80    * this inference manager
  81    * @param statsName The name of the inference manager, which is used for
  82    * giving unique names for statistics,
  83    * @param cacheLemmas Whether all lemmas sent using this theory inference
  84    * manager are added to a user-context dependent cache. This means that
  85    * only lemmas that are unique after rewriting are sent to the theory engine
  86    * from this inference manager.
  87    */
  88   TheoryInferenceManager(Theory& t,
  89                          TheoryState& state,
  90                          ProofNodeManager* pnm,
  91                          const std::string& statsName,
  92                          bool cacheLemmas = true);
  93   virtual ~TheoryInferenceManager();
  94   //--------------------------------------- initialization
  95   /**
  96    * Set equality engine, ee is a pointer to the official equality engine
  97    * of theory.
  98    */
  99   void setEqualityEngine(eq::EqualityEngine* ee);
 100   /** Set the decision manager */
 101   void setDecisionManager(DecisionManager* dm);
 102   //--------------------------------------- end initialization
 103   /**
 104    * Are proofs enabled in this inference manager? Returns true if the proof
 105    * node manager pnm provided to the constructor of this class was non-null.
 106    */
 107   bool isProofEnabled() const;
 108   /** Get the underlying proof equality engine */
 109   eq::ProofEqEngine* getProofEqEngine();
 110   /**
 111    * Reset, which resets counters regarding the number of added lemmas and
 112    * internal facts. This method should be manually called by the theory at
 113    * the appropriate time for the purpose of tracking the usage of this
 114    * inference manager.
 115    *
 116    * For example, some theories implement an internal checking loop that
 117    * repeats while new facts are added. The theory should call reset at the
 118    * beginning of this loop and repeat its strategy while hasAddedFact is true.
 119    */
 120   void reset();
 121   /**
 122    * Returns true if we are in conflict, or if we have sent a lemma or fact
 123    * since the last call to reset.
 124    */
 125   bool hasSent() const;
 126   //--------------------------------------- propagations
 127   /**
 128    * T-propagate literal lit, possibly encountered by equality engine,
 129    * returns false if we are in conflict.
 130    *
 131    * Note that this is the preferred method to call on
 132    * EqualityEngineNotify::eqNotifyTriggerPredicate and
 133    * EqualityEngineNotify::eqNotifyTriggerTermEquality.
 134    */
 135   bool propagateLit(TNode lit);
 136   /**
 137    * Return an explanation for the literal represented by parameter lit
 138    * (which was previously propagated by this theory). By default, this
 139    * returns the explanation given by the official equality engine of the
 140    * Theory, if it exists.
 141    */
 142   virtual TrustNode explainLit(TNode lit);
 143   //--------------------------------------- conflicts
 144   /**
 145    * Raise conflict, called when constants a and b merge. Sends the conflict
 146    * on the output channel corresponding to the equality engine's explanation
 147    * of (= a b). The proof equality engine (if it exists) will be used as the
 148    * proof generator.
 149    *
 150    * Note that this is the preferred method to call on
 151    * EqualityEngineNotify::eqNotifyConstantTermMerge.
 152    */
 153   void conflictEqConstantMerge(TNode a, TNode b);
 154   /**
 155    * Raise conflict conf (of any form), without proofs. This method should
 156    * only be called if there is not yet proof support in the given theory.
 157    */
 158   void conflict(TNode conf, InferenceId id);
 159   /**
 160    * Raise trusted conflict tconf (of any form) where a proof generator has
 161    * been provided (as part of the trust node) in a custom way.
 162    */
 163   void trustedConflict(TrustNode tconf, InferenceId id);
 164   /**
 165    * Explain and send conflict from contradictory facts. This method is called
 166    * when the proof rule id with premises exp and arguments args concludes
 167    * false. This method sends a trusted conflict corresponding to the official
 168    * equality engine's explanation of literals in exp, with the proof equality
 169    * engine as the proof generator (if it exists).
 170    */
 171   void conflictExp(InferenceId id,
 172                    PfRule pfr,
 173                    const std::vector<Node>& exp,
 174                    const std::vector<Node>& args);
 175   /**
 176    * Make the trust node corresponding to the conflict of the above form. It is
 177    * the responsibility of the caller to subsequently call trustedConflict with
 178    * the returned trust node.
 179    */
 180   TrustNode mkConflictExp(PfRule pfr,
 181                           const std::vector<Node>& exp,
 182                           const std::vector<Node>& args);
 183   /**
 184    * Explain and send conflict from contradictory facts. This method is called
 185    * when proof generator pg has a proof of false from free assumptions exp.
 186    * This method sends a trusted conflict corresponding to the official
 187    * equality engine's explanation of literals in exp, with the proof equality
 188    * engine as the proof generator (if it exists), where pg provides the
 189    * final step(s) of this proof during this call.
 190    */
 191   void conflictExp(InferenceId id,
 192                    const std::vector<Node>& exp,
 193                    ProofGenerator* pg);
 194   /**
 195    * Make the trust node corresponding to the conflict of the above form. It is
 196    * the responsibility of the caller to subsequently call trustedConflict with
 197    * the returned trust node.
 198    */
 199   TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
 200   //--------------------------------------- lemmas
 201   /**
 202    * Send (trusted) lemma lem with property p on the output channel.
 203    *
 204    * @param tlem The trust node containing the lemma and its proof generator.
 205    * @param p The property of the lemma
 206    * @return true if the lemma was sent on the output channel.
 207    */
 208   bool trustedLemma(const TrustNode& tlem,
 209                     InferenceId id,
 210                     LemmaProperty p = LemmaProperty::NONE);
 211   /**
 212    * Send lemma lem with property p on the output channel. Same as above, with
 213    * a node instead of a trust node.
 214    */
 215   bool lemma(TNode lem, InferenceId id, LemmaProperty p = LemmaProperty::NONE);
 216   /**
 217    * Explained lemma. This should be called when
 218    *   ( exp => conc )
 219    * is a valid theory lemma. This method adds a lemma where part of exp
 220    * is replaced by its explanation according to the official equality engine
 221    * of the theory.
 222    *
 223    * In particular, this method adds a lemma on the output channel of the form
 224    *   ( ^_{e in exp \ noExplain} EXPLAIN(e) ^ noExplain ) => conc
 225    * where EXPLAIN(e) returns the explanation of literal e according to the
 226    * official equality engine of the theory. Note that noExplain is the *subset*
 227    * of exp that should not be explained.
 228    *
 229    * @param conc The conclusion of the lemma
 230    * @param id The proof rule concluding conc
 231    * @param exp The set of (all) literals that imply conc
 232    * @param noExplain The subset of exp that should not be explained by the
 233    * equality engine
 234    * @param args The arguments to the proof step concluding conc
 235    * @param p The property of the lemma
 236    * @return true if the lemma was sent on the output channel.
 237    */
 238   bool lemmaExp(Node conc,
 239                 InferenceId id,
 240                 PfRule pfr,
 241                 const std::vector<Node>& exp,
 242                 const std::vector<Node>& noExplain,
 243                 const std::vector<Node>& args,
 244                 LemmaProperty p = LemmaProperty::NONE);
 245   /**
 246    * Make the trust node for the above method. It is responsibility of the
 247    * caller to subsequently call trustedLemma with the returned trust node.
 248    */
 249   TrustNode mkLemmaExp(Node conc,
 250                        PfRule id,
 251                        const std::vector<Node>& exp,
 252                        const std::vector<Node>& noExplain,
 253                        const std::vector<Node>& args);
 254   /**
 255    * Same as above, but where pg can provide a proof of conc from free
 256    * assumptions in exp. This sends a trusted lemma on the output channel where
 257    * the proof equality engine is the proof generator. The generator pg
 258    * is asked to provide the final step(s) of this proof during this call.
 259    *
 260    * @param conc The conclusion of the lemma
 261    * @param exp The set of (all) literals that imply conc
 262    * @param noExplain The subset of exp that should not be explained by the
 263    * equality engine
 264    * @param pg If non-null, the proof generator who can provide a proof of conc.
 265    * @param p The property of the lemma
 266    * @return true if the lemma was sent on the output channel.
 267    */
 268   bool lemmaExp(Node conc,
 269                 InferenceId id,
 270                 const std::vector<Node>& exp,
 271                 const std::vector<Node>& noExplain,
 272                 ProofGenerator* pg = nullptr,
 273                 LemmaProperty p = LemmaProperty::NONE);
 274   /**
 275    * Make the trust node for the above method. It is responsibility of the
 276    * caller to subsequently call trustedLemma with the returned trust node.
 277    */
 278   TrustNode mkLemmaExp(Node conc,
 279                        const std::vector<Node>& exp,
 280                        const std::vector<Node>& noExplain,
 281                        ProofGenerator* pg = nullptr);
 282   /**
 283    * Has this inference manager cached and sent the given lemma (in this user
 284    * context)? This method can be overridden by the particular manager. If not,
 285    * this returns true if lem is in the cache d_lemmasSent maintained by this
 286    * class. Notice that the default cache in this base class is not dependent
 287    * on the lemma property.
 288    */
 289   virtual bool hasCachedLemma(TNode lem, LemmaProperty p);
 290   /** The number of lemmas we have sent since the last call to reset */
 291   uint32_t numSentLemmas() const;
 292   /** Have we added a lemma since the last call to reset? */
 293   bool hasSentLemma() const;
 294   //--------------------------------------- internal facts
 295   /**
 296    * Assert internal fact. This is recommended method for asserting "internal"
 297    * facts into the equality engine of the theory. In particular, this method
 298    * should be used for anything the theory infers that is not sent on the
 299    * output channel as a propagation or lemma. This method ensures that the
 300    * Theory's preNotifyFact and notifyFact method have been called with
 301    * isInternal = true.
 302    *
 303    * @param atom The atom of the fact to assert
 304    * @param pol Its polarity
 305    * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid.
 306    * @return true if the fact was processed, i.e. it was asserted to the
 307    * equality engine or preNotifyFact returned true.
 308    */
 309   bool assertInternalFact(TNode atom, bool pol, InferenceId id, TNode exp);
 310   /**
 311    * Assert internal fact, with a proof step justification. Notice that if
 312    * proofs are not enabled in this inference manager, then this asserts
 313    * a fact to the equality engine in the normal way.
 314    *
 315    * @param atom The atom of the fact to assert
 316    * @param pol Its polarity
 317    * @param id The proof rule identifier of the proof step
 318    * @param exp Its explanation, interpreted as a conjunction
 319    * @param args The arguments of the proof step
 320    * @return true if the fact was processed, i.e. it was asserted to the
 321    * equality engine or preNotifyFact returned true.
 322    */
 323   bool assertInternalFact(TNode atom,
 324                           bool pol,
 325                           InferenceId id,
 326                           PfRule pfr,
 327                           const std::vector<Node>& exp,
 328                           const std::vector<Node>& args);
 329   /**
 330    * Assert internal fact, with a proof generator justification. Same as above,
 331    * but with a proof generator instead of an explicit step.
 332    *
 333    * @param atom The atom of the fact to assert
 334    * @param pol Its polarity
 335    * @param exp Its explanation, interpreted as a conjunction
 336    * @param pg The proof generator for this step. If non-null, pg must be able
 337    * to provide a proof concluding (~) atom from free asumptions in exp in
 338    * the remainder of the current SAT context.
 339    * @return true if the fact was processed, i.e. it was asserted to the
 340    * equality engine or preNotifyFact returned true.
 341    */
 342   bool assertInternalFact(TNode atom,
 343                           bool pol,
 344                           InferenceId id,
 345                           const std::vector<Node>& exp,
 346                           ProofGenerator* pg);
 347   /** The number of internal facts we have added since the last call to reset */
 348   uint32_t numSentFacts() const;
 349   /** Have we added a internal fact since the last call to reset? */
 350   bool hasSentFact() const;
 351   //--------------------------------------- phase requirements
 352   /** Get the decision manager, which manages decision strategies. */
 353   DecisionManager* getDecisionManager();
 354   /**
 355    * Set that literal n has SAT phase requirement pol, that is, it should be
 356    * decided with polarity pol, for details see OutputChannel::requirePhase.
 357    */
 358   void requirePhase(TNode n, bool pol);
 359
 360   /**
 361    * Forward to OutputChannel::spendResource() to spend resources.
 362    */
 363   void spendResource(Resource r);
 364
 365   /**
 366    * Forward to OutputChannel::safePoint() to spend resources.
 367    */
 368   void safePoint(Resource r);
 369   /**
 370    * Notification from a theory that it realizes it is incomplete at
 371    * this context level.
 372    */
 373   void setIncomplete(IncompleteId id);
 374
 375  protected:
 376   /**
 377    * Process internal fact. This is a common helper method for the
 378    * assertInternalFact variants above. Returns true if the fact was processed.
 379    */
 380   bool processInternalFact(TNode atom,
 381                            bool pol,
 382                            InferenceId iid,
 383                            PfRule id,
 384                            const std::vector<Node>& exp,
 385                            const std::vector<Node>& args,
 386                            ProofGenerator* pg);
 387   /**
 388    * Explain conflict from constants merging in the equality engine. This
 389    * method is called by conflictEqConstantMerge. By default, it returns
 390    * the explanation of the official equality engine of the theory, if it
 391    * exists.
 392    */
 393   virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
 394   /**
 395    * Explain formula n (which is possibly a conjunction with no nested
 396    * conjunctions), add its explanation to assumptions.
 397    */
 398   void explain(TNode n, std::vector<TNode>& assumptions);
 399   /**
 400    * Explain formula n (which is possibly a conjunction with no nested
 401    * conjunctions), return the explanation as a conjunction.
 402    */
 403   Node mkExplain(TNode n);
 404   /**
 405    * Explain the set of formulas in exp using the official equality engine of
 406    * the theory. We ask the equality engine to explain literals in exp
 407    * that do not occur in noExplain, and return unchanged those that occur in
 408    * noExplain. Note the vector noExplain should be a subset of exp.
 409    */
 410   Node mkExplainPartial(const std::vector<Node>& exp,
 411                         const std::vector<Node>& noExplain);
 412   /**
 413    * Cache that lemma lem is being sent with property p. Return true if it
 414    * did not already exist in the cache maintained by this class. If this
 415    * method is not overridden, then we use the d_lemmasSent cache maintained
 416    * by this class, which notice is not dependent on lemma property. If
 417    * the lemma property should be taken into account, the manager should
 418    * override this method to take the lemma property into account as needed.
 419    */
 420   virtual bool cacheLemma(TNode lem, LemmaProperty p);
 421   /** The theory object */
 422   Theory& d_theory;
 423   /** Reference to the state of theory */
 424   TheoryState& d_theoryState;
 425   /** Reference to the output channel of the theory */
 426   OutputChannel& d_out;
 427   /** Pointer to equality engine of the theory. */
 428   eq::EqualityEngine* d_ee;
 429   /** Pointer to the decision manager */
 430   DecisionManager* d_decManager;
 431   /** A proof equality engine */
 432   std::unique_ptr<eq::ProofEqEngine> d_pfee;
 433   /** The proof node manager of the theory */
 434   ProofNodeManager* d_pnm;
 435   /** Whether this manager caches lemmas */
 436   bool d_cacheLemmas;
 437   /**
 438    * The keep set of this class. This set is maintained to ensure that
 439    * facts and their explanations are ref-counted. Since facts and their
 440    * explanations are SAT-context-dependent, this set is also
 441    * SAT-context-dependent.
 442    */
 443   NodeSet d_keep;
 444   /**
 445    * A cache of all lemmas sent, which is a user-context-dependent set of
 446    * nodes. Notice that this cache does not depedent on lemma property.
 447    */
 448   NodeSet d_lemmasSent;
 449   /** The number of conflicts sent since the last call to reset. */
 450   uint32_t d_numConflicts;
 451   /** The number of lemmas sent since the last call to reset. */
 452   uint32_t d_numCurrentLemmas;
 453   /** The number of internal facts added since the last call to reset. */
 454   uint32_t d_numCurrentFacts;
 455   /** Statistics for conflicts sent via this inference manager. */
 456   HistogramStat<InferenceId> d_conflictIdStats;
 457   /** Statistics for facts sent via this inference manager. */
 458   HistogramStat<InferenceId> d_factIdStats;
 459   /** Statistics for lemmas sent via this inference manager. */
 460   HistogramStat<InferenceId> d_lemmaIdStats;
 461 };
 462
 463 }  // namespace theory
 464 }  // namespace cvc5
 465
 466 #endif /* CVC5__THEORY__THEORY_INFERENCE_MANAGER_H */