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

5 files changed, 43 insertions, 3 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: