Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.

Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.

QCF is now functional backend to rewrite rules. Support boolean variables in QCF.  Change check-model to ignore rewrite rules.  Incorporate some fixes from master.

Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.

Minor fixes to QCF/rewrite engine, removes RE on last call approach.  Add option for one inst per round in RE.

Merging rewrite rules into master, check-model current fails on 3 FMF regressions.

Fix check-model issue, a line of code was omitted during merge.

1 files changed, 209 insertions, 91 deletions

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 81de1e11d..59ba40ca7 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace CVC4;
 using namespace std;
@@ -37,14 +38,15 @@ struct PrioritySort {
 
 
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
-
+  d_true = NodeManager::currentNM()->mkConst( true );
 }
 
 double RewriteEngine::getPriority( Node f ) {
-  Node rr = f.getAttribute(QRewriteRuleAttribute());
+  Node rr = TermDb::getRewriteRule( f );
   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 ){
@@ -54,26 +56,31 @@ double RewriteEngine::getPriority( Node f ) {
   }else{
     return 6.0;
   }
+
+  //return deterministic ? 0.0 : 1.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]] );
+  if( e==Theory::EFFORT_FULL ){
+    Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
+    //if( e==Theory::EFFORT_LAST_CALL ){
+    //  if( !d_quantEngine->getModel()->isModelSet() ){
+    //    d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );
+    //  }
+    //}
+    if( d_needsSort ){
+      d_priority_order.clear();
+      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++ ){
+        d_priority_order.push_back( d_rr_quant[indicies[i]] );
+      }
+      d_needsSort = false;
     }
 
     //apply rewrite rules
@@ -81,16 +88,17 @@ void RewriteEngine::check( Theory::Effort e ) {
     //per priority level
     int index = 0;
     bool success = true;
-    while( success && index<(int)priority_order.size() ) {
-      addedLemmas += checkRewriteRule( priority_order[index] );
+    while( success && index<(int)d_priority_order.size() ) {
+      addedLemmas += checkRewriteRule( d_priority_order[index], e );
       index++;
-      if( index<(int)priority_order.size() ){
-        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );
+      if( index<(int)d_priority_order.size() ){
+        success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] );
       }
     }
 
-    Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
+    Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
     if (addedLemmas==0) {
+
     }else{
       //otherwise, the search will continue
       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -98,85 +106,185 @@ void RewriteEngine::check( Theory::Effort e ) {
   }
 }
 
-int RewriteEngine::checkRewriteRule( Node f ) {
-  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;
+int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
   int addedLemmas = 0;
-  //reset triggers
-  Node rr = f.getAttribute(QRewriteRuleAttribute());
-  if( d_rr_triggers.find(f)==d_rr_triggers.end() ){
-    std::vector< inst::Trigger * > triggers;
-    if( f.getNumChildren()==3 ){
-      for(unsigned i=0; i<f[2].getNumChildren(); i++ ){
-        Node pat = f[2][i];
-        std::vector< Node > nodes;
-        Trace("rewrite-engine-trigger") << "Trigger is : ";
-        for( int j=0; j<(int)pat.getNumChildren(); j++ ){
-          Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );
-          nodes.push_back( p );
-          Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";
-        }
-        Trace("rewrite-engine-trigger") << std::endl;
-        Assert( inst::Trigger::isUsableTrigger( nodes, f ) );
-        inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );
-        tr->getGenerator()->setActiveAdd(false);
-        triggers.push_back( tr );
-      }
-    }
-    d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );
-  }
-  for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){
-    Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;
-    d_rr_triggers[f][i]->resetInstantiationRound();
-    d_rr_triggers[f][i]->reset( Node::null() );
-    bool success;
-    do
-    {
-      InstMatch m( f );
-      success = d_rr_triggers[f][i]->getNextMatch( f, m );
-      if( success ){
-        //see if instantiation is true in the model
-        Node rr = f.getAttribute(QRewriteRuleAttribute());
-        Node rrg = rr[1];
-        std::vector< Node > vars;
-        std::vector< Node > terms;
-        d_quantEngine->computeTermVector( f, m, vars, terms );
-        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;
-        Node inst = d_rr_guard[f];
-        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;
-        FirstOrderModel * fm = d_quantEngine->getModel();
-        Node v = fm->getValue( inst );
-        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;
-        if( v==d_true ){
-          Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
-          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);
+  Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl;
+  QuantConflictFind * qcf = d_quantEngine->getConflictFind();
+  if( qcf ){
+    //reset QCF module
+    qcf->computeRelevantEqr();
+    qcf->setEffort( QuantConflictFind::effort_conflict );
+    //get the proper quantifiers info
+    std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f );
+    if( it!=d_qinfo.end() ){
+      QuantInfo * qi = &it->second;
+      if( qi->d_mg->isValid() ){
+        Node rr = TermDb::getRewriteRule( f );
+        Trace("rewrite-engine-inst-debug") << "   Reset round..." << std::endl;
+        qi->reset_round( qcf );
+        Trace("rewrite-engine-inst-debug") << "   Get matches..." << std::endl;
+        while( qi->d_mg->getNextMatch( qcf, qi ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+          Trace("rewrite-engine-inst-debug") << "   Got match to complete..." << std::endl;
+          qi->debugPrintMatch( "rewrite-engine-inst-debug" );
+          std::vector< int > assigned;
+          if( !qi->isMatchSpurious( qcf ) ){
+            bool doContinue = false;
+            bool success = true;
+            int tempAddedLemmas = 0;
+            while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+              success = qi->completeMatch( qcf, assigned, doContinue );
+              doContinue = true;
+              if( success ){
+                Trace("rewrite-engine-inst-debug") << "   Construct match..." << std::endl;
+                std::vector< Node > inst;
+                qi->getMatch( inst );
+                Trace("rewrite-engine-inst-debug") << "   Add instantiation..." << std::endl;
+                for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+                  Trace("rewrite-engine-inst-debug") << "  " << f[0][i] << " -> ";
+                  if( i<inst.size() ){
+                    Trace("rewrite-engine-inst-debug") << inst[i] << std::endl;
+                  }else{
+                    Trace("rewrite-engine-inst-debug") << "OUT_OF_RANGE" << std::endl;
+                    Assert( false );
+                  }
+                }
+                //resize to remove auxiliary variables
+                if( inst.size()>f[0].getNumChildren() ){
+                  inst.resize( f[0].getNumChildren() );
+                }
+                if( d_quantEngine->addInstantiation( f, inst ) ){
+                  addedLemmas++;
+                  tempAddedLemmas++;
+                  /*
+                  //remove rewritten terms from consideration
+                  std::vector< Node > to_remove;
+                  switch( rr[2].getKind() ){
+                  case kind::RR_REWRITE:
+                    to_remove.push_back( rr[2][0] );
+                    break;
+                  case kind::RR_REDUCTION:
+                    for( unsigned i=0; i<rr[2][0].getNumChildren(); i++ ){
+                      to_remove.push_back( rr[2][0][i] );
+                    }
+                    break;
+                  default:
+                    break;
+                  }
+                  for( unsigned j=0; j<to_remove.size(); j++ ){
+                    Node ns = d_quantEngine->getSubstitute( to_remove[j], inst );
+                    Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl;
+                    ns.setAttribute(NoMatchAttribute(),true);
+                  }
+                  */
+                }else{
+                  Trace("rewrite-engine-inst-debug") << "   - failed." << std::endl;
+                }
+                Trace("rewrite-engine-inst-debug") << "   Get next completion..." << std::endl;
+              }
+            }
+            //Trace("rewrite-engine-inst-debug") << "   Reverted assigned variables : ";
+            //for( unsigned a=0; a<assigned.size(); a++ ) {
+            //  Trace("rewrite-engine-inst-debug") << assigned[a] << " ";
             //}
+            //Trace("rewrite-engine-inst-debug") << std::endl;
+            //qi->revertMatch( assigned );
+            //Assert( assigned.empty() );
+            Trace("rewrite-engine-inst-debug") << "   - failed to complete." << std::endl;
           }else{
-            Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
+            Trace("rewrite-engine-inst-debug") << "   - match is spurious." << std::endl;
           }
+          Trace("rewrite-engine-inst-debug") << "   Get next match..." << std::endl;
         }
+      }else{
+        Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl;
       }
-    }while(success);
+    }else{
+      Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
+    }
   }
-  Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;
+  Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
   return addedLemmas;
 }
 
 void RewriteEngine::registerQuantifier( Node f ) {
-  if( f.hasAttribute(QRewriteRuleAttribute()) ){
-    Trace("rewrite-engine") << "Register quantifier " << f << std::endl;
-    Node rr = f.getAttribute(QRewriteRuleAttribute());
-    Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;
+  Node rr = TermDb::getRewriteRule( f );
+  if( !rr.isNull() ){
+    Trace("rr-register") << "Register quantifier " << f << std::endl;
+    Trace("rr-register") << "  rewrite rule is : " << rr << std::endl;
     d_rr_quant.push_back( f );
-    d_rr_guard[f] = rr[1];
-    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;
+    d_rr[f] = rr;
+    d_needsSort = true;
+    Trace("rr-register") << "  guard is : " << d_rr[f][1] << std::endl;
+
+    QuantConflictFind * qcf = d_quantEngine->getConflictFind();
+    if( qcf ){
+      std::vector< Node > qcfn_c;
+
+      std::vector< Node > bvl;
+      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        bvl.push_back( f[0][i] );
+      }
+
+      std::vector< Node > cc;
+      //Node head = rr[2][0];
+      //if( head!=d_true ){
+        //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head );
+        //head_eq = head_eq.negate();
+        //cc.push_back( head_eq );
+        //Trace("rr-register-debug") << "  head eq is " << head_eq << std::endl;
+      //}
+      //add patterns
+      for( unsigned i=1; i<f[2].getNumChildren(); i++ ){
+        std::vector< Node > nc;
+        for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){
+          Node nn;
+          Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() );
+          if( f[2][i][j].getType().isBoolean() ){
+            if( f[2][i][j].getKind()!=APPLY_UF ){
+              nn = f[2][i][j].negate();
+            }else{
+              nn = f[2][i][j].iffNode( nbv ).negate();
+              bvl.push_back( nbv );
+            }
+            //nn = f[2][i][j].negate();
+          }else{
+            nn = f[2][i][j].eqNode( nbv ).negate();
+            bvl.push_back( nbv );
+          }
+          nc.push_back( nn );
+        }
+        if( !nc.empty() ){
+          Node n = nc.size()==1 ? nc[0] : NodeManager::currentNM()->mkNode( AND, nc );
+          Trace("rr-register-debug") << "  pattern is " << n << std::endl;
+          if( std::find( cc.begin(), cc.end(), n )==cc.end() ){
+            cc.push_back( n );
+          }
+        }
+      }
+      qcfn_c.push_back( NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvl ) );
+
+      std::vector< Node > body_c;
+      //add the guards
+      if( d_rr[f][1].getKind()==AND ){
+        for( unsigned j=0; j<d_rr[f][1].getNumChildren(); j++ ){
+          if( MatchGen::isHandled( d_rr[f][1][j] ) ){
+            body_c.push_back( d_rr[f][1][j].negate() );
+          }
+        }
+      }else if( d_rr[f][1]!=d_true ){
+        if( MatchGen::isHandled( d_rr[f][1] ) ){
+          body_c.push_back( d_rr[f][1].negate() );
+        }
+      }
+      //add the patterns to the body
+      body_c.push_back( cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( AND, cc ) );
+      //make the body
+      qcfn_c.push_back( body_c.size()==1 ? body_c[0] : NodeManager::currentNM()->mkNode( OR, body_c ) );
+      //make the quantified formula
+      d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
+      Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
+      d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] );
+    }
   }
 }
 
@@ -184,3 +292,13 @@ void RewriteEngine::assertNode( Node n ) {
 
 }
 
+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() ){
+    Node nn = d_quantEngine->getTermDatabase()->getInstConstantNode( n, q );
+    d_inst_const_node[q][n] = nn;
+    return nn;
+  }else{
+    return it->second;
+  }
+}
\ No newline at end of file