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.

1 files changed, 7 insertions, 2 deletions

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;