Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.

Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.

QCF is now functional backend to rewrite rules. Support boolean variables in QCF.  Change check-model to ignore rewrite rules.  Incorporate some fixes from master.

Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.

Minor fixes to QCF/rewrite engine, removes RE on last call approach.  Add option for one inst per round in RE.

Merging rewrite rules into master, check-model current fails on 3 FMF regressions.

Fix check-model issue, a line of code was omitted during merge.

1 files changed, 6 insertions, 26 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fbc501aec..858093543 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,8 +20,8 @@
 #include "theory/theory.h"
 #include "util/hash.h"
 #include "theory/quantifiers/inst_match.h"
-#include "theory/rewriterules/rr_inst_match.h"
 #include "theory/quantifiers/quant_util.h"
+#include "expr/attribute.h"
 
 #include "util/statistics_registry.h"
 
@@ -49,6 +49,8 @@ public:
   virtual void finishInit() {}
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+  /* reset at a round */
+  virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
@@ -75,11 +77,7 @@ namespace inst {
   class TriggerTrie;
 }/* CVC4::theory::inst */
 
-namespace rrinst {
-  class TriggerTrie;
-}/* CVC4::theory::inst */
-
-class EfficientEMatcher;
+//class EfficientEMatcher;
 class EqualityQueryQuantifiersEngine;
 
 class QuantifiersEngine {
@@ -102,8 +100,6 @@ private:
   quantifiers::RelevantDomain* d_rel_dom;
   /** phase requirements for each quantifier for each instantiation literal */
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
-  /** efficient e-matcher */
-  EfficientEMatcher* d_eem;
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -131,8 +127,6 @@ private:
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
-  /** all triggers for rewrite rules will be stored in this trie */
-  rrinst::TriggerTrie* d_rr_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   /** statistics for debugging */
@@ -144,8 +138,6 @@ private:
 public:
   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
-  /** get instantiator for id */
-  //Instantiator* getInstantiator( theory::TheoryId id );
   /** get theory engine */
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
@@ -171,8 +163,6 @@ public:
   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
   /** get phase requirement terms */
   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
-  /** get efficient e-matching utility */
-  EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
   /** get bounded integers utility */
   quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
   /** Conflict find mechanism for quantifiers */
@@ -199,8 +189,6 @@ private:
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
   void setInstantiationLevelAttr( Node n, uint64_t level );
-  /** do substitution */
-  Node doSubstitute( Node n, std::vector< Node >& terms );
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -208,6 +196,8 @@ public:
   Node getInstantiation( Node f, InstMatch& m );
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& terms );
+  /** do substitution */
+  Node getSubstitute( Node n, std::vector< Node >& terms );
   /** exist instantiation ? */
   bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
@@ -238,8 +228,6 @@ public:
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
-  /** get rewrite trigger database */
-  rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
   /** get the master equality engine */
@@ -260,14 +248,6 @@ public:
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;
     IntStat d_multi_trigger_instantiations;
-    IntStat d_term_in_termdb;
-    IntStat d_num_mono_candidates;
-    IntStat d_num_mono_candidates_new_term;
-    IntStat d_num_multi_candidates;
-    IntStat d_mono_candidates_cache_hit;
-    IntStat d_mono_candidates_cache_miss;
-    IntStat d_multi_candidates_cache_hit;
-    IntStat d_multi_candidates_cache_miss;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */