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, 5 insertions, 16 deletions

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 66b45be2f..b3db6d266 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -44,15 +44,6 @@ typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
 struct InstVarNumAttributeId {};
 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
 
-// Attribute that tell if a node have been asserted in this branch
-struct AvailableInTermDbId {};
-/** use the special for boolean flag */
-typedef expr::Attribute<AvailableInTermDbId,
-                        bool,
-                        expr::attr::NullCleanupStrategy,
-                        true  // context dependent
-                        > AvailableInTermDb;
-
 struct ModelBasisAttributeId {};
 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 //for APPLY_UF terms, 1 : term has direct child with model basis attribute,
@@ -60,10 +51,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 struct ModelBasisArgAttributeId {};
 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
 
-//for rewrite rules
-struct QRewriteRuleAttributeId {};
-typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
-
 //for bounded integers
 struct BoundIntLitAttributeId {};
 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
@@ -128,9 +115,6 @@ public:
   void reset( Theory::Effort effort );
   /** get operation */
   Node getOperator( Node n );
-private:
-  /** for efficient e-matching */
-  void addTermEfficient( Node n, std::set< Node >& added);
 public:
   /** parent structure (for efficient E-matching):
       n -> op -> index -> L
@@ -252,6 +236,11 @@ public:
   int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
+public:
+  /** is quantifier treated as a rewrite rule? */
+  static bool isRewriteRule( Node q );
+  /** get the rewrite rule associated with the quanfied formula */
+  static Node getRewriteRule( Node q );
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */