1 files changed, 80 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c86aa17de..972abe3d8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -52,6 +52,9 @@ class QuantifiersEngine;
 class TheoryModel;
 class SubstitutionMap;
 
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
+
 namespace rrinst {
   class CandidateGenerator;
 }/* CVC4::theory::rrinst namespace */
@@ -808,6 +811,63 @@ public:
    * in a queriable form.  As this is
    */
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+
+  /**
+   * This allows the theory to be queried for whether a literal, lit, is
+   * entailed by the theory.  This returns a pair of a Boolean and a node E.
+   *
+   * If the Boolean is true, then E is a formula that entails lit and E is propositionally
+   * entailed by the assertions to the theory.
+   *
+   * If the Boolean is false, it is "unknown" if lit is entailed and E may be
+   * any node.
+   *
+   * The literal lit is either an atom a or (not a), which must belong to the theory:
+   *   There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
+   *
+   * There are NO assumptions that a or the subterms of a have been
+   * preprocessed in any form.  This includes ppRewrite, rewriting,
+   * preregistering, registering, definition expansion or ITE removal!
+   *
+   * Theories are free to limit the amount of effort they use and so may
+   * always opt to return "unknown".  Both "unknown" and "not entailed",
+   * may return for E a non-boolean Node (e.g. Node::null()).  (There is no explicit output
+   * for the negation of lit is entailed.)
+   *
+   * If lit is theory valid, the return result may be the Boolean constant
+   * true for E.
+   *
+   * If lit is entailed by multiple assertions on the theory's getFact()
+   * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
+   * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
+   *
+   * If lit is entailed by a single assertion on the theory's getFact()
+   * queue, say a, this may return E=a.
+   *
+   * The theory may always return false!
+   *
+   * The search is controlled by the parameter params.  For default behavior,
+   * this may be left NULL.
+   *
+   * Theories that want parameters extend the virtual EntailmentCheckParameters
+   * class.  Users ask the theory for an appropriate subclass from the theory
+   * and configure that.  How this is implemented is on a per theory basis.
+   *
+   * The search may provide additional output to guide the user of
+   * this function.  This output is stored in a EntailmentCheckSideEffects*
+   * output parameter.  The implementation of this is theory specific.  For
+   * no output, this is NULL.
+   *
+   * Theories may not touch their output stream during an entailment check.
+   *
+   * @param  lit     a literal belonging to the theory.
+   * @param  params  the control parameters for the entailment check.
+   * @param  out     a theory specific output object of the entailment search.
+   * @return         a pair <b,E> s.t. if b is true, then a formula E such that
+   * E |= lit in the theory.
+   */
+  virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
@@ -852,6 +912,26 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+class EntailmentCheckParameters {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckParameters(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckParameters();
+};/* class EntailmentCheckParameters */
+
+class EntailmentCheckSideEffects {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckSideEffects(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckSideEffects();
+};/* class EntailmentCheckSideEffects */
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */