Minor improvements for alpha equivalence and partial quantifier elimination in increm...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bd67af4661c8f99479ca6560ccfd85fa1a49c383..771195a381d8410538b3e592339641e4eebbe564 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5152,7 +5152,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
 
     //ensure all instantiations were accounted for
     for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
-      if( visited.find( it->first )==visited.end() ){
+      if( !it->second.empty() && visited.find( it->first )==visited.end() ){
         stringstream ss;
         ss << "While performing quantifier elimination, processed a quantified formula : " << it->first;
         ss << " that was not related to the query.  Try option --simplification=none.";

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 8abc3f65a396fbd1652dab077ef033ec91306b33..80066d690553d844525250d00ba7f56de3e782b3 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -29,7 +29,7 @@ struct sortTypeOrder {
   }
 };
 
-bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
   while( !tt.empty() ){
     if( tt.size()==arg_index.size()+1 ){
       Node t = tt.back();
@@ -49,26 +49,25 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
       }
     }
   }
+  Node lem;
   Trace("aeq-debug") << std::endl;
   if( aen->d_quant.isNull() ){
     aen->d_quant = q;
-    return true;
   }else{
     if( q.getNumChildren()==2 ){
       //lemma ( q <=> d_quant )
       Trace("quant-ae") << "Alpha equivalent : " << std::endl;
       Trace("quant-ae") << "  " << q << std::endl;
       Trace("quant-ae") << "  " << aen->d_quant << std::endl;
-      qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
-      return false;
+      lem = q.iffNode( aen->d_quant );
     }else{
       //do not reduce annotated quantified formulas based on alpha equivalence 
-      return true;
     }
   }
+  return lem;
 }
 
-bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
+Node AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
                                              QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
   while( index<(int)typs.size() ){
     TypeNode curr = typs[index];
@@ -84,7 +83,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
   return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
 }
 
