From c5e4a56d4895ce29cd37bac027bb3d486d687f9d Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 30 Apr 2014 17:28:00 -0400
Subject: T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
---
 src/theory/theory.h | 80 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

(limited to 'src/theory/theory.h')

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 */
 
-- 
cgit v1.2.3