Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and contract is the same as for TheoryEngine version.

3 files changed, 51 insertions, 38 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8bc67616f..0495a866b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -73,8 +73,7 @@ struct NodeTheoryPairHashFunction {
 };/* struct NodeTheoryPairHashFunction */
 
 
-
-/* Forward Declarations Block */
+/* Forward declarations */
 namespace theory {
   class TheoryModel;
   class TheoryEngineModelBuilder;
@@ -82,11 +81,12 @@ namespace theory {
 
   namespace eq {
     class EqualityEngine;
-  }
+  }/* CVC4::theory::eq namespace */
 
   class EntailmentCheckParameters;
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
+
 class DecisionEngine;
 class RemoveITE;
 class UnconstrainedSimplifier;
@@ -759,7 +759,7 @@ public:
   Node getModelValue(TNode var);
 
   /**
-   * Forwards an entailmentCheck according to the given theoryOfMode mode.
+   * Forwards an entailment check according to the given theoryOfMode.
    * 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);
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index d4aef4fff..72d878782 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -23,34 +23,34 @@ namespace CVC4 {
 namespace theory {
 
 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
- switch (s1) {
- case EQUALITY_TRUE:
- case EQUALITY_TRUE_IN_MODEL:
- case EQUALITY_TRUE_AND_PROPAGATED:
-   switch (s2) {
-   case EQUALITY_TRUE:
-   case EQUALITY_TRUE_IN_MODEL:
-   case EQUALITY_TRUE_AND_PROPAGATED:
-     return true;
-   default:
-     return false;
-   }
-   break;
- case EQUALITY_FALSE:
- case EQUALITY_FALSE_IN_MODEL:
- case EQUALITY_FALSE_AND_PROPAGATED:
-   switch (s2) {
-   case EQUALITY_FALSE:
-   case EQUALITY_FALSE_IN_MODEL:
-   case EQUALITY_FALSE_AND_PROPAGATED:
-     return true;
-   default:
-     return false;
-   }
-   break;
- default:
-   return false;
- }
+  switch (s1) {
+  case EQUALITY_TRUE:
+  case EQUALITY_TRUE_IN_MODEL:
+  case EQUALITY_TRUE_AND_PROPAGATED:
+    switch (s2) {
+    case EQUALITY_TRUE:
+    case EQUALITY_TRUE_IN_MODEL:
+    case EQUALITY_TRUE_AND_PROPAGATED:
+      return true;
+    default:
+      return false;
+    }
+    break;
+  case EQUALITY_FALSE:
+  case EQUALITY_FALSE_IN_MODEL:
+  case EQUALITY_FALSE_AND_PROPAGATED:
+    switch (s2) {
+    case EQUALITY_FALSE:
+    case EQUALITY_FALSE_IN_MODEL:
+    case EQUALITY_FALSE_AND_PROPAGATED:
+      return true;
+    default:
+      return false;
+    }
+    break;
+  default:
+    return false;
+  }
 }
 
 bool Valuation::isSatLiteral(TNode n) const {
@@ -87,7 +87,6 @@ Node Valuation::getModelValue(TNode var) {
   return d_engine->getModelValue(var);
 }
 
-
 Node Valuation::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
@@ -106,5 +105,9 @@ unsigned Valuation::getAssertionLevel() const{
   return d_engine->getPropEngine()->getAssertionLevel();
 }
 
+std::pair<bool, Node> Valuation::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params, theory::EntailmentCheckSideEffects* out) {
+  return d_engine->entailmentCheck(mode, lit, params, out);
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index d175e5e3d..2462896c7 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -5,7 +5,7 @@
  ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): Tim King, Andrew Reynolds, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -22,6 +22,7 @@
 #define __CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
+#include "theory/theoryof_mode.h"
 
 namespace CVC4 {
 
@@ -29,6 +30,9 @@ class TheoryEngine;
 
 namespace theory {
 
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
+
 /**
  * The status of an equality in the current context.
  */
@@ -47,11 +51,11 @@ enum EqualityStatus {
   EQUALITY_FALSE_IN_MODEL,
   /** The equality is completely unknown */
   EQUALITY_UNKNOWN
-};
+};/* enum EqualityStatus */
 
 /**
- * Returns true if the two statuses are compatible, i.e. bot TRUE
- * or both FALSE (regardles of inmodel/propagation).
+ * Returns true if the two statuses are compatible, i.e. both TRUE
+ * or both FALSE (regardless of inmodel/propagation).
  */
 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
 
@@ -125,6 +129,12 @@ public:
    */
   unsigned getAssertionLevel() const;
 
+  /**
+   * Request an entailment check according to the given theoryOfMode.
+   * 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);
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */