more cleanup of quantifiers code

1 files changed, 33 insertions, 222 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4d7e93ef2..9d7c8e315 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -34,35 +34,9 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-//#define COMPUTE_RELEVANCE
-//#define REWRITE_ASSERTED_QUANTIFIERS
-
-  /** reset instantiation */
-void InstStrategy::resetInstantiationRound( Theory::Effort effort ){
-  d_no_instantiate_temp.clear();
-  d_no_instantiate_temp.insert( d_no_instantiate_temp.begin(), d_no_instantiate.begin(), d_no_instantiate.end() );
-  processResetInstantiationRound( effort );
-}
-
-/** do instantiation round method */
-int InstStrategy::doInstantiation( Node f, Theory::Effort effort, int e ){
-  if( shouldInstantiate( f ) ){
-    int origLemmas = d_quantEngine->getNumLemmasWaiting();
-    int retVal = process( f, effort, e );
-    if( d_quantEngine->getNumLemmasWaiting()!=origLemmas ){
-      for( int i=0; i<(int)d_priority_over.size(); i++ ){
-        d_priority_over[i]->d_no_instantiate_temp.push_back( f );
-      }
-    }
-    return retVal;
-  }else{
-    return STATUS_UNKNOWN;
-  }
-}
-
 QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
 d_te( te ),
-d_active( c ){
+d_quant_rel( false ){ //currently do not care about relevance
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_hasAddedLemma = false;
@@ -122,8 +96,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
 
   d_hasAddedLemma = false;
-  d_model_set = false;
-  d_resetInstRound = false;
   if( e==Theory::EFFORT_LAST_CALL ){
     ++(d_statistics.d_instantiation_rounds_lc);
   }else if( e==Theory::EFFORT_FULL ){
@@ -141,7 +113,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   //build the model if not done so already
   //  this happens if no quantifiers are currently asserted and no model-building module is enabled
-  if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){
+  if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
     d_te->getModelBuilder()->buildModel( d_model, true );
   }
 }
@@ -161,68 +133,23 @@ std::vector<Node> QuantifiersEngine::createInstVariable( std::vector<Node> & var
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
     d_quants.push_back( f );
-    std::vector< Node > quants;
-#ifdef REWRITE_ASSERTED_QUANTIFIERS
-    //do assertion-time rewriting of quantifier
-    Node nf = quantifiers::QuantifiersRewriter::rewriteQuant( f, false, false );
-    if( nf!=f ){
-      Debug("quantifiers-rewrite") << "*** assert-rewrite " << f << std::endl;
-      Debug("quantifiers-rewrite") << " to " << std::endl;
-      Debug("quantifiers-rewrite") << nf << std::endl;
-      //we will instead register all the rewritten quantifiers
-      if( nf.getKind()==FORALL ){
-        quants.push_back( nf );
-      }else if( nf.getKind()==AND ){
-        for( int i=0; i<(int)nf.getNumChildren(); i++ ){
-          quants.push_back( nf[i] );
-        }
-      }else{
-        //unhandled: rewrite must go to a quantifier, or conjunction of quantifiers
-        Assert( false );
-      }
-    }else{
-      quants.push_back( f );
+
+    ++(d_statistics.d_num_quant);
+    Assert( f.getKind()==FORALL );
+    //make instantiation constants for f
+    d_term_db->makeInstantiationConstantsFor( f );
+    //register with quantifier relevance
+    d_quant_rel.registerQuantifier( f );
+    //register with each module
+    for( int i=0; i<(int)d_modules.size(); i++ ){
+      d_modules[i]->registerQuantifier( f );
     }
-#else
-    quants.push_back( f );
-#endif
-    for( int q=0; q<(int)quants.size(); q++ ){
-      d_quant_rewritten[f].push_back( quants[q] );
-      d_rewritten_quant[ quants[q] ] = f;
-      ++(d_statistics.d_num_quant);
-      Assert( quants[q].getKind()==FORALL );
-      //register quantifier
-      d_r_quants.push_back( quants[q] );
-      //make instantiation constants for quants[q]
-      d_term_db->makeInstantiationConstantsFor( quants[q] );
-      //compute symbols in quants[q]
-      std::vector< Node > syms;
-      computeSymbols( quants[q][1], syms );
-      d_syms[quants[q]].insert( d_syms[quants[q]].begin(), syms.begin(), syms.end() );
-      //set initial relevance
-      int minRelevance = -1;
-      for( int i=0; i<(int)syms.size(); i++ ){
-        d_syms_quants[ syms[i] ].push_back( quants[q] );
-        int r = getRelevance( syms[i] );
-        if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
-          minRelevance = r;
-        }
-      }
-#ifdef COMPUTE_RELEVANCE
-      if( minRelevance!=-1 ){
-        setRelevance( quants[q], minRelevance+1 );
-      }
-#endif
-      //register with each module
-      for( int i=0; i<(int)d_modules.size(); i++ ){
-        d_modules[i]->registerQuantifier( quants[q] );
-      }
-      Node ceBody = d_term_db->getCounterexampleBody( quants[q] );
-      generatePhaseReqs( quants[q], ceBody );
-      //also register it with the strong solver
-      if( options::finiteModelFind() ){
-        ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] );
-      }
+    Node ceBody = d_term_db->getInstConstantBody( f );
+    //generate the phase requirements
+    d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+    //also register it with the strong solver
+    if( options::finiteModelFind() ){
+      ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
     }
   }
 }
@@ -236,11 +163,9 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 
 void QuantifiersEngine::assertNode( Node f ){
   Assert( f.getKind()==FORALL );
-  for( int j=0; j<(int)d_quant_rewritten[f].size(); j++ ){
-    d_model->assertQuantifier( d_quant_rewritten[f][j] );
-    for( int i=0; i<(int)d_modules.size(); i++ ){
-      d_modules[i]->assertNode( d_quant_rewritten[f][j] );
-    }
+  d_model->assertQuantifier( f );
+  for( int i=0; i<(int)d_modules.size(); i++ ){
+    d_modules[i]->assertNode( f );
   }
 }
 
@@ -263,15 +188,12 @@ Node QuantifiersEngine::getNextDecisionRequest(){
 }
 
 void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
-  //if( !d_resetInstRound ){
-  d_resetInstRound = true;
   for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
     if( getInstantiator( i ) ){
       getInstantiator( i )->resetInstantiationRound( level );
     }
   }
   getTermDatabase()->reset( level );
-  //}
 }
 
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
@@ -281,16 +203,12 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
     uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
     d_ith->newTerms(added);
   }
-#ifdef COMPUTE_RELEVANCE
   //added contains also the Node that just have been asserted in this branch
-  for( std::set< Node >::iterator i=added.begin(), end=added.end();
-       i!=end; i++ ){
+  for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
     if( !withinQuant ){
-      setRelevance( i->getOperator(), 0 );
+      d_quant_rel.setRelevance( i->getOperator(), 0 );
     }
   }
-#endif
-
 }
 
 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
@@ -316,7 +234,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
     }
     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-    Trace("partial-inst") << "Partial instantiation : " << d_rewritten_quant[f] << std::endl;
+    Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
     Trace("partial-inst") << "                      : " << body << std::endl;
   }
   return body;
@@ -330,7 +248,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 }
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
-  return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, NULL, modInst );
+  return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst );
 }
 
 bool QuantifiersEngine::addLemma( Node lem ){
@@ -355,7 +273,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   Node body = getInstantiation( f, vars, terms );
   //make the lemma
   NodeBuilder<> nb(kind::OR);
-  nb << d_rewritten_quant[f].notNode() << body;
+  nb << f.notNode() << body;
   Node lem = nb;
   //check for duplication
   if( addLemma( lem ) ){
@@ -462,15 +380,17 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){
 }
 
 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
-  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE ){
-    bool printed = false;
+  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
     // doing literal-based matching (consider polarity of literals)
     for( int i=0; i<(int)nodes.size(); i++ ){
       Node prev = nodes[i];
       bool nodeChanged = false;
-      if( isPhaseReq( f, nodes[i] ) ){
-        bool preq = getPhaseReq( f, nodes[i] );
-        nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
+      if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
+        bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
+        std::vector< Node > children;
+        children.push_back( nodes[i] );
+        children.push_back( NodeManager::currentNM()->mkConst<bool>(preq) );
+        nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f );
         nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
@@ -478,13 +398,7 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
       //  trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
       //}
       if( nodeChanged ){
-        if( !printed ){
-          Debug("literal-matching") << "LitMatch for " << f << ":" << std::endl;
-          printed = true;
-        }
         Debug("literal-matching") << "  Make " << prev << " -> " << nodes[i] << std::endl;
-        Assert( prev.hasAttribute(InstConstantAttribute()) );
-        d_term_db->setInstantiationConstantAttr( nodes[i], prev.getAttribute(InstConstantAttribute()) );
         ++(d_statistics.d_lit_phase_req);
       }else{
         ++(d_statistics.d_lit_phase_nreq);
@@ -495,76 +409,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
   }
 }
 
-void QuantifiersEngine::computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
-  bool newReqPol = false;
-  bool newPolarity;
-  if( n.getKind()==NOT ){
-    newReqPol = true;
-    newPolarity = !polarity;
-  }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
-    if( !polarity ){
-      newReqPol = true;
-      newPolarity = false;
-    }
-  }else if( n.getKind()==AND ){
-    if( polarity ){
-      newReqPol = true;
-      newPolarity = true;
-    }
-  }else{
-    int val = polarity ? 1 : -1;
-    if( phaseReqs.find( n )==phaseReqs.end() ){
-      phaseReqs[n] = val;
-    }else if( val!=phaseReqs[n] ){
-      phaseReqs[n] = 0;
-    }
-  }
-  if( newReqPol ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n.getKind()==IMPLIES && i==0 ){
-        computePhaseReqs2( n[i], !newPolarity, phaseReqs );
-      }else{
-        computePhaseReqs2( n[i], newPolarity, phaseReqs );
-      }
-    }
-  }
-}
-
-void QuantifiersEngine::computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ){
-  std::map< Node, int > phaseReqs2;
-  computePhaseReqs2( n, polarity, phaseReqs2 );
-  for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
-    if( it->second==1 ){
-      phaseReqs[ it->first ] = true;
-    }else if( it->second==-1 ){
-      phaseReqs[ it->first ] = false;
-    }
-  }
-}
-
-void QuantifiersEngine::generatePhaseReqs( Node f, Node n ){
-  computePhaseReqs( n, false, d_phase_reqs[f] );
-  Debug("inst-engine-phase-req") << "Phase requirements for " << f << ":" << std::endl;
-  //now, compute if any patterns are equality required
-  for( std::map< Node, bool >::iterator it = d_phase_reqs[f].begin(); it != d_phase_reqs[f].end(); ++it ){
-    Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
-    if( it->first.getKind()==EQUAL ){
-      if( it->first[0].hasAttribute(InstConstantAttribute()) ){
-        if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
-          d_phase_reqs_equality_term[f][ it->first[0] ] = it->first[1];
-          d_phase_reqs_equality[f][ it->first[0] ] = it->second;
-          Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
-        }
-      }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
-        d_phase_reqs_equality_term[f][ it->first[1] ] = it->first[0];
-        d_phase_reqs_equality[f][ it->first[1] ] = it->second;
-        Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
-      }
-    }
-  }
-
-}
-
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
@@ -644,39 +488,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
 }
 
-/** compute symbols */
-void QuantifiersEngine::computeSymbols( Node n, std::vector< Node >& syms ){
-  if( n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
-      syms.push_back( op );
-    }
-  }
-  if( n.getKind()!=FORALL ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      computeSymbols( n[i], syms );
-    }
-  }
-}
-
-/** set relevance */
-void QuantifiersEngine::setRelevance( Node s, int r ){
-  int rOld = getRelevance( s );
-  if( rOld==-1 || r<rOld ){
-    d_relevance[s] = r;
-    if( s.getKind()==FORALL ){
-      for( int i=0; i<(int)d_syms[s].size(); i++ ){
-        setRelevance( d_syms[s][i], r );
-      }
-    }else{
-      for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
-        setRelevance( d_syms_quants[s][i], r+1 );
-      }
-    }
-  }
-}
-
-
 
 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
   eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();