Variable patterns only look at eligible terms. Minor refactoring of quantifiers check for sat.

7 files changed, 93 insertions, 93 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 9e3fed20a..7d2544b6f 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -200,7 +200,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     TNode n = (*d_eq);
     ++d_eq;
     if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
-      TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n );
+      TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 ){
           nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 2a9a764b9..088ba093f 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -257,8 +257,8 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
 }
 
 
-QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){
-  
+QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){
+
 }
 
 /** add quantifier */
@@ -278,7 +278,7 @@ bool QuantLtePartialInst::addQuantifier( Node q ) {
       vars[q[0][i]] = true;
     }
     getEligibleInstVars( q[1], vars );
-    
+
     //TODO : instantiate only if we would force ground instances?
     bool doInst = true;
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
@@ -290,7 +290,7 @@ bool QuantLtePartialInst::addQuantifier( Node q ) {
       }
     }
     Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
-    d_do_inst[q] = doInst;    
+    d_do_inst[q] = doInst;
     if( doInst ){
       d_lte_asserts.push_back( q );
     }
@@ -354,11 +354,12 @@ void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
       getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 );
       Assert( !conj.empty() );
       lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
+      d_wasInvoked = true;
     }
   }
 }
 
-void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, 
+void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
                                                     std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){
   if( index==vars.size() ){
     Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index c1c39fa0f..116211bfb 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -28,7 +28,7 @@ namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
-  
+
 class QuantArith
 {
 public:
@@ -112,6 +112,9 @@ public:
 
 class QuantLtePartialInst {
 private:
+  // was this module invoked
+  bool d_wasInvoked;
+  //representatives per type
   std::map< TypeNode, std::vector< Node > > d_reps;
   // should we instantiate quantifier
   std::map< Node, bool > d_do_inst;
@@ -125,7 +128,7 @@ private:
   /** reset */
   void reset();
   /** get instantiations */
-  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, 
+  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
                                  std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index );
   /** get eligible inst variables */
   void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
@@ -135,6 +138,8 @@ public:
   bool addQuantifier( Node q );
   /** get instantiations */
   void getInstantiations( std::vector< Node >& lemmas );
+  /** was invoked */
+  bool wasInvoked() { return d_wasInvoked; }
 };
 
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index fb28974a9..0f0329a93 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -338,33 +338,60 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   }
 }
 
-Node TermDb::getHasTermEqc( Node r ) {
-  if( hasTermCurrent( r ) ){
+bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
+  if( options::lteRestrictInstClosure() ){
+    //has to be both in inst closure and in ground assertions
+    if( !isInstClosure( n ) ){
+      Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
+      return false;
+    }
+    // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
+    if( !hasTermCurrent( n, false ) ){
+      Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
+      return false;
+    }
+  }
+  if( options::instMaxLevel()!=-1 ){
+    if( n.hasAttribute(InstLevelAttribute()) ){
+      int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f );
+      unsigned ml = fml>=0 ? fml : options::instMaxLevel();
+
+      if( n.getAttribute(InstLevelAttribute())>ml ){
+        Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
+        Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
+        return false;
+      }
+    }else{
+      if( options::instLevelInputOnly() ){
+        Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+Node TermDb::getEligibleTermInEqc( TNode r ) {
+  if( isTermEligibleForInstantiation( r, TNode::null() ) ){
     return r;
   }else{
-    /*
-    if( options::termDbInstClosure()  ){
-      std::map< Node, Node >::iterator it = d_has_eqc.find( r );
-      if( it==d_has_eqc.end() ){
-        Node h;
-        eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-        while( h.isNull() && !eqc_i.isFinished() ){
-          TNode n = (*eqc_i);
-          ++eqc_i;
-          if( hasTermCurrent( n ) ){
-            h = n;
-          }
+    std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
+    if( it==d_term_elig_eqc.end() ){
+      Node h;
+      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+      while( h.isNull() && !eqc_i.isFinished() ){
+        TNode n = (*eqc_i);
+        ++eqc_i;
+        if( hasTermCurrent( n ) ){
+          h = n;
         }
-        d_has_eqc[r] = h;
-        return h;
-      }else{
-        return it->second;
       }
+      d_term_elig_eqc[r] = h;
+      return h;
+    }else{
+      return it->second;
     }
-    */
-    //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
-    return Node::null();
   }
 }
 
@@ -404,7 +431,7 @@ void TermDb::reset( Theory::Effort effort ){
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
     d_has_map.clear();
-    d_has_eqc.clear();
+    d_term_elig_eqc.clear();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
       TNode r = (*eqcs_i);
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 8a20d6b41..eb491d036 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -151,7 +151,7 @@ public:
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
-  std::map< Node, Node > d_has_eqc;
+  std::map< Node, Node > d_term_elig_eqc;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
@@ -184,8 +184,10 @@ public:
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
   /** has term */
   bool hasTermCurrent( Node n, bool useMode = true );
+  /** is term eligble for instantiation? */
+  bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false );
   /** get has term eqc */
-  Node getHasTermEqc( Node r );
+  Node getEligibleTermInEqc( TNode r );
   /** is inst closure */
   bool isInstClosure( Node r );
 //for model basis
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 13822eb98..2cf6002cd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -286,7 +286,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
   }
-  bool defaultBuildModel = false;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
     Trace("quant-engine-debug") << "  modules to check : ";
@@ -371,19 +370,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
-
-    //build the model if not done so already
-    //  this happens if no quantifiers are currently asserted and no model-building module is enabled
-    if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
-      if( options::produceModels() && !d_model->isModelSet() ){
-        defaultBuildModel = true;
-      }
-      if( Trace.isOn("inst-per-quant") ){
-        for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
-          Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
-        }
-      }
-    }else{
+    if( d_hasAddedLemma ){
+      //debug information
       if( Trace.isOn("inst-per-quant-round") ){
         for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
           Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
@@ -392,16 +380,29 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
-  }else{
-    if( e==Theory::EFFORT_LAST_CALL && options::produceModels() ){
-      defaultBuildModel = true;
-    }
   }
-
-  if( defaultBuildModel ){
-    Trace("quant-engine-debug") << "Build the model..." << std::endl;
-    d_te->getModelBuilder()->buildModel( d_model, true );
-    Trace("quant-engine-debug") << "Done building the model." << std::endl;
+  //SAT case
+  if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+    if( options::produceModels() && !d_model->isModelSet() ){
+      //use default model builder when no module built the model
+      Trace("quant-engine-debug") << "Build the model..." << std::endl;
+      d_te->getModelBuilder()->buildModel( d_model, true );
+      Trace("quant-engine-debug") << "Done building the model." << std::endl;
+    }
+    //check other sources of incompleteness
+    bool setInc = false;
+    if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
+      setInc = true;
+    }
+    if( setInc ){
+      getOutputChannel().setIncomplete();
+    }
+    //output debug stats
+    if( Trace.isOn("inst-per-quant") ){
+      for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
+        Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
+      }
+    }
   }
 }
 
@@ -603,40 +604,6 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
   }
 }
 
-bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) {
-  if( options::lteRestrictInstClosure() ){
-    //has to be both in inst closure and in ground assertions
-    if( !d_term_db->isInstClosure( n ) ){
-      Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
-      return false;
-    }
-    // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
-    if( !d_term_db->hasTermCurrent( n, false ) ){
-      Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
-      return false;
-    }
-  }
-  if( options::instMaxLevel()!=-1 ){
-    if( n.hasAttribute(InstLevelAttribute()) ){
-      int fml = d_term_db->getQAttrQuantInstLevel( f );
-      unsigned ml = fml>=0 ? fml : options::instMaxLevel();
-
-      if( n.getAttribute(InstLevelAttribute())>ml ){
-        Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
-        Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
-        return false;
-      }
-    }else{
-      if( options::instLevelInputOnly() ){
-        Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-
 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
   if( n.getKind()==INST_CONSTANT ){
     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
@@ -791,7 +758,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   //check based on instantiation level
   if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( !isTermEligibleForInstantiation( terms[i], f, true ) ){
+      if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){
         return false;
       }
     }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 14e26f2b6..c533f4cbb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -282,8 +282,6 @@ public:
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
-  /** is term eligble for instantiation? */
-  bool isTermEligibleForInstantiation( Node n, Node f, bool print = false );
 public:
   /** get number of quantifiers */
   int getNumQuantifiers() { return (int)d_quants.size(); }