Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.

14 files changed, 231 insertions, 167 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index d001684a0..04b6e6813 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -37,11 +37,6 @@ option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false
  aggressive split quantified formulas that lead to variable eliminations
 option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
  split ites with dt testers as conditions
-# Whether to CNF quantifier bodies
-# option cnfQuant --cnf-quant bool :default false
-#  apply CNF conversion to quantified formulas
-option nnfQuant --nnf-quant bool :default true
- apply NNF conversion to quantified formulas
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 98ed9c4fd..784d82228 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -552,6 +552,11 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   unsigned d_simplifyAssertionsDepth;
 
+  /** whether certain preprocess steps are necessary */
+  bool d_needsExpandDefs;
+  bool d_needsRewriteBoolTerms;
+  bool d_needsConstrainSubTypes;
+
 public:
   /**
    * Map from skolem variables to index in d_assertions containing
@@ -679,6 +684,9 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
+    d_needsExpandDefs(true),
+    d_needsRewriteBoolTerms(true),
+    d_needsConstrainSubTypes(true), //TODO
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
@@ -3860,6 +3868,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+
   dumpAssertions("pre-constrain-subtypes", d_assertions);
   {
     // Any variables of subtype types need to be constrained properly.
@@ -4194,6 +4203,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
   dumpAssertions("post-everything", d_assertions);
+  
 
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8123fe39c..f044ff401 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -375,15 +375,23 @@ void TheoryDatatypes::flushPendingFacts(){
         Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
       }else{
         Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
-        Node ee_exp;
+        std::vector< TNode > assumptions;
         //if( options::dtRExplainLemmas() ){
-          ee_exp = explain( exp );
+        explain( exp, assumptions );
         //}else{
         //  ee_exp = exp;
         //}
-        Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
-        lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact );
-        lem = Rewriter::rewrite( lem );
+        //Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
+        if( assumptions.empty() ){
+          lem = fact;
+        }else{
+          std::vector< Node > children;
+          for( unsigned i=0; i<assumptions.size(); i++ ){
+            children.push_back( assumptions[i].negate() );
+          }
+          children.push_back( fact );
+          lem = NodeManager::currentNM()->mkNode( OR, children );
+        }
       }
       Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
       if( doSendLemma( lem ) ){
@@ -1941,14 +1949,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   bool addLemma = false;
   if( options::dtInferAsLemmas() && exp!=d_true ){
     addLemma = true;    
-  }else if( n.getKind()==EQUAL || n.getKind()==IFF ){
-    /*
-    for( unsigned i=0; i<2; i++ ){
-      if( !n[i].isVar() && n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
-        addLemma = true;
-      }
-    }
-    */
+  }else if( n.getKind()==EQUAL ){
     TypeNode tn = n[0].getType();
     if( !DatatypesRewriter::isTypeDatatype( tn ) ){
       addLemma = true;
@@ -1956,15 +1957,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       addLemma = dt.involvesExternalType();
     }
-    //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
-    //  if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
-    //    addLemma = true;
-    //    break;
-    //  }
-    //}
-  }else if( n.getKind()==LEQ ){
-    addLemma = true;
-  }else if( n.getKind()==OR ){
+  }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){
     addLemma = true;
   }
   if( addLemma ){
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 1f68884b6..e5cc34f7e 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -62,6 +62,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
   d_op( op ), d_qe( qe ), d_term_iter( -1 ){
   Assert( !d_op.isNull() );
 }
+
 void CandidateGeneratorQE::resetInstantiationRound(){
   d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
 }
@@ -71,20 +72,20 @@ void CandidateGeneratorQE::reset( Node eqc ){
   if( eqc.isNull() ){
     d_mode = cand_term_db;
   }else{
-    //create an equivalence class iterator in eq class eqc
-    //d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
-
-    eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
-    if( ee->hasTerm( eqc ) ){
-      Node rep = ee->getRepresentative( eqc );
-      d_eqc_iter = eq::EqClassIterator( rep, ee );
-      d_mode = cand_term_eqc;
+    if( isExcludedEqc( eqc ) ){
+      d_mode = cand_term_none;
     }else{
-      d_n = eqc;
-      d_mode = cand_term_ident;
+      eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+      if( ee->hasTerm( eqc ) ){
+        //create an equivalence class iterator in eq class eqc
+        Node rep = ee->getRepresentative( eqc );
+        d_eqc_iter = eq::EqClassIterator( rep, ee );
+        d_mode = cand_term_eqc;
+      }else{
+        d_n = eqc;
+        d_mode = cand_term_ident;
+      }
     }
-    //a should be in its equivalence class
-    //Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
   }
 }
 bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
@@ -98,17 +99,26 @@ bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
 
 Node CandidateGeneratorQE::getNextCandidate(){
   if( d_mode==cand_term_db ){
+    Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
       Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
       d_term_iter++;
       if( isLegalCandidate( n ) ){
         if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
-          return n;
+          if( d_exclude_eqc.empty() ){
+            return n;
+          }else{
+            Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+            if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
+              return n;
+            }
+          }
         }
       }
     }
   }else if( d_mode==cand_term_eqc ){
+    Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
     while( !d_eqc_iter.isFinished() ){
       Node n = *d_eqc_iter;
       ++d_eqc_iter;
@@ -117,6 +127,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
       }
     }
   }else if( d_mode==cand_term_ident ){
+    Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
     if( !d_n.isNull() ){
       Node n = d_n;
       d_n = Node::null();
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index d86891de7..9d8e318aa 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -88,10 +88,12 @@ private:
     cand_term_db,
     cand_term_ident,
     cand_term_eqc,
+    cand_term_none,
   };
   short d_mode;
   bool isLegalOpCandidate( Node n );
   Node d_n;
+  std::map< Node, bool > d_exclude_eqc;
 public:
   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
   ~CandidateGeneratorQE() throw() {}
@@ -99,6 +101,8 @@ public:
   void resetInstantiationRound();
   void reset( Node eqc );
   Node getNextCandidate();
+  void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
+  bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
 };
 
 class CandidateGeneratorQELitEq : public CandidateGenerator
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 41c62192f..7d732ab8a 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -40,7 +40,6 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
   d_match_pattern_type = pat.getType();
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
-  d_eq_class_rel = false;
 }
 
 InstMatchGenerator::InstMatchGenerator() {
@@ -59,7 +58,7 @@ void InstMatchGenerator::setActiveAdd(bool val){
 
 void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
   if( !d_pattern.isNull() ){
-    Debug("inst-match-gen") << "Pattern term is " << d_pattern << std::endl;
+    Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
     if( d_match_pattern.getKind()==NOT ){
       //we want to add the children of the NOT
       d_match_pattern = d_pattern[0];
@@ -67,29 +66,23 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
       //make sure the matching portion of the equality is on the LHS of d_pattern
       //  and record what d_match_pattern is
-      if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){
-        if( d_match_pattern[1].getKind()!=INST_CONSTANT ){
-          Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
-          Node mp = d_match_pattern[1];
-          //swap sides
-          Node pat = d_pattern;
-          if(d_match_pattern.getKind()==GEQ){
-            d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] );
-            d_pattern = d_pattern.negate();
-          }else{
-            d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
-          }
-          d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
-          d_match_pattern = mp;
-        }
-      }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){
-        if( d_match_pattern[0].getKind()!=INST_CONSTANT ){
-          Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
-          if( d_pattern.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
-            d_match_pattern = d_match_pattern[0];
-          }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
-            d_match_pattern = d_match_pattern[0];
+      for( unsigned i=0; i<2; i++ ){
+        if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
+          Node mp = d_match_pattern[1-i];
+          Node mpo = d_match_pattern[i];
+          if( mp.getKind()!=INST_CONSTANT ){
+            if( i==0 ){
+              if( d_match_pattern.getKind()==GEQ ){
+                d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
+                d_pattern = d_pattern.negate();
+              }else{
+                d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
+              }
+            }
+            d_eq_class_rel = mpo;
+            d_match_pattern = mp;
           }
+          break;
         }
       }
     }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT && options::purifyDtTriggers() ){
@@ -100,7 +93,6 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
 
     //now, collect children of d_match_pattern
-    //int childMatchPolicy = MATCH_GEN_DEFAULT;
     for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
       Node qa = quantifiers::TermDb::getInstConstAttr(d_match_pattern[i]);
       if( !qa.isNull() ){
@@ -127,7 +119,15 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     }
 
     //create candidate generator
-    if( d_match_pattern.getKind()==INST_CONSTANT ){
+    if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+      //we will be scanning lists trying to find d_match_pattern.getOperator()
+      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
+      //if matching on disequality, inform the candidate generator not to match on eqc
+      if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
+        ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
+        d_eq_class_rel = Node::null();
+      } 
+    }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
         Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
         size_t selectorIndex = Datatype::cindexOf(selectorExpr);
@@ -140,6 +140,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
     }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+      Assert( d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT );
       //we will be producing candidates via literal matching heuristics
       if( d_pattern.getKind()!=NOT ){
         //candidates will be all equalities
@@ -148,26 +149,6 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
         //candidates will be all disequalities
         d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
       }
-    }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF ||
-              d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){
-      Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
-      if( d_pattern.getKind()==NOT ){
-        if (d_pattern[0][1].getKind()!=INST_CONSTANT) {
-          Unimplemented("Disequal generator unimplemented");
-        }else{
-          d_eq_class = d_pattern[0][1];
-        }
-      }else{
-        //store the equivalence class that we will call d_cg->reset( ... ) on
-        d_eq_class = d_pattern[1];
-      }
-      d_eq_class_rel = true;
-      Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
-      //we are matching only in a particular equivalence class
-      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
-    }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
-      //we will be scanning lists trying to find d_match_pattern.getOperator()
-      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
     }else{
       d_cg = new CandidateGeneratorQueue;
       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
@@ -231,8 +212,8 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
         }
       }
     //for relational matching
-    }else if( d_eq_class_rel && d_eq_class.getKind()==INST_CONSTANT ){
-      int v = d_eq_class.getAttribute(InstVarNumAttribute());
+    }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
+      int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
       //also must fit match to equivalence class
       bool pol = d_pattern.getKind()!=NOT;
       Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
@@ -313,20 +294,22 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
 void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   eqc = qe->getEqualityQuery()->getRepresentative( eqc );
   Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
-  if( !eqc.isNull() ){
+  if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
+    d_eq_class = d_eq_class_rel;
+  }else if( !eqc.isNull() ){
     d_eq_class = eqc;
   }
   //we have a specific equivalence class in mind
   //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
   //just look in equivalence class of the RHS
-  d_cg->reset( d_eq_class_rel ? Node::null() : d_eq_class );
+  d_cg->reset( d_eq_class );
   d_needsReset = false;
 }
 
 bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
-    reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
+    reset( d_eq_class, qe );
   }
   m.d_matched = Node::null();
   Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
@@ -346,7 +329,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
   if( !success ){
     Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
     //we failed, must reset
-    reset( d_eq_class_rel ? Node::null() : d_eq_class, qe );
+    reset( d_eq_class, qe );
   }
   return success;
 }
@@ -696,6 +679,12 @@ int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
 }
 
 InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+    d_eqc = d_match_pattern[1];
+    d_match_pattern = d_match_pattern[0];
+    Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) );
+  }
+  Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
       if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==q ){
@@ -716,9 +705,18 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
   InstMatch m( q );
   m.add( baseMatch );
   int addedLemmas = 0;
-
-  addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_op ]) );
-  return addedLemmas;
+  quantifiers::TermArgTrie* tat;
+  if( d_eqc.isNull() ){
+    tat = qe->getTermDatabase()->getTermArgTrie( d_op );
+  }else{
+    tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+  }
+  if( tat ){
+    addInstantiations( m, qe, addedLemmas, 0, tat );
+    return addedLemmas;
+  }else{
+    return 0;
+  }
 }
 
 void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 75adeb2d8..58531f3e6 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -64,7 +64,7 @@ protected:
   InstMatchGenerator* d_next;
   /** eq class */
   Node d_eq_class;
