Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.

9 files changed, 85 insertions, 22 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 8e6673fb9..1f4d398be 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -39,6 +39,7 @@ d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_v
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
   d_true = NodeManager::currentNM()->mkConst( true );
+  d_is_nested_quant = false;
 }
 
 void CegInstantiator::computeProgVars( Node n ){
@@ -1202,8 +1203,13 @@ void CegInstantiator::processAssertions() {
       //collect all assertions from theory
       for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
         Node lit = (*it).assertion;
-        d_curr_asserts[tid].push_back( lit );
-        Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
+          d_curr_asserts[tid].push_back( lit );
+          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        }else{
+          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
+        }
         if( lit.getKind()==EQUAL ){
           std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
           if( itae!=d_aux_eq.end() ){
@@ -1338,6 +1344,25 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st
   subs_rhs.push_back( r );
 }
 
+void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==FORALL ){
+    d_is_nested_quant = true;
+  }else{
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      if( TermDb::isBoolConnective( n.getKind() ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          collectCeAtoms( n[i], visited );
+        }
+      }else{
+        if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
+          d_ce_atoms.push_back( n );
+        }
+      }
+    }
+  }
+}
+
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
   Assert( d_vars.empty() );
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
@@ -1367,6 +1392,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }
     lems[i] = rlem;
   }
+  //collect atoms from lem[0]: we will only do bounds coming from original body
+  d_is_nested_quant = false;
+  std::map< Node, bool > visited;
+  collectCeAtoms( lems[0], visited );
 }
 
 //old implementation
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9b3b15dc5..9fe938f16 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -65,7 +65,12 @@ private:
   std::map< Node, std::map< Node, Node > > d_aux_eq;
   //the CE variables
   std::vector< Node > d_vars;
+  //atoms of the CE lemma
+  bool d_is_nested_quant;
+  std::vector< Node > d_ce_atoms;
 private:
+  //collect atoms
+  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
   //for adding instantiations during check
   void computeProgVars( Node n );
   //solved form, involves substitution with coefficients
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index b7d82bc9e..9e13ef5eb 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1649,7 +1649,7 @@ void MatchGen::setInvalid() {
 }
 
 bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );
+  return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() );
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 366c7ce07..2c9430876 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1549,6 +1549,10 @@ bool TermDb::isComm( Kind k ) {
          k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
 }
 
+bool TermDb::isBoolConnective( Kind k ) {
+  return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT;
+}
+
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
     d_op_triggers[op].push_back( tr );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 682a9f8e0..1b0b72bf9 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -394,6 +394,8 @@ public:
   static bool isAssoc( Kind k );
   /** is comm */
   static bool isComm( Kind k );
+  /** is bool connective */
+  static bool isBoolConnective( Kind k );
 
 //for sygus
 private:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f1c47a21a..2c2e4ea5b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -298,7 +298,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 }
 
 void QuantifiersEngine::presolve() {
-  Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl;
+  Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
@@ -306,9 +306,11 @@ void QuantifiersEngine::presolve() {
   d_presolve = false;
   //add all terms to database
   if( options::incrementalSolving() ){
+    Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
     for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
       addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
     }
+    Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
   }
 }
 
@@ -558,9 +560,9 @@ bool QuantifiersEngine::registerQuantifier( Node 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 );
-      }
+      //if( options::finiteModelFind() ){
+      //  ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
+      //}
       d_quants[f] = true;
       return true;
     }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 073399894..858761078 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -265,6 +265,9 @@ void TheoryUF::presolve() {
       d_out->lemma(*i);
     }
   }
+  if( d_thss ){
+    d_thss->presolve();
+  }
   Debug("uf") << "uf: end presolve()" << endl;
 }
 
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 2a33b8b36..29e726da7 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -706,6 +706,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
   }
 }
 
+void StrongSolverTheoryUF::SortModel::presolve() {
+  d_initialized = false;
+  d_aloc_cardinality = 0;
+}
+
 void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){
 
 }
@@ -719,11 +724,14 @@ Node StrongSolverTheoryUF::SortModel::getNextDecisionRequest(){
       if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
         Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl;
         return cn;
+      }else{
+        Trace("uf-ss-dec-debug") << "  dec : " << cn << " already asserted " << d_cardinality_assertions[cn].get() << std::endl;
       }
     }
   }
   Trace("uf-ss-dec") << "UFSS : no decisions for " << d_type << "." << std::endl;
   Trace("uf-ss-dec-debug") << "  aloc_cardinality = " << d_aloc_cardinality << ", cardinality = " << d_cardinality << ", hasCard = " << d_hasCard << std::endl;
+  Assert( d_hasCard );
   return Node::null();
 }
 
@@ -834,6 +842,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
   if( !d_conflict ){
     Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = ";
     Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
+    Assert( c>0 );
     Node cl = getCardinalityLiteral( c );
     d_cardinality_assertions[ cl ] = val;
     if( val ){
@@ -878,10 +887,12 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
       if( !d_hasCard ){
         bool needsCard = true;
         for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
-          if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
-            Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
-            needsCard = false;
-            break;
+          if( it->first<=d_aloc_cardinality.get() ){
+            if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
+              Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
+              needsCard = false;
+              break;
+            }
           }
         }
         if( needsCard ){
@@ -1702,6 +1713,14 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
   }
 }
 
+void StrongSolverTheoryUF::presolve() {
+  d_aloc_com_card.set( 0 );
+  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+    it->second->presolve();
+    it->second->initialize( d_out );
+  }
+}
+
 /** propagate */
 void StrongSolverTheoryUF::propagate( Theory::Effort level ){
   //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
@@ -1779,14 +1798,14 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
   }
 }
 
-void StrongSolverTheoryUF::registerQuantifier( Node f ){
-  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
+//void StrongSolverTheoryUF::registerQuantifier( Node f ){
+//  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
   //must ensure the quantifier does not quantify over arithmetic
   //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
   //  TypeNode tn = f[0][i].getType();
   //  preRegisterType( tn, true );
   //}
-}
+//}
 
 
 StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
@@ -1798,15 +1817,10 @@ StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
     it = d_rep_model.find( tn );
   }
   if( it!=d_rep_model.end() ){
-    //initialize the type if necessary
-    //if( d_rep_model_init.find( tn )==d_rep_model_init.end() ){
-      ////initialize the model
-      //it->second->initialize( d_out );
-      //d_rep_model_init[tn] = true;
-    //}
     return it->second;
+  }else{
+    return NULL;
   }
-  return NULL;
 }
 
 void StrongSolverTheoryUF::notifyRestart(){
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 3619a8ba7..3e612ff1f 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -268,6 +268,8 @@ public:
     bool areDisequal( Node a, Node b );
     /** check */
     void check( Theory::Effort level, OutputChannel* out );
+    /** presolve */
+    void presolve();
     /** propagate */
     void propagate( Theory::Effort level, OutputChannel* out );
     /** get next decision request */
@@ -365,6 +367,8 @@ public:
 public:
   /** check */
   void check( Theory::Effort level );
+  /** presolve */
+  void presolve();
   /** propagate */
   void propagate( Theory::Effort level );
   /** get next decision request */
@@ -372,7 +376,7 @@ public:
   /** preregister a term */
   void preRegisterTerm( TNode n );
   /** preregister a quantifier */
-  void registerQuantifier( Node f );
+  //void registerQuantifier( Node f );
   /** notify restart */
   void notifyRestart();
 public: