From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 5 May 2016 23:44:47 +0000 (-0500)
Subject: Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant... 
X-Git-Tag: cvc5-1.0.0~6049^2~53
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c87ee73ad3d51c238700f236c18e425b80e8e7ac;p=cvc5.git

Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges.  Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
---

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index c96791aeb..22e326cda 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -24,7 +24,7 @@ int colnum = 1;
 const char *filename = 0;
 FILE *curfile = 0;
 
-//#define USE_HASH_MAPS
+//#define USE_HASH_MAPS  //AJR: deprecated
 
 symmap2 progs;
 std::vector< Expr* > ascHoles;
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index ae0e49531..5cb774fbf 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -34,7 +34,6 @@ bool destroy_progs = false;
     Expr *r = rr;	    \
     int ref = r->data >> 9; \
     ref = ref - 1; \
-    r->debugrefcnt(ref,DEC); \
     if (ref == 0) {  \
       _e = r;		  \
       goto start_destroy; \
@@ -43,6 +42,7 @@ bool destroy_progs = false;
       r->data = (ref << 9) | (r->data & 511); \
   } while(0)
 
+//removed from below "ref = ref -1;":   r->debugrefcnt(ref,DEC);
 
 void Expr::destroy(Expr *_e, bool dec_kids) {
  start_destroy:
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 32a62ab33..5a505a3d9 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -8,9 +8,9 @@
 #include <map>
 #include "chunking_memory_management.h"
 
-#define USE_FLAT_APP
+#define USE_FLAT_APP  //AJR: off deprecated
 #define MARKVAR_32
-#define DEBUG_SYM_NAMES
+//#define DEBUG_SYM_NAMES
 //#define DEBUG_SYMS
 
 // Expr class
@@ -66,7 +66,6 @@ protected:
 
   enum { INC, DEC, CREATE };
   void debugrefcnt(int ref, int what) {
-#ifdef DEBUG_REFCNT
     std::cout << "[";
     debug();
     switch(what) {
@@ -83,10 +82,6 @@ protected:
     char tmp[10];
     sprintf(tmp,"%d",ref);
     std::cout << tmp << "]\n";
-#else
-    (void)ref;
-    (void)what;
-#endif
   }
 
   Expr(int _class, int _op)
@@ -114,14 +109,18 @@ public:
     //   std::cout << " " << ref << std::endl;
     //}
     ref = ref<4194303 ? ref + 1 : ref;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(ref,INC);
+#endif
     data = (ref << 9) | (data & 511);
   }
   static void destroy(Expr *, bool);
   inline void dec(bool dec_kids = true) {
     int ref = getrefcnt();
     ref = ref - 1;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(ref,DEC);
+#endif
     if (ref == 0)
       destroy(this,dec_kids);
     else
@@ -131,10 +130,10 @@ public:
   //must pass statType (the expr representing "type") to this function
   bool isType( Expr* statType );
 
-  inline bool isDatatype() {
+  inline bool isDatatype() const {
     return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
   }
-  inline bool isArithTerm() {
+  inline bool isArithTerm() const {
     return getop() == ADD || getop() == NEG;
   }
 
@@ -188,13 +187,17 @@ public:
   CExpr(int _op) : Expr(CEXPR, _op), kids() {
     kids = new Expr *[1];
     kids[0] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
     kids = new Expr *[2];
     kids[0] = e1;
     kids[1] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2)
     : Expr(CEXPR, _op), kids() {
@@ -202,7 +205,9 @@ public:
     kids[0] = e1;
     kids[1] = e2;
     kids[2] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2, Expr *e3)
     : Expr(CEXPR, _op), kids() {
@@ -211,7 +216,9 @@ public:
     kids[1] = e2;
     kids[2] = e3;
     kids[3] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4)
     : Expr(CEXPR, _op), kids() {
@@ -221,7 +228,9 @@ public:
     kids[2] = e3;
     kids[3] = e4;
     kids[4] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   CExpr(int _op, const std::vector<Expr *> &_kids) 
     : Expr(CEXPR, _op), kids() {
@@ -230,13 +239,17 @@ public:
     for (i = 0; i < iend; i++)
       kids[i] = _kids[i];
     kids[i] = 0;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
 
   // _kids must be null-terminated.
   CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
     (void)dummy;
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
 
   Expr *whr();
@@ -253,7 +266,9 @@ class IntExpr : public Expr {
   }
   IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
     mpz_init_set(n,_n);
+#ifdef DEBUG_REFCNT    
     debugrefcnt(1,CREATE);
+#endif
   }
   IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() {
     mpz_init_set_si( n, _n );
@@ -271,7 +286,9 @@ class RatExpr : public Expr {
   RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
     mpq_init( n );
     mpq_set(n,_n);
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
     mpq_canonicalize( n );
   }
   RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() {
@@ -290,15 +307,19 @@ class SymExpr : public Expr {
     : Expr(theclass, 0), val(0)
   {   
     (void)_s;
+#ifdef DEBUG_REFCNT   
     if (theclass == SYM_EXPR)
       debugrefcnt(1,CREATE);
+#endif
   }
   SymExpr(const SymExpr &e, int theclass = SYM_EXPR) 
     : Expr(theclass, 0), val(0)
   {
     (void)e;
+#ifdef DEBUG_REFCNT   
     if (theclass == SYM_EXPR)
       debugrefcnt(1,CREATE);
+#endif
   }
 #ifdef MARKVAR_32
 private:
@@ -317,12 +338,16 @@ class SymSExpr : public SymExpr {
   SymSExpr(std::string _s, int theclass = SYMS_EXPR) 
     : SymExpr(_s, theclass), s(_s)
   {
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
   SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) 
     : SymExpr(e, theclass), s(e.s)
   { 
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
 };
 
@@ -338,7 +363,9 @@ public:
 #ifdef DEBUG_HOLE_NAMES
     id = next_id++;
 #endif
+#ifdef DEBUG_REFCNT   
     debugrefcnt(1,CREATE);
+#endif
   }
   Expr *val; // may be set during subst(), defeq(), and clone().
 };
diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp
index 80f36e69f..1d8ba5809 100644
--- a/proofs/lfsc_checker/main.cpp
+++ b/proofs/lfsc_checker/main.cpp
@@ -133,6 +133,7 @@ int main(int argc, char **argv) {
   a.files.clear();
 #endif
 
+  std::cout << "Proof checked successfully!" << std::endl << std::endl;
   std::cout << "time = " << (int)clock() - check_time << std::endl;
   std::cout << "sym count = " << SymExpr::symmCount << std::endl;
   std::cout << "marked count = " << Expr::markedCount << std::endl;
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index 8e8c51857..580b54418 100644
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -280,7 +280,34 @@
   	     	   (bbltn (fail bblt))
 	 	   ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry))
 				  	 (bblast_bvadd a' b' carry)))))))
-				
+
+
+(program reverse_help ((x bblt) (acc bblt)) bblt
+(match x
+       (bbltn acc)
+       ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
+
+
+(program reverseb ((x bblt)) bblt
+	 (reverse_help x bbltn))
+
+
+; AJR: use this version?
+;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt
+;(match a
+;  ( bbltn (match b (bbltn bbltn) (default (fail bblt))))
+;  ((bbltc ai a') (match b 
+;       (bbltn (fail bblt))
+;	 	   ((bbltc bi b') 
+;	 	     (let carry' (or (and ai bi) (and (xor ai bi) carry))
+;	 	     (bbltc (xor (xor ai bi) carry)
+;				  	    (bblast_bvadd_2h a' b' carry'))))))))
+
+;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt
+;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit 
+;(let br (reverseb b) ;; from the least significant bit up
+;(let ret (bblast_bvadd_2h ar br carry)
+;  (reverseb ret)))))
 				
 (declare bv_bbl_bvadd (! n mpz
                       (! x (term (BitVec n))
@@ -322,15 +349,6 @@
 			   
 ;; shift add multiplier
 
-(program reverse_help ((x bblt) (acc bblt)) bblt
-(match x
-       (bbltn acc)
-       ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
-
-
-(program reverseb ((x bblt)) bblt
-	 (reverse_help x bbltn))
-
 ;; (program concat ((a bblt) (b bblt)) bblt
 ;;   (match a (bbltn b)
 ;;   	   ((bbltc ai a') (bbltc ai (concat a' b)))))
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a2809bd67..7d41ae862 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -254,15 +254,21 @@ last-call\n\
 const std::string OptionsHandler::s_literalMatchHelp = "\
 Literal match modes currently supported by the --literal-match option:\n\
 \n\
-none (default)\n\
+none \n\
 + Do not use literal matching.\n\
 \n\
-predicate\n\
-+ Consider the phase requirements of predicate literals when applying heuristic\n\
-  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
-  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
-  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
-  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+use (default)\n\
++ Consider phase requirements of triggers conservatively. For example, the\n\
+  trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
+  terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
+  terms in the equivalence class of false. Extends to equality.\n\
+\n\
+agg-predicate \n\
++ Consider phase requirements aggressively for predicates. In the above example,\n\
+  only match P( x ) with terms that are in the equivalence class of false.\n\
+\n\
+agg \n\
++ Consider the phase requirements aggressively for all triggers.\n\
 \n\
 ";
 
@@ -506,10 +512,12 @@ void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::
 theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg ==  "none") {
     return theory::quantifiers::LITERAL_MATCH_NONE;
-  } else if(optarg ==  "predicate") {
-    return theory::quantifiers::LITERAL_MATCH_PREDICATE;
-  } else if(optarg ==  "equality") {
-    return theory::quantifiers::LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "use") {
+    return theory::quantifiers::LITERAL_MATCH_USE;
+  } else if(optarg ==  "agg-predicate") {
+    return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
+  } else if(optarg ==  "agg") {
+    return theory::quantifiers::LITERAL_MATCH_AGG;
   } else if(optarg ==  "help") {
     puts(s_literalMatchHelp.c_str());
     exit(1);
@@ -520,9 +528,7 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s
 }
 
 void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
-  if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) {
-    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
-  }
+
 }
 
 theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index a58120974..e2cd78de5 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -46,11 +46,14 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
   case theory::quantifiers::LITERAL_MATCH_NONE:
     out << "LITERAL_MATCH_NONE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
-    out << "LITERAL_MATCH_PREDICATE";
+  case theory::quantifiers::LITERAL_MATCH_USE:
+    out << "LITERAL_MATCH_USE";
     break;
-  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
-    out << "LITERAL_MATCH_EQUALITY";
+  case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE:
+    out << "LITERAL_MATCH_AGG_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_AGG:
+    out << "LITERAL_MATCH_AGG";
     break;
   default:
     out << "LiteralMatchMode!UNKNOWN";
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 5749da972..b4b9abdaf 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -44,10 +44,12 @@ enum InstWhenMode {
 enum LiteralMatchMode {
   /** Do not consider polarity of patterns */
   LITERAL_MATCH_NONE,
-  /** Consider polarity of boolean predicates only */
-  LITERAL_MATCH_PREDICATE,
-  /** Consider polarity of boolean predicates, as well as equalities */
-  LITERAL_MATCH_EQUALITY,
+  /** Conservatively consider polarity of patterns */
+  LITERAL_MATCH_USE,
+  /** Aggressively consider polarity of Boolean predicates */
+  LITERAL_MATCH_AGG_PREDICATE,
+  /** Aggressively consider polarity of all terms */
+  LITERAL_MATCH_AGG,
 };
 
 enum MbqiMode {
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f69a8df8b..9fef0295e 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -120,7 +120,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
 option fullSaturateInst --fs-inst bool :default false
  interleave full saturate instantiation with other techniques
 
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
  choose literal matching mode
 
 ### finite model finding options
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 38163c579..c28d23eac 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
         Debug("parser-sygus") << "...constructed exists " << body << std::endl;   
       }
-      body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      if( !PARSER_STATE->getSygusFunSymbols().empty() ){
+        body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      }
       Debug("parser-sygus") << "...constructed forall " << body << std::endl;   
       Command* c = new SetUserAttributeCommand("sygus", sygusVar);
       c->setMuted(true);
@@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
   std::string sname;
   std::vector< Expr > let_vars;
   bool readingLet = false;
+  std::string s;
 }
   : LPAREN_TOK
     //read operator
@@ -890,6 +893,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
       sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
       sgt.d_gterm_type = SygusGTerm::gterm_op;
     }
+  | str[s,false]
+    { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl;
+      sgt.d_expr = MK_CONST( ::CVC4::String(s) );
+      sgt.d_name = s;
+      sgt.d_gterm_type = SygusGTerm::gterm_op;
+    }
   | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
     { if( readEnum ){
         name = name + "__Enum__" + name2;
@@ -2773,7 +2782,7 @@ STRING_LITERAL_2_0
  * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL_2_5
-  : { PARSER_STATE->v2_5() }?=>
+  : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
     '"' (~('"') | '""')* '"'
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ebad90583..2da44152a 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -350,6 +350,8 @@ void Smt2::setLogic(std::string name) {
       name = "UFLIRA";
     } else if(name == "BV") {
       name = "UFBV";
+    } else if(name == "SLIA") {
+      name = "UFSLIA";
     } else if(name == "ALL_SUPPORTED") {
       //no change
     } else {
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index fa71f0132..f4eb67d74 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1572,7 +1572,6 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         if( d_match_status_child_num==0 ){
           //initial binding
           TNode f = s->getTgFunc( d_typ, d_status_num );
-          //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
           Assert( !eqc.isNull() );
           TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
           if( tat ){
@@ -1726,9 +1725,9 @@ void TermGenEnv::collectSignatureInformation() {
   d_func_kind.clear();
   d_func_args.clear();
   TypeNode tnull;
-  for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
-    if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){
-      Node nn = getTermDatabase()->getGroundTerm( it->first, 0 );
+  for( std::map< Node, std::vector< Node > >::iterator it = getTermDatabase()->d_op_map.begin(); it != getTermDatabase()->d_op_map.end(); ++it ){
+    if( !it->second.empty() ){
+      Node nn = it->second[0];
       Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
         bool do_enum = true;
@@ -1750,7 +1749,7 @@ void TermGenEnv::collectSignatureInformation() {
           d_typ_tg_funcs[nn.getType()].push_back( it->first );
           d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );
           Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
-          getTermDatabase()->computeUfEqcTerms( it->first );
+          //getTermDatabase()->computeUfEqcTerms( it->first );
         }
       }
       Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 1dc6f6d50..41c9c40c8 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -34,6 +34,7 @@ bool EqualityQueryInstProp::reset( Theory::Effort e ) {
   d_uf.clear();
   d_uf_exp.clear();
   d_diseq_list.clear();
+  d_uf_func_map_trie.clear();
   return true;
 }
 
@@ -103,7 +104,7 @@ TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& arg
   if( !t.isNull() ){
     return t;
   }else{
-    return d_func_map_trie[f].existsTerm( args );
+    return d_uf_func_map_trie[f].existsTerm( args );
   }
 }
 
@@ -168,6 +169,21 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >&
   }
 }
 
+TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ) {
+  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
+  if( !t.isNull() ){
+    return t;
+  }else{
+    TNode tt = d_uf_func_map_trie[f].existsTerm( args );
+    if( !tt.isNull() ){
+      //TODO?
+      return tt;
+    }else{
+      return tt;
+    }
+  }
+}
+
 Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
   Assert( exp.empty() );
   std::map< Node, Node >::iterator it = d_uf.find( a );
@@ -279,11 +295,13 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
       Assert( d_uf_exp[ar].empty() );
       Assert( d_uf_exp[br].empty() );
 
+      //registerUfTerm( ar );
       d_uf[ar] = br;
       merge_exp( d_uf_exp[ar], exp_a );
       merge_exp( d_uf_exp[ar], exp_b );
       merge_exp( d_uf_exp[ar], reason );
 
+      //registerUfTerm( br );
       d_uf[br] = br;
       d_uf_exp[br].clear();
 
@@ -316,6 +334,25 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
   }
 }
 
+void EqualityQueryInstProp::registerUfTerm( TNode n ) {
+  if( d_uf.find( n )==d_uf.end() ){
+    if( !getEngine()->hasTerm( n ) ){
+      TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+      if( !f.isNull() ){
+        std::vector< TNode > args;
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( !getEngine()->hasTerm( n[i] ) ){
+            return;
+          }else{
+            args.push_back( n[i] );
+          }
+        }
+        d_uf_func_map_trie[f].addTerm( n, args );
+      }
+    }
+  }
+}
+
 //void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
 void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) {
   if( is_watch ){
@@ -573,6 +610,7 @@ bool InstPropagator::reset( Theory::Effort e ) {
   d_watch_list.clear();
   d_update_list.clear();
   d_relevant_inst.clear();
+  d_has_relevant_inst = false;
   return d_qy.reset( e );
 }
 
@@ -607,7 +645,31 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st
     return !d_conflict;
   }else{
     Assert( false );
-    return true;
+    return false;
+  }
+}
+
+void InstPropagator::filterInstantiations() {
+  if( d_has_relevant_inst ){
+    //now, inform quantifiers engine which instances should be retracted
+    Trace("qip-prop-debug") << "...remove instantiation ids : ";
+    for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
+      if( !it->second.d_q.isNull() ){
+        if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
+          if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+            Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
+            Assert( false );
+          }else{
+            Trace("qip-prop-debug") << it->first << " ";
+          }
+        }else{
+          //mark the quantified formula as relevant
+          d_qe->markRelevant( it->second.d_q );
+        }
+      }
+    }
+    Trace("qip-prop-debug") << std::endl;
+    Trace("quant-engine-conflict") << "-----> InstPropagator::" << ( d_conflict ? "conflict" : "propagate" ) << " with " << d_relevant_inst.size() << " instances." << std::endl;
   }
 }
 
@@ -720,10 +782,12 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e
   }
   if( pol ){
     if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
+      Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl;
       Assert( d_qy.getEngine()->hasTerm( a ) );
       Assert( d_qy.getEngine()->hasTerm( b ) );
       Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
       addRelevantInstances( exp, "qip-propagate" );
+      //d_has_relevant_inst = true;
     }
     Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl;
     for( unsigned i=0; i<2; i++ ){
@@ -750,27 +814,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
   d_conflict = true;
   d_relevant_inst.clear();
   addRelevantInstances( exp, "qip-propagate" );
-
-  //now, inform quantifiers engine which instances should be retracted
-  Trace("qip-prop-debug") << "...remove instantiation ids : ";
-  for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
-    if( !it->second.d_q.isNull() ){
-      if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
-        if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
-          Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
-          Assert( false );
-        }else{
-          Trace("qip-prop-debug") << it->first << " ";
-        }
-      }else{
-        //mark the quantified formula as relevant
-        d_qe->markRelevant( it->second.d_q );
-      }
-    }
-  }
-  Trace("qip-prop-debug") << std::endl;
-  //will interupt the quantifiers engine
-  Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl;
+  d_has_relevant_inst = true;
 }
 
 bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 61aa8257f..6201cf152 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -64,9 +64,11 @@ public:
   bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
   /** returns true is a and b are disequal in the current context */
   bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+  /** get congruent term */