-  bool d_eq_class_rel;
+  Node d_eq_class_rel;
   /** variable numbers */
   std::map< int, int > d_var_num;
   /** initialize pattern */
@@ -211,6 +211,8 @@ private:
   Node d_f;
   /** match term */
   Node d_match_pattern;
+  /** equivalence class */
+  Node d_eqc;
   /** match pattern arg types */
   std::vector< TypeNode > d_match_pattern_arg_types;
   /** operator */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 111eab116..fac83ec5c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -246,29 +246,32 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     d_patTerms[1][f].clear();
     bool ntrivTriggers = options::relationalTriggers();
     std::vector< Node > patTermsF;
+    std::map< Node, int > reqPol;
     //well-defined function: can assume LHS is only trigger
     if( options::quantFunWellDefined() ){
       Node hd = TermDb::getFunDefHead( f );
       if( !hd.isNull() ){
         hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
         patTermsF.push_back( hd );
+        reqPol[hd] = 0;
       }
     }
     //otherwise, use algorithm for collecting pattern terms
     if( patTermsF.empty() ){
       Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], reqPol, true );
       Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
       if( ntrivTriggers ){
         sortTriggers st;
         std::sort( patTermsF.begin(), patTermsF.end(), st );
       }
       for( unsigned i=0; i<patTermsF.size(); i++ ){
-        Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << std::endl;
+        Assert( reqPol.find( patTermsF[i] )!=reqPol.end() );
+        Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << " " << reqPol[patTermsF[i]] << std::endl;
       }
       Trace("auto-gen-trigger-debug") << std::endl;
     }
-    //sort into single/multi triggers
+    //sort into single/multi triggers, calculate which terms should not be considered
     std::map< Node, std::vector< Node > > varContains;
     std::map< Node, bool > vcMap;
     std::map< Node, bool > rmPatTermsF;
@@ -284,20 +287,34 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       }
       int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
       if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
-        Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
+        Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
         rmPatTermsF[patTermsF[i]] = true;
       }else{
         last_weight = curr_w;
       }
     }
     for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
-      if( rmPatTermsF.find( it->first )==rmPatTermsF.end() ){
-        if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){
-          d_patTerms[0][f].push_back( it->first );
-          d_is_single_trigger[ it->first ] = true;
+      Node pat = it->first;
+      Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+      if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
+        //process the pattern: if it has a required polarity, consider it
+        if( options::instNoEntail() ){
+          Assert( reqPol.find( pat )!=reqPol.end() );
+          int rpol = reqPol[pat];
+          Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << std::endl;
+          if( rpol!=0 ){
+            Assert( pat.getType().isBoolean() );
+            if( pat.getKind()==APPLY_UF ){
+              pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+            }
+          }
+        }
+        if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+          d_patTerms[0][f].push_back( pat );
+          d_is_single_trigger[ pat ] = true;
         }else{
-          d_patTerms[1][f].push_back( it->first );
-          d_is_single_trigger[ it->first ] = false;
+          d_patTerms[1][f].push_back( pat );
+          d_is_single_trigger[ pat ] = false;
         }
       }
     }
@@ -332,7 +349,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         //sort based on # occurrences (this will cause Trigger to select rarer symbols)
         std::sort( patTerms.begin(), patTerms.end(), sqfs );
         Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
