Added Theory::presolve().

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index eb4c18161..f27e61544 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -617,4 +617,20 @@ Node TheoryEngine::getValue(TNode node) {
   return theoryOf(node)->getValue(node, this);
 }/* TheoryEngine::getValue(TNode node) */
 
+
+bool TheoryEngine::presolve(){
+  d_theoryOut.d_conflictNode = Node::null();
+  d_theoryOut.d_propagatedLiterals.clear();
+  try {
+    //d_uf->presolve();
+    d_arith->presolve();
+    //d_arrays->presolve();
+    //d_bv->presolve();
+  } catch(const theory::Interrupted&) {
+    Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl;
+  }
+  // Return wheather we have a conflict
+  return d_theoryOut.d_conflictNode.get().isNull();
+}
+
 }/* CVC4 namespace */