From d0ec84da973d3ba7054b61fd620a1eba0d459a48 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 18 Jul 2013 13:08:56 -0500
Subject: Fix quantifier instantiation bug in cbqi, add default priorities in
 rewrite engine.

---
 src/theory/quantifiers/rewrite_engine.cpp | 60 +++++++++++++++++++++++++++++--
 1 file changed, 57 insertions(+), 3 deletions(-)

(limited to 'src/theory/quantifiers/rewrite_engine.cpp')

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index aa0569ef4..e278de9e1 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/inst_match_generator.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace std;
@@ -25,20 +26,67 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
+struct PrioritySort {
+  std::vector< double > d_priority;
+  bool operator() (int i,int j) {
+    return d_priority[i] < d_priority[j];
+  }
+};
+
+
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
 
 }
 
+double RewriteEngine::getPriority( Node f ) {
+  Node rr = f.getAttribute(QRewriteRuleAttribute());
+  Node rrr = rr[2];
+  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;
+  bool deterministic = rrr[1].getKind()!=OR;
+  if( rrr.getKind()==RR_REWRITE ){
+    return deterministic ? 0.0 : 3.0;
+  }else if( rrr.getKind()==RR_DEDUCTION ){
+    return deterministic ? 1.0 : 4.0;
+  }else if( rrr.getKind()==RR_REDUCTION ){
+    return deterministic ? 2.0 : 5.0;
+  }else{
+    return 6.0;
+  }
+}
+
 void RewriteEngine::check( Theory::Effort e ) {
   if( e==Theory::EFFORT_LAST_CALL ){
+    if( !d_quantEngine->getModel()->isModelSet() ){
+      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
+    }
     if( d_true.isNull() ){
       d_true = NodeManager::currentNM()->mkConst( true );
     }
+    std::vector< Node > priority_order;
+    PrioritySort ps;
+    std::vector< int > indicies;
+    for( int i=0; i<(int)d_rr_quant.size(); i++ ){
+      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );
+      indicies.push_back( i );
+    }
+    std::sort( indicies.begin(), indicies.end(), ps );
+    for( unsigned i=0; i<indicies.size(); i++ ){
+      priority_order.push_back( d_rr_quant[indicies[i]] );
+    }
+
     //apply rewrite rules
     int addedLemmas = 0;
-    for( unsigned i=0; i<d_rr_quant.size(); i++ ) {
-      addedLemmas += checkRewriteRule( d_rr_quant[i] );
+    //per priority level
+    int index = 0;
+    bool success = true;
+    while( success && index<(int)priority_order.size() ) {
+      addedLemmas += checkRewriteRule( priority_order[index] );
+      index++;
+      if( index<(int)priority_order.size() ){
+        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );
+      }
     }
+
     Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
     if (addedLemmas==0) {
     }else{
@@ -49,7 +97,7 @@ void RewriteEngine::check( Theory::Effort e ) {
 }
 
 int RewriteEngine::checkRewriteRule( Node f ) {
-  Trace("rewrite-engine-inst") << "Check " << f << "..." << std::endl;
+  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;
   int addedLemmas = 0;
   //reset triggers
   Node rr = f.getAttribute(QRewriteRuleAttribute());
@@ -102,6 +150,12 @@ int RewriteEngine::checkRewriteRule( Node f ) {
           if( d_quantEngine->addInstantiation( f, m ) ){
             addedLemmas++;
             Trace("rewrite-engine-inst-debug") << "success" << std::endl;
+            //set the no-match attribute (the term is rewritten and can be ignored)
+            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;
+            //if( !m.d_matched.isNull() ){
+            //  NoMatchAttribute nma;
+            //  m.d_matched.setAttribute(nma,true);
+            //}
           }else{
             Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
           }
-- 
cgit v1.2.3