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

Conflicts:
	src/options/quantifiers_options

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 2c58b8f77..ec1b41a98 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
@@ -204,6 +205,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
       Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
     }
   }
+  d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
   Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
   return addedLemmas;
 }
@@ -294,6 +296,11 @@ void RewriteEngine::assertNode( Node n ) {
 
 }
 
+bool RewriteEngine::checkCompleteFor( Node q ) { 
+  // by semantics of rewrite rules, saturation -> SAT 
+  return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
+}
+
 Node RewriteEngine::getInstConstNode( Node n, Node q ) {
   std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
   if( it==d_inst_const_node[q].end() ){