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>

1 files changed, 9 insertions, 0 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9a987c9d7..8bc67616f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,9 @@ namespace theory {
   namespace eq {
     class EqualityEngine;
   }
+
+  class EntailmentCheckParameters;
+  class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 class DecisionEngine;
 class RemoveITE;
@@ -755,6 +758,12 @@ public:
    */
   Node getModelValue(TNode var);
 
+  /**
+   * Forwards an entailmentCheck according to the given theoryOfMode mode.
+   * See theory.h for documentation on entailmentCheck().
+   */
+  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+
 private:
 
   /** Default visitor for pre-registration */