+  TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
 private:
   /** term index */
-  std::map< Node, TermArgTrie > d_func_map_trie;
+  std::map< Node, TermArgTrie > d_uf_func_map_trie;
   /** union find for terms beyond what is stored in equality engine */
   std::map< Node, Node > d_uf;
   std::map< Node, std::vector< Node > > d_uf_exp;
@@ -75,6 +77,8 @@ private:
   std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
   /** add arg */
   void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
+  /** register term */
+  void registerUfTerm( TNode n );
 public:
   enum {
     STATUS_CONFLICT,
@@ -110,10 +114,13 @@ private:
     virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
       return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
+    virtual void filterInstantiations() { d_ip.filterInstantiations(); }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
   bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  /** remove instance ids */
+  void filterInstantiations();  
   /** allocate instantiation */
   unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
   /** equality query */
@@ -142,6 +149,7 @@ private:
   std::vector< unsigned > d_update_list;
   /** relevant instances */
   std::map< unsigned, bool > d_relevant_inst;
+  bool d_has_relevant_inst;
 private:
   bool update( unsigned id, InstInfo& i, bool firstTime = false );
   void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index d58bbcf3a..7bc51dc50 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -332,19 +332,30 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         unsigned num_fv = tinfo[pat].d_fv.size();
         Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
         if( rpol!=0 ){
+          Assert( rpol==1 || rpol==-1 );
           if( Trigger::isRelationalTrigger( pat ) ){
             pat = rpol==-1 ? pat.negate() : pat;
           }else{
             Assert( Trigger::isAtomicTrigger( pat ) );
             if( pat.getType().isBoolean() && rpoleq.isNull() ){
-              pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+              if( options::literalMatchMode()==LITERAL_MATCH_USE ){
+                pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+              }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+                pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
+              }
             }else{
               Assert( !rpoleq.isNull() );
               if( rpol==-1 ){
-                //all equivalence classes except rpoleq
-                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+                if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+                  //all equivalence classes except rpoleq
+                  pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+                }
               }else if( rpol==1 ){
-                //all equivalence classes that are not disequal to rpoleq TODO
+                if( options::literalMatchMode()==LITERAL_MATCH_AGG ){
+                  //only equivalence class rpoleq
+                  pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
+                }
+                //all equivalence classes that are not disequal to rpoleq TODO?
               }
             }
           }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 52563978f..1365feda9 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -119,7 +119,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
     //}
     //get all variables that are always relevant
     std::map< TNode, bool > visited;