-bool AlphaEquivalence::reduceQuantifier( Node q ) {
+Node AlphaEquivalence::reduceQuantifier( Node q ) {
   Assert( q.getKind()==FORALL );
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
@@ -104,7 +103,7 @@ bool AlphaEquivalence::reduceQuantifier( Node q ) {
   sto.d_tdb = d_qe->getTermDatabase();
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+  Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 40f533da764d6603d0da3c258474d1cf05a4c54b..8e7556eb61f81ab9363626e54905ab42efd6faa3 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -28,14 +28,14 @@ class AlphaEquivalenceNode {
 public:
   std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
   Node d_quant;
-  static bool registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+  static Node registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
 };
 
 class AlphaEquivalenceTypeNode {
 public:
   std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
   AlphaEquivalenceNode d_data;
-  static bool registerNode( AlphaEquivalenceTypeNode* aetn,
+  static Node registerNode( AlphaEquivalenceTypeNode* aetn,
                             QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
 };
 
@@ -47,8 +47,8 @@ private:
 public:
   AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
   ~AlphaEquivalence(){}
-
-  bool reduceQuantifier( Node q );
+  /** reduce quantifier, return value (if non-null) is lemma justifying why q ia reducible. */
+  Node reduceQuantifier( Node q );
 };
 
 }

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index dd6db951da1c0a084bcaa296e0692ab0d5b8fb2f..5192da7ded8bb631a2ff1d2ad4da45408f0cf454 100644 (file)
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -159,7 +159,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
       return true;
     }else{
       if( depth==q[0].getNumChildren() ){
-        if( qe->addInstantiation( q, terms ) ){
+        if( qe->addInstantiation( q, terms, true ) ){
           Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;
           inst++;
           return true;

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index b00ddf036988f0e3d990bcfa54e321c9368e88b3..d9059a3e606df5bb50fc6dcb77d04f51673f3ae6 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -432,7 +432,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       Assert( aq==q );
       std::vector< Node > model_terms;
       if( getModelValues( conj, conj->d_candidates, model_terms ) ){
-        d_quantEngine->addInstantiation( q, model_terms, false );
+        d_quantEngine->addInstantiation( q, model_terms );
       }
     }
   }else{

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6b06b9e5c71687330372231194bd41b794100431..33c8533289e7165c844e797d1b683d30dd289115 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -682,7 +682,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
               }else{
                 //just add the instance
                 d_triedLemmas++;
-                if( d_qe->addInstantiation( f, inst ) ){
+                if( d_qe->addInstantiation( f, inst, true ) ){
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
                   if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
@@ -810,7 +810,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       if (ev!=d_true) {
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if( d_qe->addInstantiation( f, inst ) ){
+        if( d_qe->addInstantiation( f, inst, true ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
           if( d_qe->inConflict() || options::fmfOneInstPerRound() ){

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 55a4e8f8c8aa40d03268579e411367731d10208d..8818175db4fe3ae63864cc7c08610135b0cab7b6 100644 (file)
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -142,7 +142,7 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
 }
 
 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
-                                  bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) {
+                                  ImtIndexOrder* imtio, bool onlyExist, int index ) {
   if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
     return false;
   }else{
@@ -150,7 +150,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
     Node n = m[i_index];
     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
+      bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 );
       if( !onlyExist || !ret ){
         return ret;
       }
@@ -165,7 +165,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
           if( en!=n ){
             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
             if( itc!=d_data.end() ){
-              if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+              if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){
                 return false;
               }
             }
@@ -175,7 +175,7 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
       }
     }
     if( !onlyExist ){
-      d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+      d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 );
     }
     return true;
   }
@@ -240,7 +240,7 @@ CDInstMatchTrie::~CDInstMatchTrie() {
 
 
 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
-                                    context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+                                    context::Context* c, bool modEq, int index, bool onlyExist ){
   bool reset = false;
   if( !d_valid.get() ){
     if( onlyExist ){
@@ -256,7 +256,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
     Node n = m[ index ];
     std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
+      bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist );
       if( !onlyExist || !ret ){
         return reset || ret;
       }
@@ -271,7 +271,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
           if( en!=n ){
             std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
             if( itc!=d_data.end() ){
-              if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+              if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){
                 return false;
               }
             }
@@ -286,7 +286,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
       CDInstMatchTrie* imt = new CDInstMatchTrie( c );
       Assert(d_data.find(n) == d_data.end());
       d_data[n] = imt;
-      imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+      imt->addInstMatch( qe, f, m, c, modEq, index+1, false );
     }
     return true;
   }

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a87d2704edcfe2aaf3817904034115345a7524f3..ad287c1a3adfc60794e4d37696afa86e8f79569a 100644 (file)
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -111,23 +111,23 @@ public:
         modInst is if we return true if m is an instance of a match that exists
    */
   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
-    return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+                        ImtIndexOrder* imtio = NULL, int index = 0 ) {
+    return !addInstMatch( qe, f, m, modEq, imtio, true, index );
   }
   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
-                        bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
-    return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+                        ImtIndexOrder* imtio = NULL, int index = 0 ) {
+    return !addInstMatch( qe, f, m, modEq, imtio, true, index );
   }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
-    return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
+                     ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
+    return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
   }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+                     ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
   bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
   void print( std::ostream& out, Node q ) const{
     std::vector< TNode > terms;
@@ -159,23 +159,23 @@ public:
         modInst is if we return true if m is an instance of a match that exists
    */
   bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
-                        bool modInst = false, int index = 0 ) {
-    return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
+                        int index = 0 ) {
+    return !addInstMatch( qe, q, m, c, modEq, index, true );
   }
   bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
-                        bool modInst = false, int index = 0 ) {
-    return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
+                        int index = 0 ) {
+    return !addInstMatch( qe, q, m, c, modEq, index, true );
   }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
-                     bool modInst = false, int index = 0, bool onlyExist = false ) {
-    return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist );
+                     int index = 0, bool onlyExist = false ) {
+    return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
   }
   bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
-                     bool modInst = false, int index = 0, bool onlyExist = false );
+                     int index = 0, bool onlyExist = false );
   bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
   void print( std::ostream& out, Node q ) const{
     std::vector< TNode > terms;
@@ -202,10 +202,10 @@ public:
 public:
   /** add match m, return true if successful */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
-    return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
+    return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
   }
   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
-    return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
+    return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
   }
 };/* class InstMatchTrieOrdered */
 

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 791e36ce45a4c94037a0b40565430cd01ba1980b..bf05de3bb4e2eb1e1f6bb98eb1743a5ea61b8345 100644 (file)
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -270,7 +270,7 @@ bool InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEng
     return d_next->getNextMatch( f, m, qe );
   }else{
     if( d_active_add ){
-      return qe->addInstantiation( f, m, false );
+      return qe->addInstantiation( f, m );
     }else{
       return true;
     }
@@ -343,7 +343,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
   while( getNextMatch( f, m, qe ) ){
     if( !d_active_add ){
       m.add( baseMatch );
-      if( qe->addInstantiation( f, m, false ) ){
+      if( qe->addInstantiation( f, m ) ){
         addedLemmas++;
         if( qe->inConflict() ){
           break;
@@ -366,7 +366,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
   if( !d_match_pattern.isNull() ){
     InstMatch m( f );
     if( getMatch( f, t, m, qe ) ){
-      if( qe->addInstantiation( f, m, false ) ){
+      if( qe->addInstantiation( f, m ) ){
         return 1;
       }
     }
@@ -674,7 +674,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
     }
   }else{
     //m is an instantiation
-    if( qe->addInstantiation( d_f, m, false ) ){
+    if( qe->addInstantiation( d_f, m ) ){
       addedLemmas++;
       Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
     }
@@ -770,7 +770,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
       Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
       m.setValue( it->second, t[it->first] );
     }
-    if( qe->addInstantiation( d_f, m, false ) ){
+    if( qe->addInstantiation( d_f, m ) ){
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
     }
@@ -815,7 +815,7 @@ int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
       return 0;
     }
   }
-  return qe->addInstantiation( q, m, false ) ? 1 : 0;
+  return qe->addInstantiation( q, m ) ? 1 : 0;
 }
 
 }/* CVC4::theory::inst namespace */

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index fe4867b4e8168071caf81db44ba49a0e5f731947..149330c61cf6abd72b9bd03f6949464bd57cbde2 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -648,12 +648,12 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true );
+    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
-    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
       //d_added_inst.insert( d_curr_quant );
       return true;
     }else{

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8c67eb95eaf2ef451cb6d790ce700b97d6273710..630880690fab4dfc359a2f7cd03225c1457bba59 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -599,18 +599,6 @@ bool FullSaturation::process( Node f, bool fullEffort ){
   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
   unsigned rend = fullEffort ? 1 : rstart;
   for( unsigned r=rstart; r<=rend; r++ ){
-      /*
-      //complete guess
-      if( d_guessed.find( f )==d_guessed.end() ){
-        Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
-        d_guessed[f] = true;
-        InstMatch m( f );
-        if( d_quantEngine->addInstantiation( f, m ) ){
-          ++(d_quantEngine->d_statistics.d_instantiations_guess);
-          return true;
-        }
-      }
-      */
     if( rd || r>0 ){
       if( r==0 ){
         Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
@@ -700,7 +688,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                   Trace("inst-alg-rd") << "  " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl;
                 }
               }
-              if( d_quantEngine->addInstantiation( f, terms, false ) ){
+              if( d_quantEngine->addInstantiation( f, terms ) ){
                 Trace("inst-alg-rd") << "Success!" << std::endl;
                 ++(d_quantEngine->d_statistics.d_instantiations_guess);
                 return true;

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index b0ca43cfe5026be5cbb22f3806d18be13532351d..3ae36b1d485a3fb4fcb50a5200a9c06710e57741 100644 (file)
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -280,7 +280,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
     //try to add it
     Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
     //add model basis instantiation
-    if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){
+    if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){
       d_quant_basis_match_added[f] = true;
       return 1;
     }else{
@@ -430,7 +430,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           //add as instantiation
-          if( d_qe->addInstantiation( f, m ) ){
+          if( d_qe->addInstantiation( f, m, true ) ){
             d_addedLemmas++;
             if( d_qe->inConflict() ){
               break;

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f94e947e54b7488f2db6d016ffd950f7595df9d9..0bbca88eb57899f7a3096403af92e864c19dc2e6 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -294,7 +294,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if( d_quantEngine->addInstantiation( f, m ) ){
+          if( d_quantEngine->addInstantiation( f, m, true ) ){
             addedLemmas++;
             if( d_quantEngine->inConflict() ){
               break;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c796333b3a1347f918c365fbd2354cc78de700d7..ca87a607db5fbc896ebe0da7023f7dfc894d4964 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2004,7 +2004,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       Assert( !getTermDatabase()->isEntailed( inst, true ) );
                       Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
                     }
-                    if( d_quantEngine->addInstantiation( q, terms, false ) ){
+                    if( d_quantEngine->addInstantiation( q, terms ) ){
                       Trace("qcf-check") << "   ... Added instantiation" << std::endl;
                       Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
                       qi->debugPrintMatch("qcf-inst");

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 07b1462c6b9b2306b5522255a7e8b465c4eb2d64..5365dbcfae593a825868a7785ff6cb8dae6eec72 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -154,7 +154,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
                 if( inst.size()>f[0].getNumChildren() ){
                   inst.resize( f[0].getNumChildren() );
                 }
-                if( d_quantEngine->addInstantiation( f, inst, false ) ){
+                if( d_quantEngine->addInstantiation( f, inst ) ){
                   addedLemmas++;
                   tempAddedLemmas++;
                   /*

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1008d7d493c58b0b3407670de66f8b2e365718dd..6d3b1725436af51ce8fbd817039fdc67f598e861 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -58,7 +58,7 @@ using namespace CVC4::theory::inst;
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
     d_te( te ),
     //d_quants(u),
-    //d_quants_red(u),
+    d_quants_red(u),
     d_lemmas_produced_c(u),
     d_skolemized(u),
     d_ierCounter_c(c),
@@ -385,6 +385,14 @@ void QuantifiersEngine::check( Theory::Effort e ){
     if( d_hasAddedLemma ){
       return;
     }
+    if( !d_recorded_inst.empty() ){
+      Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl;
+      //remove explicitly recorded instantiations
+      for( unsigned i=0; i<d_recorded_inst.size(); i++ ){
+        removeInstantiationInternal( d_recorded_inst[i].first, d_recorded_inst[i].second );
+      } 
+      d_recorded_inst.clear();
+    }
 
     if( Trace.isOn("quant-engine-debug") ){
       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -503,6 +511,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
           }
         }else if( quant_e==QEFFORT_MODEL ){
           if( e==Theory::EFFORT_LAST_CALL ){
+            if( !d_recorded_inst.empty() ){
+              setIncomplete = true;
+            }
             //if we have a chance not to set incomplete
             if( !setIncomplete ){
               setIncomplete = false;
@@ -572,20 +583,29 @@ void QuantifiersEngine::notifyCombineTheories() {
 }
 
 bool QuantifiersEngine::reduceQuantifier( Node q ) {
-  std::map< Node, bool >::iterator it = d_quants_red.find( q );
+  BoolMap::const_iterator it = d_quants_red.find( q );
   if( it==d_quants_red.end() ){
-    if( d_alpha_equiv ){
-      Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
-      //add equivalence with another quantified formula
-      if( d_alpha_equiv->reduceQuantifier( q ) ){
-        Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
-        ++(d_statistics.d_red_alpha_equiv);
-        d_quants_red[q] = true;
-        return true;
+    Node lem;
+    std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
+    if( itr==d_quants_red_lem.end() ){
+      if( d_alpha_equiv ){
+        Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
+        //add equivalence with another quantified formula
+        lem = d_alpha_equiv->reduceQuantifier( q );
+        if( !lem.isNull() ){
+          Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
+          ++(d_statistics.d_red_alpha_equiv);
+        }
       }
+      d_quants_red_lem[q] = lem;
+    }else{
+      lem = itr->second;
     }
-    d_quants_red[q] = false;
-    return false;
+    if( !lem.isNull() ){
+      getOutputChannel().lemma( lem );
+    }
+    d_quants_red[q] = !lem.isNull();
+    return !lem.isNull();
   }else{
     return (*it).second;
   }
@@ -759,13 +779,13 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
 }
 
 
-bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) {
+bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
   if( !addedLem ){
     //record the instantiation for deletion later
-    //TODO
+    d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
   }
   if( options::incrementalSolving() ){
-    Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
+    Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl;
     inst::CDInstMatchTrie* imt;
     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
     if( it!=d_c_inst_match_trie.end() ){
@@ -774,10 +794,10 @@ bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >
       imt = new CDInstMatchTrie( getUserContext() );
       d_c_inst_match_trie[q] = imt;
     }
-    return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
+    return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
   }else{
     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-    return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
+    return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
   }
 }
 
@@ -906,24 +926,20 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bo
 }
 
 /*
-bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
   if( options::incrementalSolving() ){
     if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
-      if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
+      if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
         return true;
       }
     }
   }else{
     if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-      if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+      if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
         return true;
       }
     }
   }
-  //also check model builder (it may contain instantiations internally)
-  if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
-    return true;
-  }
   return false;
 }
 */
@@ -969,13 +985,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
   d_phase_req_waiting[lit] = req;
 }
 
-bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
+bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
   std::vector< Node > terms;
   m.getTerms( q, terms );
-  return addInstantiation( q, terms, mkRep, modEq, modInst, doVts );
+  return addInstantiation( q, terms, mkRep, modEq, doVts );
 }
 
-bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
+bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
   // For resource-limiting (also does a time check).
   getOutputChannel().safePoint(options::quantifierStep());
   Assert( !d_conflict );
@@ -1052,7 +1068,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   }
 
   //check for term vector duplication
-  bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
+  bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
   if( alreadyExists ){
     Trace("inst-add-debug") << " --> Already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate_eq);

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index a088dfec64e124f57f0e340c4b607c53f197cd57..4ee66f9e7969050203ca4530895573d0d35929a1 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -164,7 +164,8 @@ private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
   /** quantifiers reduced */
-  std::map< Node, bool > d_quants_red;
+  BoolMap d_quants_red;
+  std::map< Node, Node > d_quants_red_lem;
   /** list of all lemmas produced */
   //std::map< Node, bool > d_lemmas_produced;
   BoolMap d_lemmas_produced_c;
@@ -175,6 +176,8 @@ private:
   /** list of all instantiations produced for each quantifier */
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
+  /** recorded instantiations */
+  std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
   /** quantifiers that have been skolemized */
   BoolMap d_skolemized;
   /** term database */
@@ -287,7 +290,7 @@ private:
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
   /** record instantiation, return true if it was non-duplicate */
-  bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true );
+  bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
   /** remove instantiation */
   bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
   /** set instantiation level attr */
@@ -310,9 +313,9 @@ public:
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
   /** do instantiation specified by m */
-  bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+  bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
   /** add instantiation */
-  bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+  bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
   /** remove pending instantiation */
   bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
   /** split on node n */