Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 18 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 94281156f..a14534efe 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1123,6 +1123,15 @@ Node TheoryEngine::preprocess(TNode assertion) {
   return d_ppCache[assertion];
 }
 
+void TheoryEngine::notifyPreprocessedAssertions( std::vector< Node >& assertions ){
+  // call all the theories
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
+    if(d_theoryTable[theoryId]) {
+      theoryOf(theoryId)->ppNotifyAssertions( assertions );
+    }
+  }
+}
+
 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 
   // What and where we are asserting
@@ -1444,6 +1453,15 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins
   }
 }
 
+Node TheoryEngine::getInstantiatedConjunction( Node q ) {
+  if( d_quantEngine ){
+    return d_quantEngine->getInstantiatedConjunction( q );
+  }else{
+    Assert( false );
+    return Node::null();
+  }
+}
+
 
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {