Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.

6 files changed, 31 insertions, 23 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 98cd175fd..5e4b6828e 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -744,12 +744,14 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
   for( unsigned i=0; i<c.getNumChildren(); i++ ){
     if( c[i].getType().isInteger() ){
       if( fm->isInterval(c[i]) ){
+        Trace("fmc-exh-debug") << "...set " << i << " based on interval." << std::endl;
         for( unsigned b=0; b<2; b++ ){
           if( !fm->isStar(c[i][b]) ){
             riter.d_bounds[b][i] = c[i][b];
           }
         }
       }else if( !fm->isStar(c[i]) ){
+        Trace("fmc-exh-debug") << "...set " << i << " based on point." << std::endl;
         riter.d_bounds[0][i] = c[i];
         riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );
       }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 4b173c833..70ee01b92 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -274,7 +274,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
+      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl;
       if( !riter.d_incomplete ){
         int triedLemmas = 0;
         int addedLemmas = 0;
@@ -299,6 +299,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
     }else{
+      Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl;
       Assert( riter.d_incomplete );
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 4c58aa886..0d7c9352c 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1652,20 +1652,6 @@ bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, boo
   return false;
 }
 
-bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) {
-  if( n.getKind()==UNINTERPRETED_CONSTANT ){
-    return true;
-  }else if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( containsUninterpretedConstant2( n[i], visited ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
 bool TermDb::containsTerm( Node n, Node t ) {
   std::map< Node, bool > visited;
   return containsTerm2( n, t, visited );
@@ -1696,8 +1682,22 @@ int TermDb::getTermDepth( Node n ) {
 }
 
 bool TermDb::containsUninterpretedConstant( Node n ) {
-  std::map< Node, bool > visited;
-  return containsUninterpretedConstant2( n, visited );
+  if (!n.hasAttribute(ContainsUConstAttribute()) ){
+    bool ret = false;
+    if( n.getKind()==UNINTERPRETED_CONSTANT ){
+      ret = true;
+    }else{
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( containsUninterpretedConstant( n[i] ) ){
+          ret = true;
+          break;
+        }
+      }
+    }
+    ContainsUConstAttribute cuca;
+    n.setAttribute(cuca, ret ? 1 : 0);
+  }
+  return n.getAttribute(ContainsUConstAttribute())!=0;
 }
 
 Node TermDb::simpleNegate( Node n ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index fcacbd686..6b8f9c783 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -71,6 +71,9 @@ typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
 struct TermDepthAttributeId {};
 typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
 
+struct ContainsUConstAttributeId {};
+typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
+
 struct ModelBasisAttributeId {};
 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 //for APPLY_UF terms, 1 : term has direct child with model basis attribute,
@@ -429,7 +432,6 @@ private:
   //helper for contains term
   static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
   static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
-  static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited );
 //general utilities
 public:
   /** simple check for whether n contains t as subterm */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 568483380..4be55ebb5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -88,6 +88,9 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
     d_te( te ),
     d_lemmas_produced_c(u),
     d_skolemized(u),
+    //d_ierCounter(c),
+    //d_ierCounter_lc(c),
+    //d_ierCounterLastLc(c),
     d_presolve(u, true),
     d_presolve_in(u),
     d_presolve_cache(u),
@@ -141,7 +144,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
   d_ierCounter_lc = 0;
-  d_ierCounterLastLc = d_ierCounter_lc;
+  d_ierCounterLastLc = 0;
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 }
 
@@ -465,11 +468,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
           if( e==Theory::EFFORT_FULL ){
             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
-              d_ierCounter++;
+              d_ierCounter = d_ierCounter + 1;
               d_ierCounterLastLc = d_ierCounter_lc;
             }
           }else if( e==Theory::EFFORT_LAST_CALL ){
-            d_ierCounter_lc++;
+            d_ierCounter_lc = d_ierCounter_lc + 1;
           }
         }else if( quant_e==QEFFORT_MODEL ){
           if( e==Theory::EFFORT_LAST_CALL ){
@@ -1339,7 +1342,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
   Assert( f.isNull() || f.getKind()==FORALL );
   Node r = getRepresentative( a );
   if( options::finiteModelFind() ){
-    if( r.isConst() ){
+    if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){
       //map back from values assigned by model, if any
       if( d_qe->getModel() ){
         std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0c43223d8..228ac9ee9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -203,7 +203,7 @@ private:
   std::map< Node, int > d_total_inst_debug;
   std::map< Node, int > d_temp_inst_debug;
   int d_total_inst_count_debug;
-  /** inst round counters */
+  /** inst round counters TODO: make context-dependent? */
   int d_ierCounter;
   int d_ierCounter_lc;
   int d_ierCounterLastLc;