-    getPropagateVars( vars, q[1], false, visited );
+    getPropagateVars( p, vars, q[1], false, visited );
     for( unsigned j=0; j<vars.size(); j++ ){
       Node v = vars[j];
       TNode f = p->getTermDatabase()->getMatchOperator( v );
@@ -140,7 +140,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   }
 }
 
-void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
   std::map< TNode, bool >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
     visited[n] = true;
@@ -149,6 +149,12 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol,
     if( d_var_num.find( n )!=d_var_num.end() ){
       Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
       vars.push_back( n );
+      TNode f = p->getTermDatabase()->getMatchOperator( n );
+      if( !f.isNull() ){
+        if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){
+          p->d_func_rel_dom[f].push_back( d_q );
+        }
+      } 
     }else if( MatchGen::isHandledBoolConnective( n ) ){
       Assert( n.getKind()!=IMPLIES );
       QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
@@ -156,7 +162,7 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol,
     Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
     if( rec ){
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        getPropagateVars( vars, n[i], pol, visited );
+        getPropagateVars( p, vars, n[i], pol, visited );
       }
     }
   }
@@ -238,7 +244,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
 }
 
 
-void QuantInfo::reset_round( QuantConflictFind * p ) {
+bool QuantInfo::reset_round( QuantConflictFind * p ) {
   for( unsigned i=0; i<d_match.size(); i++ ){
     d_match[i] = TNode::null();
     d_match_term[i] = TNode::null();
@@ -246,6 +252,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
   d_vars_set.clear();
   d_curr_var_deq.clear();
   d_tconstraints.clear();
+  
   //add built-in variable constraints
   for( unsigned r=0; r<2; r++ ){
     for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
@@ -263,7 +270,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
           d_mg->d_children.clear();
           d_mg->d_n = NodeManager::currentNM()->mkConst( true );
           d_mg->d_type = MatchGen::typ_ground;
-          return;
+          return false;
         }
       }
     }
@@ -274,6 +281,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
   }
   //now, reset for matching
   d_mg->reset( p, false, this );
+  return true;
 }
 
 int QuantInfo::getCurrentRepVar( int v ) {
@@ -1283,11 +1291,14 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }
   }else if( d_type==typ_var ){
     Assert( isHandledUfTerm( d_n ) );
-    Node f = getMatchOperator( p, d_n );
+    TNode f = getMatchOperator( p, d_n );
     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
     TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
     if( qni!=NULL ){
       d_qn.push_back( qni );
+    }else{
+      //inform irrelevant quantifiers
+      p->setIrrelevantFunction( f );
     }
     d_matched_basis = false;
   }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
@@ -2013,6 +2024,18 @@ void QuantConflictFind::reset_round( Theory::Effort level ) {
   d_needs_computeRelEqr = true;
 }
 
+void QuantConflictFind::setIrrelevantFunction( TNode f ) {
+  if( d_irr_func.find( f )==d_irr_func.end() ){
+    d_irr_func[f] = true;
+    std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f );
+    if( it != d_func_rel_dom.end()){
+      for( unsigned j=0; j<it->second.size(); j++ ){
+        d_irr_quant[it->second[j]] = true;
+      }
+    }
+  }
+}
+
 /** check */
 void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
@@ -2035,14 +2058,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
       }
       computeRelevantEqr();
 
-      //determine order for quantified formulas
-      std::vector< Node > qorder;
-      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
-        if( d_quantEngine->hasOwnership( q, this ) ){
-          qorder.push_back( q );
-        }
-      }
+      d_irr_func.clear();
+      d_irr_quant.clear();
+
       if( Trace.isOn("qcf-debug") ){
         Trace("qcf-debug") << std::endl;
         debugPrint("qcf-debug");
@@ -2053,80 +2071,83 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
       for( short e = effort_conflict; e<=end_e; e++ ){
         d_effort = e;
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
-        for( unsigned j=0; j<qorder.size(); j++ ){
-          Node q = qorder[j];
-          QuantInfo * qi = &d_qinfo[q];
-
-          Assert( d_qinfo.find( q )!=d_qinfo.end() );
-          if( qi->matchGeneratorIsValid() ){
-            Trace("qcf-check") << "Check quantified formula ";
-            debugPrintQuant("qcf-check", q);
-            Trace("qcf-check") << " : " << q << "..." << std::endl;
-
-            Trace("qcf-check-debug") << "Reset round..." << std::endl;
-            qi->reset_round( this );
-            //try to make a matches making the body false
-            Trace("qcf-check-debug") << "Get next match..." << std::endl;
-            while( qi->getNextMatch( this ) ){
-              Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
-              qi->debugPrintMatch("qcf-inst");
-              Trace("qcf-inst") << std::endl;
-              if( !qi->isMatchSpurious( this ) ){
-                std::vector< int > assigned;
-                if( qi->completeMatch( this, assigned ) ){
-                  std::vector< Node > terms;
-                  qi->getMatch( terms );
-                  bool tcs = qi->isTConstraintSpurious( this, terms );
-                  if( !tcs ){
-                    //for debugging
-                    if( Debug.isOn("qcf-check-inst") ){
-                      Node inst = d_quantEngine->getInstantiation( q, terms );
-                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                      Assert( !getTermDatabase()->isEntailed( inst, true ) );
-                      Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
-                    }
-                    if( d_quantEngine->addInstantiation( q, terms ) ){
-                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                      Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
-                      qi->debugPrintMatch("qcf-inst");
-                      Trace("qcf-inst") << std::endl;
-                      ++addedLemmas;
-                      if( e==effort_conflict ){
-                        d_quantEngine->markRelevant( q );
-                        ++(d_statistics.d_conflict_inst);
-                        if( options::qcfAllConflict() ){
-                          isConflict = true;
+        for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+          Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+          if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){
+            QuantInfo * qi = &d_qinfo[q];
+
+            Assert( d_qinfo.find( q )!=d_qinfo.end() );
+            if( qi->matchGeneratorIsValid() ){
+              Trace("qcf-check") << "Check quantified formula ";
+              debugPrintQuant("qcf-check", q);
+              Trace("qcf-check") << " : " << q << "..." << std::endl;
+
+              Trace("qcf-check-debug") << "Reset round..." << std::endl;
+              if( qi->reset_round( this ) ){
+                //try to make a matches making the body false
+                Trace("qcf-check-debug") << "Get next match..." << std::endl;
+                while( qi->getNextMatch( this ) ){
+                  Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+                  qi->debugPrintMatch("qcf-inst");
+                  Trace("qcf-inst") << std::endl;
+                  if( !qi->isMatchSpurious( this ) ){
+                    std::vector< int > assigned;
+                    if( qi->completeMatch( this, assigned ) ){
+                      std::vector< Node > terms;
+                      qi->getMatch( terms );
+                      bool tcs = qi->isTConstraintSpurious( this, terms );
+                      if( !tcs ){
+                        //for debugging
+                        if( Debug.isOn("qcf-check-inst") ){
+                          Node inst = d_quantEngine->getInstantiation( q, terms );
+                          Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+                          Assert( !getTermDatabase()->isEntailed( inst, true ) );
+                          Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
+                        }
+                        if( d_quantEngine->addInstantiation( q, terms ) ){
+                          Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+                          Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
+                          qi->debugPrintMatch("qcf-inst");
+                          Trace("qcf-inst") << std::endl;
+                          ++addedLemmas;
+                          if( e==effort_conflict ){
+                            d_quantEngine->markRelevant( q );
+                            ++(d_statistics.d_conflict_inst);
+                            if( options::qcfAllConflict() ){
+                              isConflict = true;
+                            }else{
+                              d_conflict.set( true );
+                            }
+                            break;
+                          }else if( e==effort_prop_eq ){
+                            d_quantEngine->markRelevant( q );
+                            ++(d_statistics.d_prop_inst);
+                          }
                         }else{
-                          d_conflict.set( true );
+                          Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
+                          //this should only happen if the algorithm generates the same propagating instance twice this round
+                          //in this case, break to avoid exponential behavior
+                          break;
                         }
-                        break;
-                      }else if( e==effort_prop_eq ){
-                        d_quantEngine->markRelevant( q );
-                        ++(d_statistics.d_prop_inst);
+                      }else{
+                        Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
                       }
+                      //clean up assigned
+                      qi->revertMatch( this, assigned );
+                      d_tempCache.clear();
                     }else{
-                      Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
-                      //this should only happen if the algorithm generates the same propagating instance twice this round
-                      //in this case, break to avoid exponential behavior
-                      break;
+                      Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
                     }
                   }else{
-                    Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
+                    Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
                   }
-                  //clean up assigned
-                  qi->revertMatch( this, assigned );
-                  d_tempCache.clear();
-                }else{
-                  Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
                 }
-              }else{
-                Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
+                Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
+                if( d_conflict ){
+                  break;
+                }
               }
             }
-            Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
-            if( d_conflict ){
-              break;
-            }
           }
         }
         if( addedLemmas>0 ){
@@ -2157,17 +2178,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
 void QuantConflictFind::computeRelevantEqr() {
   if( d_needs_computeRelEqr ){
     d_needs_computeRelEqr = false;
-    Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
-    //d_uf_terms.clear();
-    //d_eqc_uf_terms.clear();
+    Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
     d_eqcs.clear();
-    //d_arg_reps.clear();
-    //double clSet = 0;
-    //if( Trace.isOn("qcf-opt") ){
-    //  clSet = double(clock())/double(CLOCKS_PER_SEC);
-    //}
 
-    //now, store matches
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
     while( !eqcs_i.isFinished() ){
       Node r = (*eqcs_i);
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 16f6b6a1b..974495269 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -117,7 +117,7 @@ private: //for completing match
   std::vector< int > d_una_eqc_count;
   //optimization: track which arguments variables appear under UF terms in
   std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
-  void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
+  void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
   //optimization: number of variables set, to track when we can stop
   std::map< int, bool > d_vars_set;
   std::map< Node, bool > d_ground_terms;
@@ -156,7 +156,7 @@ public:
   }
 
   Node d_q;
-  void reset_round( QuantConflictFind * p );
+  bool reset_round( QuantConflictFind * p );
 public:
   //initialize
   void initialize( QuantConflictFind * p, Node q, Node qn );
@@ -195,6 +195,11 @@ private:
   std::map< Kind, Node > d_zero;
   //for storing nodes created during t-constraint solving (prevents memory leaks)
   std::vector< Node > d_tempCache;
+  //optimization: list of quantifiers that depend on ground function applications
+  std::map< TNode, std::vector< Node > > d_func_rel_dom;
+  std::map< TNode, bool > d_irr_func;
+  std::map< Node, bool > d_irr_quant;
+  void setIrrelevantFunction( TNode f );
 private:
   std::map< Node, Node > d_op_node;
   int d_fid_count;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2f7864831..6963f7e62 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -187,7 +187,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
     std::vector< Node > args;
     Node body = in;
     bool doRewrite = false;
-    bool firstTime = true;
     while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){
       for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
         args.push_back( body[0][i] );
@@ -197,8 +196,11 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
     }
     if( doRewrite ){
       std::vector< Node > children;
+      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
+        args.push_back( body[0][i] );
+      }      
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
-      children.push_back( body );
+      children.push_back( body[1] );
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b143286cc..61c02d3ac 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -163,6 +163,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
         //if this is an atomic trigger, consider adding it
         if( inst::Trigger::isAtomicTrigger( n ) ){
           Trace("term-db") << "register term in db " << n << std::endl;
+          if( options::finiteModelFind() ){
+            computeModelBasisArgAttribute( n );
+          }
+          
           Node op = getMatchOperator( n );
           d_op_map[op].push_back( n );
           added.insert( n );
@@ -222,7 +226,86 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   }
 }
 
+void TermDb::computeUfTerms( TNode f ) {
+  if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){
+    d_op_nonred_count[ f ] = 0;
+    std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
+    if( it!=d_op_map.end() ){
+      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        //to be added to term index, term must be relevant, and exist in EE
+        if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+          if( isTermActive( n ) ){
+            computeArgReps( n );
+
+            Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+            for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+              Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+              if( std::find( d_func_map_rel_dom[f][i].begin(), 
+                             d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){
+                d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] );
+              }
+            }
+            Trace("term-db-debug") << std::endl;
+            Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+            Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] );
+            Trace("term-db-debug2") << "...add term returned " << at << std::endl;
+            if( at!=n && ee->areEqual( at, n ) ){
+              setTermInactive( n );
+              Trace("term-db-debug") << n << " is redundant." << std::endl;
+              //congruentCount++;
+            }else{
+              if( at!=n && ee->areDisequal( at, n, false ) ){
+                std::vector< Node > lits;
+                lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+                for( unsigned i=0; i<at.getNumChildren(); i++ ){
+                  if( at[i]!=n[i] ){
+                    lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+                  }
+                }
+                Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
+                if( Trace.isOn("term-db-lemma") ){
+                  Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
+                  if( !d_quantEngine->getTheoryEngine()->needCheck() ){
+                    Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
+                  }
+                  Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
+                }
+                d_quantEngine->addLemma( lem );
+                d_consistent_ee = false;
+                return;
+              }
+              //nonCongruentCount++;
+              d_op_nonred_count[ f ]++;
+            }
+          }else{
+            Trace("term-db-debug") << n << " is already redundant." << std::endl;
+            //congruentCount++;
+            //alreadyCongruentCount++;
+          }
+        }else{
+          Trace("term-db-debug") << n << " is not relevant." << std::endl;
+          //nonRelevantCount++;
+        }
+      }
+      
+      /*
+      if( Trace.isOn("term-db-index") ){
+        Trace("term-db-index") << "Term index for " << f << " : " << std::endl;
+        Trace("term-db-index") << "- " << it->first << std::endl;
+        d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]);
+        Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = ";
+        Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; 
+      }
+      */
+    }
+  }
+}
+
 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+  computeUfTerms( f );
   Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
@@ -584,10 +667,10 @@ void TermDb::presolve() {
 }
 
 bool TermDb::reset( Theory::Effort effort ){
-  int nonCongruentCount = 0;
-  int congruentCount = 0;
-  int alreadyCongruentCount = 0;
-  int nonRelevantCount = 0;
+  //int nonCongruentCount = 0;
+  //int congruentCount = 0;
+  //int alreadyCongruentCount = 0;
+  //int nonRelevantCount = 0;
   d_op_nonred_count.clear();
   d_arg_reps.clear();
   d_func_map_trie.clear();
@@ -642,71 +725,16 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
 
+/*
   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-    d_op_nonred_count[ it->first ] = 0;
-    Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
-    for( unsigned i=0; i<it->second.size(); i++ ){
-      Node n = it->second[i];
-      //to be added to term index, term must be relevant, and exist in EE
-      if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
-        if( isTermActive( n ) ){
-          if( options::finiteModelFind() ){
-            computeModelBasisArgAttribute( n );
-          }
-          computeArgReps( n );
-
-          Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
-          for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
-            Trace("term-db-debug") << d_arg_reps[n][i] << " ";
-            if( std::find( d_func_map_rel_dom[it->first][i].begin(), 
-                           d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){
-              d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] );
-            }
-          }
-          Trace("term-db-debug") << std::endl;
-          Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
-          Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
-          Trace("term-db-debug2") << "...add term returned " << at << std::endl;
-          if( at!=n && ee->areEqual( at, n ) ){
-            setTermInactive( n );
-            Trace("term-db-debug") << n << " is redundant." << std::endl;
-            congruentCount++;
-          }else{
-            if( at!=n && ee->areDisequal( at, n, false ) ){
-              std::vector< Node > lits;
-              lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
-              for( unsigned i=0; i<at.getNumChildren(); i++ ){
-                if( at[i]!=n[i] ){
-                  lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
-                }
-              }
-              Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
-              if( Trace.isOn("term-db-lemma") ){
-                Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
-                if( !d_quantEngine->getTheoryEngine()->needCheck() ){
-                  Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
-                }
-                Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
-              }
-              d_quantEngine->addLemma( lem );
-              d_consistent_ee = false;
-              return false;
-            }
-            nonCongruentCount++;
-            d_op_nonred_count[ it->first ]++;
-          }
-        }else{
-          Trace("term-db-debug") << n << " is already redundant." << std::endl;
-          congruentCount++;
-          alreadyCongruentCount++;
-        }
-      }else{
-        Trace("term-db-debug") << n << " is not relevant." << std::endl;
-        nonRelevantCount++;
-      }
+    computeUfTerms( it->first );
+    if( !d_consistent_ee ){
+      return false;
     }
   }
+*/  
+  /*
   Trace("term-db-stats") << "TermDb: Reset" << std::endl;
   Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
   Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
@@ -719,10 +747,12 @@ bool TermDb::reset( Theory::Effort effort ){
       }
     }
   }
+  */
   return true;
 }
 
 TermArgTrie * TermDb::getTermArgTrie( Node f ) {
+  computeUfTerms( f );
   std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
   if( itut!=d_func_map_trie.end() ){
     return &itut->second;
@@ -751,11 +781,18 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
 }
 
 TNode TermDb::getCongruentTerm( Node f, Node n ) {
-  computeArgReps( n );
-  return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
+  computeUfTerms( f );
+  std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+  if( itut!=d_func_map_trie.end() ){
+    computeArgReps( n );
+    return itut->second.existsTerm( d_arg_reps[n] );
+  }else{
+    return TNode::null();
+  }
 }
 
 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+  computeUfTerms( f );
   return d_func_map_trie[f].existsTerm( args );
 }
 
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 004292622..684b6cf83 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -248,6 +248,8 @@ public:
   void computeArgReps( TNode n );
   /** compute uf eqc terms */
   void computeUfEqcTerms( TNode f );
+  /** compute uf terms */
+  void computeUfTerms( TNode f );
   /** in relevant domain */
   bool inRelevantDomain( TNode f, unsigned i, TNode r );
   /** evaluate a term under a substitution.  Return representative in EE if possible.
@@ -271,7 +273,7 @@ public:
   Node getEligibleTermInEqc( TNode r );
   /** is inst closure */
   bool isInstClosure( Node r );
-
+  
 //for model basis
 private:
   //map from types to model basis terms
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2451036f1..12edb5277 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -353,7 +353,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
-    for( int i=0; i<(int)d_modules.size(); i++ ){
+    for( unsigned i=0; i<d_modules.size(); i++ ){
       if( d_modules[i]->needsCheck( e ) ){
         qm.push_back( d_modules[i] );
         needsCheck = true;
@@ -396,6 +396,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
       } 
       d_recorded_inst.clear();
     }
+    
+    double clSet = 0;
+    if( Trace.isOn("quant-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
+    }
 
     if( Trace.isOn("quant-engine-debug") ){
       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -456,7 +462,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     flushLemmas();
     if( d_hasAddedLemma ){
       return;
-
     }
 
     if( e==Theory::EFFORT_LAST_CALL ){
@@ -548,6 +553,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
         }
       }
     }
+    if( Trace.isOn("quant-engine") ){
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
+      Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
+      Trace("quant-engine") << std::endl;
+    }
+    
     Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
   }else{
     Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
@@ -567,7 +579,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
     if( setIncomplete ){
-      Trace("quant-engine-debug") << "Set incomplete flag." << std::endl;
+      Trace("quant-engine") << "Set incomplete flag." << std::endl;
       getOutputChannel().setIncomplete();
     }
     //output debug stats
@@ -646,8 +658,6 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
         d_modules[i]->registerQuantifier( f );
       }
       Node ceBody = d_term_db->getInstConstantBody( 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 );
@@ -1209,9 +1219,19 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
 
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
+    //filter based on notify classes
+    if( !d_inst_notify.empty() ){
+      unsigned prev_lem_sz = d_lemmas_waiting.size();
+      for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+        d_inst_notify[j]->filterInstantiations();
+      }  
+      if( prev_lem_sz!=d_lemmas_waiting.size() ){
+        Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
+      }
+    }
     //take default output channel if none is provided
     d_hasAddedLemma = true;
-    for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
+    for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
     }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4c7cb4a2f..60666c4a9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -48,6 +48,7 @@ class InstantiationNotify {
 public:
   InstantiationNotify(){}
   virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+  virtual void filterInstantiations() = 0;
 };
 
 namespace quantifiers {
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 2ca807662..8c847be60 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -48,7 +48,8 @@ TESTS = commutative.sy \
         clock-inc-tuple.sy \
         dt-test-ns.sy \
         no-mention.sy \
-        max2-univ.sy
+        max2-univ.sy \
+        strings-small.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
new file mode 100644
index 000000000..bc559f94a
--- /dev/null
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -0,0 +1,35 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+(set-logic SLIA)
+(synth-fun f ((firstname String) (lastname String)) String
+((Start String (ntString))
+
+(ntString String (
+firstname 
+lastname 
+" "
+(str.++ ntString ntString)))
+
+(ntInt Int (
+0 
+1 
+2
+(+ ntInt ntInt)
+(- ntInt ntInt)
+(str.len ntString)
+(str.to.int ntString)
+(str.indexof ntString ntString ntInt)))
+
+(ntBool Bool (
+true 
+false
+(str.prefixof ntString ntString)
+(str.suffixof ntString ntString)
+(str.contains ntString ntString)))
+
+))
+
+(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer"))
+
+(check-synth)
+