Add the theory inference manager (#4948)

This class is a wrapper around OutputChannel and EqualityEngine. It is preferred that the Theory use this interface when asserting "internal facts" to the equality engine, and for sending lemmas, conflicts and propagations on the output channel.

This class will be useful when trying new methods for theory combination, where all theories behavior can be modified in a standard way based on modifications to the base inference manager class.

1 files changed, 148 insertions, 0 deletions

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
new file mode 100644
index 000000000..914c87d19
--- /dev/null
+++ b/src/theory/theory_inference_manager.h
@@ -0,0 +1,148 @@
+/*********************                                                        */
+/*! \file theory_inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief An inference manager for Theory
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+#define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H
+
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/theory_state.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace theory {
+
+class Theory;
+namespace eq {
+class EqualityEngine;
+}
+
+/**
+ * The base class for inference manager. An inference manager is a wrapper
+ * around the output channel and the official equality engine of a Theory.
+ * It is used for ensuring that the equality engine and output channel
+ * are used properly. This includes the following invariants:
+ *
+ * (1) The state tracks conflicts.
+ * In particular, TheoryState::isInConflict returns true whenever we have
+ * called OutputChannel::conflict in the current context, which we enforce
+ * by always setting d_state.notifyInConflict at the same time we send
+ * conflicts on the output channel.
+ *
+ * (2) The theory is notified of (internal) facts.
+ * In particular, Theory::preNotifyFact and Theory::notifyFact are called
+ * (with isInternal = true) whenever we assert internal facts using
+ * assertFactInernal below, mirroring what is done for facts from the fact
+ * queue (where isInternal = false).
+ */
+class TheoryInferenceManager
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  /**
+   * Constructor, note that state should be the official state of theory t.
+   */
+  TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
+  virtual ~TheoryInferenceManager() {}
+  //--------------------------------------- initialization
+  /**
+   * Set equality engine, ee is a pointer to the official equality engine
+   * of theory.
+   */
+  void setEqualityEngine(eq::EqualityEngine* ee);
+  //--------------------------------------- end initialization
+  /**
+   * T-propagate literal lit, possibly encountered by equality engine,
+   * returns false if we are in conflict.
+   *
+   * Note that this is the preferred method to call on
+   * EqualityEngineNotify::eqNotifyTriggerPredicate and
+   * EqualityEngineNotify::eqNotifyTriggerTermEquality.
+   */
+  bool propagateLit(TNode lit);
+  /**
+   * Return an explanation for the literal represented by parameter lit
+   * (which was previously propagated by this theory). By default, this
+   * returns the explanation given by the official equality engine of the
+   * Theory, if it exists.
+   */
+  virtual TrustNode explainLit(TNode lit);
+  /**
+   * Raise conflict, called when constants a and b merge. Sends the conflict
+   * on the output channel corresponding to the equality engine's explanation
+   * of (= a b). The proof equality engine (if it exists) will be used as the
+   * proof generator.
+   *
+   * Note that this is the preferred method to call on
+   * EqualityEngineNotify::eqNotifyConstantTermMerge.
+   */
+  void conflictEqConstantMerge(TNode a, TNode b);
+  /**
+   * Raise conflict conf (of any form), without proofs. This method should
+   * only be called if there is not yet proof support in the given theory.
+   */
+  void conflict(TNode conf);
+  /**
+   * Raise trusted conflict tconf (of any form) where a proof generator has
+   * been provided in a custom way.
+   */
+  void trustedConflict(TrustNode tconf);
+  /**
+   * Assert internal fact. This is recommended method for asserting "internal"
+   * facts into the equality engine of the theory. In particular, this method
+   * should be used for anything the theory infers that is not sent on the
+   * output channel as a propagation or lemma. This method ensures that the
+   * Theory's preNotifyFact and notifyFact method have been called with
+   * isInternal = true.
+   */
+  void assertInternalFact(TNode atom, bool pol, TNode fact);
+
+ protected:
+  /**
+   * Explain conflict from constants merging in the equality engine. This
+   * method is called by conflictEqConstantMerge. By default, it returns
+   * the explanation of the official equality engine of the theory, if it
+   * exists.
+   */
+  virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b);
+  /** The theory object */
+  Theory& d_theory;
+  /** Reference to the state of theory */
+  TheoryState& d_theoryState;
+  /** Reference to the output channel of the theory */
+  OutputChannel& d_out;
+  /** Pointer to equality engine of the theory. */
+  eq::EqualityEngine* d_ee;
+  /** The proof node manager of the theory */
+  ProofNodeManager* d_pnm;
+  /**
+   * The keep set of this class. This set is maintained to ensure that
+   * facts and their explanations are ref-counted. Since facts and their
+   * explanations are SAT-context-dependent, this set is also
+   * SAT-context-dependent.
+   */
+  NodeSet d_keep;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__THEORY_INFERENCE_MANAGER_H */