Fix bug related to quantifiers + incremental, thanks John Backes for the bug report. Other minor cleanup.

9 files changed, 53 insertions, 45 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 3cf603100..896cf5dff 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1048,7 +1048,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       vec.push_back( 0 );
       TypeNode tn = n[i].getType();
-      if( TermDb::isClosedEnumerableType( tn ) ){
+      if( getTermDatabase()->isClosedEnumerableType( tn ) ){
         types.push_back( tn );
       }else{
         return;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d076c6510..bb35ac4cd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -418,7 +418,7 @@ bool TermDb::mayComplete( TypeNode tn ) {
   std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
   if( it==d_may_complete.end() ){
     bool mc = false;
-    if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
+    if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
       Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
       Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
       Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
@@ -964,7 +964,19 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
 }
 
 bool TermDb::isClosedEnumerableType( TypeNode tn ) {
-  return !tn.isArray() && !tn.isSort() && !tn.isCodatatype();
+  std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
+  if( it==d_typ_closed_enum.end() ){
+    bool ret = true;
+    if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){
+      ret = false;
+    }else{
+      //TODO: all subfields must be closed enumerable?
+    }
+    d_typ_closed_enum[tn] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
 }
 
 Node TermDb::getFreeVariableForInstConstant( Node n ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index fb80cb8a8..7c136a186 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -279,11 +279,13 @@ private:
   //type enumerators
   std::map< TypeNode, unsigned > d_typ_enum_map;
   std::vector< TypeEnumerator > d_typ_enum;
+  // closed enumerable type cache
+  std::map< TypeNode, bool > d_typ_closed_enum;
 public:
   //get nth term for type
   Node getEnumerateTerm( TypeNode tn, unsigned index );
   //does this type have an enumerator that produces constants that are handled by ground theory solvers
-  static bool isClosedEnumerableType( TypeNode tn );
+  bool isClosedEnumerableType( TypeNode tn );
 
 //miscellaneous
 public:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1a5be5a57..23d46fd40 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -80,7 +80,8 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
 
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
-d_lemmas_produced_c(u){
+d_lemmas_produced_c(u),
+d_skolemized(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( c, u, this );
   d_tr_trie = new inst::TriggerTrie;
@@ -1000,13 +1001,14 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   bool printed = false;
-  for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
+  for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
+    Node q = (*it).first;
     printed = true;
-    out << "Skolem constants of " << it->first << " : " << std::endl;
+    out << "Skolem constants of " << q << " : " << std::endl;
     out << "  ( ";
-    for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
+    for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){
       if( i>0 ){ out << ", "; }
-      out << d_term_db->d_skolem_constants[it->first][i];
+      out << d_term_db->d_skolem_constants[q][i];
     }
     out << " )" << std::endl;
     out << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2658d09f0..cc8baa1c0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -178,7 +178,7 @@ private:
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
   /** quantifiers that have been skolemized */
-  std::map< Node, bool > d_skolemized;
+  BoolMap d_skolemized;
   /** term database */
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 5766a26c1..c4bc94bd2 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -236,35 +236,6 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
   return Node::null();
 }
 
-//FIXME: need to ensure that theory enumerators exist for each sort
-Node TheoryModel::getNewDomainValue( TypeNode tn ){
-  if( tn.isSort() ){
-    return Node::null();
-  }else{
-    TypeEnumerator te(tn);
-    while( !te.isFinished() ){
-      Node r = *te;
-      if(Debug.isOn("getNewDomainValue")) {
-        Debug("getNewDomainValue") << "getNewDomainValue( " << tn << ")" << endl;
-        Debug("getNewDomainValue") << "+ TypeEnumerator gave: " << r << endl;
-        Debug("getNewDomainValue") << "+ d_type_reps are:";
-        for(vector<Node>::const_iterator i = d_rep_set.d_type_reps[tn].begin();
-            i != d_rep_set.d_type_reps[tn].end();
-            ++i) {
-          Debug("getNewDomainValue") << " " << *i;
-        }
-        Debug("getNewDomainValue") << endl;
-      }
-      if( std::find(d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r) ==d_rep_set.d_type_reps[tn].end() ) {
-        Debug("getNewDomainValue") << "+ it's new, so returning " << r << endl;
-        return r;
-      }
-      ++te;
-    }
-    return Node::null();
-  }
-}
-
 /** add substitution */
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
   if( !d_substitutions.hasSubstitution( x ) ){
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 092b5e8c7..e023edadd 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -72,11 +72,6 @@ public:
     *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
     */
   Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
-  /** get new domain value
-    *   This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
-    *   If it cannot find such a node, it returns null.
-    */
-  Node getNewDomainValue( TypeNode tn );
 public:
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index bcd8da228..501e7b2c6 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -40,7 +40,8 @@ BUG_TESTS = \
   quant-fun-proc.smt2 \
   quant-fun-proc-unmacro.smt2 \
   quant-fun-proc-unfd.smt2 \
-  bug654-dd.smt2
+  bug654-dd.smt2 \
+  bug-fmf-fun-skolem.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
new file mode 100644
index 000000000..d5effc083
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --incremental --fmf-fun
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(define-fun-rec sum ((l Lst)) Int (ite (is-nil l) 0 (+ (head l) (sum (tail l)))))
+
+(declare-fun input () Int)
+(declare-fun p () Bool)
+(declare-fun acc () Lst)
+(assert (and (= acc (ite (>= input 0) (cons input nil) nil))
+             (= p (>= (sum acc) 0))))
+
+
+; EXPECT: unsat
+(push 1)
+(assert (not p))
+(check-sat)
+(pop 1)
+
+; EXPECT: unsat
+(push 1)
+(assert (not p))
+(check-sat)
+(pop 1)
+
+