-        for( int i=0; i<(int)patTerms.size(); i++ ){
+        for( unsigned i=0; i<patTerms.size(); i++ ){
           Debug("relevant-trigger") << "   " << patTerms[i] << " (";
           Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
         }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 4e7afad5d..04f35a3ed 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -73,6 +73,8 @@ private:
   std::map< Node, int > d_counter;
   /** single, multi triggers for each quantifier */
   std::map< Node, std::vector< Node > > d_patTerms[2];
+  std::map< Node, std::map< Node, bool > > d_patReqPol;
+  /** information about triggers */
   std::map< Node, bool > d_is_single_trigger;
   std::map< Node, bool > d_single_trigger_gen;
   std::map< Node, bool > d_made_multi_trigger;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 1f1efa2a8..eb92b0f70 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -377,3 +377,20 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
     newPol = pol;
   }
 }
+
+void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
+  if( n.getKind()==AND || n.getKind()==OR ){
+    newHasPol = hasPol && pol==( n.getKind()==AND );
+    newPol = pol;
+  }else if( n.getKind()==IMPLIES ){
+    newHasPol = hasPol && !pol;
+    newPol = child==0 ? !pol : pol;
+  }else if( n.getKind()==NOT ){
+    newHasPol = hasPol;
+    newPol = !pol;
+  }else{
+    newHasPol = false;
+    newPol = pol;
+  }
+}
+
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 31743d352..073777014 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -93,6 +93,7 @@ public:
   std::map< Node, Node > d_phase_reqs_equality_term;
 
   static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
+  static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 };
 
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b0340d630..9e0e40911 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -324,7 +324,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else if( isLiteral( body[0] ) ){
       return body;
     }else{
-      std::vector< Node > children;
+      std::vector< Node > children; 
       Kind k = body[0].getKind();
 
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
@@ -1546,7 +1546,7 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_NNF ){
-    return options::nnfQuant();
+    return true;
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index efffe10bd..79c677f1c 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -337,13 +337,19 @@ bool Trigger::isCbqiKind( Kind k ) {
 }
 
 bool Trigger::isSimpleTrigger( Node n ){
-  if( isAtomicTrigger( n ) ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
+  Node t = n;
+  if( n.getKind()==IFF || n.getKind()==EQUAL ){
+    if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){
+      t = n[0];
+    }
+  }
+  if( isAtomicTrigger( t ) ){
+    for( unsigned i=0; i<t.getNumChildren(); i++ ){
+      if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(t[i]) ){
         return false;
       }
     }
-    if( options::purifyDtTriggers() && n.getKind()==APPLY_SELECTOR_TOTAL ){
+    if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
       return false;
     }
     return true;
@@ -352,64 +358,66 @@ bool Trigger::isSimpleTrigger( Node n ){
   }
 }
 
-
-bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
-  if( patMap.find( n )==patMap.end() ){
-    patMap[ n ] = false;
-    if( tstrt==TS_MIN_TRIGGER ){
-      if( n.getKind()==FORALL ){
-        return false;
-      }else{
-        bool retVal = false;
+//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
+bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, int tstrt, std::vector< Node >& exclude, 
+                                std::map< Node, int >& reqPol, bool pol, bool hasPol, bool epol, bool hasEPol ){
+  std::map< Node, bool >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    visited[ n ] = false;
+    Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
+    bool retVal = false;
+    if( n.getKind()!=FORALL ){
+      if( tstrt==TS_MIN_TRIGGER ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           bool newHasPol, newPol;
+          bool newHasEPol, newEPol;
           QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
+          QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
+          if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
             retVal = true;
           }
         }
-        if( retVal ){
-          return true;
-        }else{
+        if( !retVal ){
           Node nu;
           if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
             nu = getIsUsableTrigger( n, f, pol, hasPol );
           }
           if( !nu.isNull() ){
-            patMap[ nu ] = true;
-            return true;
-          }else{
-            return false;
+            reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
+            visited[ nu ] = true;
+            retVal = true;
           }
         }
-      }
-    }else{
-      bool retVal = false;
-      Node nu;
-      if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
-        nu = getIsUsableTrigger( n, f, pol, hasPol );
-      }
-      if( !nu.isNull() ){
-        patMap[ nu ] = true;
-        if( tstrt==TS_MAX_TRIGGER ){
-          return true;
-        }else{
+      }else{
+        Node nu;
+        if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+          nu = getIsUsableTrigger( n, f, pol, hasPol );
+        }
+        bool rec = true;
+        if( !nu.isNull() ){
+          reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
+          visited[ nu ] = true;
           retVal = true;
+          if( tstrt==TS_MAX_TRIGGER ){
+            rec = false;
+          }
         }
-      }
-      if( n.getKind()!=FORALL ){
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          bool newHasPol, newPol;
-          QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
-            retVal = true;
+        if( rec ){
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            bool newHasPol, newPol;
+            bool newHasEPol, newEPol;
+            QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+            QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
+            if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
+              retVal = true;
+            }
           }
         }
       }
-      return retVal;
     }
+    return retVal;
   }else{
-    return patMap[ n ];
+    return itv->second;
   }
 }
 
@@ -493,42 +501,47 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
   return true;
 }
 
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
-  std::map< Node, bool > patMap;
+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, 
+                               std::map< Node, int >& reqPol, bool filterInst ){
+  std::map< Node, bool > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
-    collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false );
+    std::map< Node, int > reqPol2;
+    collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, reqPol2, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
     qe->getTermDatabase()->filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
       Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Trace("trigger-filter-instance") << "Old: ";
-      for( int i=0; i<(int)patTerms2.size(); i++ ){
+      for( unsigned i=0; i<patTerms2.size(); i++ ){
         Trace("trigger-filter-instance") << patTerms2[i] << " ";
       }
       Trace("trigger-filter-instance") << std::endl << "New: ";
-      for( int i=0; i<(int)temp.size(); i++ ){
+      for( unsigned i=0; i<temp.size(); i++ ){
         Trace("trigger-filter-instance") << temp[i] << " ";
       }
       Trace("trigger-filter-instance") << std::endl;
     }
     if( tstrt==TS_ALL ){
-      patTerms.insert( patTerms.begin(), temp.begin(), temp.end() );
+      for( unsigned i=0; i<temp.size(); i++ ){
+        reqPol[temp[i]] = reqPol2[temp[i]];
+        patTerms.push_back( temp[i] );
+      }
       return;
     }else{
       //do not consider terms that have instances
-      for( int i=0; i<(int)patTerms2.size(); i++ ){
+      for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
-          patMap[ patTerms2[i] ] = false;
+          visited[ patTerms2[i] ] = false;
         }
       }
     }
   }
-  collectPatTerms2( f, n, patMap, tstrt, exclude, true, true );
-  for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
-    if( it->second ){
+  collectPatTerms2( f, n, visited, tstrt, exclude, reqPol, true, true, false, true );
+  for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){
+    if( visited[it->first] ){
       patTerms.push_back( it->first );
     }
   }
@@ -611,9 +624,10 @@ Node Trigger::getInversion( Node n, Node x ) {
 
 void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
   std::vector< Node > patTerms;
+  std::map< Node, int > reqPol;
   //collect all patterns from icn
   std::vector< Node > exclude;
-  collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude );
+  collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude, reqPol );
   //collect all variables from all patterns in patTerms, add to t_vars
   for( unsigned i=0; i<patTerms.size(); i++ ){
     qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 2ca2eb55d..22c4e5905 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -100,7 +100,7 @@ class Trigger {
   };
   static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
                                std::vector< Node >& patTerms, int tstrt,
-                               std::vector< Node >& exclude,
+                               std::vector< Node >& exclude, std::map< Node, int >& reqPol,
                                bool filterInst = false );
   /** is usable trigger */
   static bool isUsableTrigger( Node n, Node q );
@@ -140,9 +140,9 @@ private:
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
                                   bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap,
-                                int tstrt, std::vector< Node >& exclude,
-                                bool pol, bool hasPol );
+  static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, 
+                                int tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol,
+                                bool pol, bool hasPol, bool epol, bool hasEPol );
 
   std::vector< Node > d_nodes;