Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

1 files changed, 218 insertions, 110 deletions

diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 265026b39..57bc6d9cf 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -23,6 +23,8 @@
 
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
 #include "theory/rewriter.h"
+#include "util/options.h"
+
 
 using namespace std;
 using namespace CVC4;
@@ -30,6 +32,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::rewriterules;
+using namespace CVC4::theory::rrinst;
 
 
 namespace CVC4 {
@@ -69,14 +72,14 @@ size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{
     Node g = substNode(re,rule->guards[start],cache);
     switch(re.addWatchIfDontKnow(g,this,start)){
     case ATRUE:
-      Debug("rewriterules") << g << "is true" << std::endl;
+      Debug("rewriterules::guards") << g << "is true" << std::endl;
       ++start;
       continue;
     case AFALSE:
-      Debug("rewriterules") << g << "is false" << std::endl;
+      Debug("rewriterules::guards") << g << "is false" << std::endl;
       return -1;
     case ADONTKNOW:
-      Debug("rewriterules") << g << "is unknown" << std::endl;
+      Debug("rewriterules::guards") << g << "is unknown" << std::endl;
       return start;
     }
   }
@@ -132,31 +135,31 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c,
                                        QuantifiersEngine* qe) :
   Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo, qe),
   d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0),
-  d_explanations(c), d_ruleinsts_to_add()
+  d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false)
   {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  Debug("rewriterules") << Node::setdepth(-1);
-  Debug("rewriterules-rewrite") << Node::setdepth(-1);
 }
 
 void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r,
                                              InstMatch & im,
                                              bool delay){
   ++r->nb_matched;
+  ++d_statistics.d_match_found;
   if(rewrite_instantiation) im.applyRewrite();
   if(representative_instantiation)
     im.makeRepresentative( getQuantifiersEngine() );
 
   if(!cache_match || !r->inCache(*this,im)){
     ++r->nb_applied;
+    ++d_statistics.d_cache_miss;
     std::vector<Node> subst;
     im.computeTermVec(getQuantifiersEngine(), r->inst_vars , subst);
     RuleInst * ri = new RuleInst(*this,r,subst,
                                  r->directrr ? im.d_matched : Node::null());
-    Debug("rewriterules") << "One matching found"
-                          << (delay? "(delayed)":"")
-                          << ":" << *ri << std::endl;
+    Debug("rewriterules::matching") << "One matching found"
+                                    << (delay? "(delayed)":"")
+                                    << ":" << *ri << std::endl;
     // Find the first non verified guard, don't save the rule if the
     // rule can already be fired In fact I save it otherwise strange
     // things append.
@@ -168,6 +171,8 @@ void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r,
         d_ruleinsts.push_back(ri);
       else delete(ri);
     };
+  }else{
+    ++d_statistics.d_cache_hit;
   };
 }
 
@@ -179,7 +184,11 @@ void TheoryRewriteRules::check(Effort level) {
   while(!done()) {
     // Get all the assertions
     // TODO: Test that it have already been ppAsserted
-    get();
+
+    //if we are here and ppAssert has not been done
+    // that means that ppAssert is off so we need to assert now
+    if(!d_ppAssert_on) addRewriteRule(get());
+    else get();
     // Assertion assertion = get();
     // TNode fact = assertion.assertion;
 
@@ -190,30 +199,30 @@ void TheoryRewriteRules::check(Effort level) {
 
     };
 
-  Debug("rewriterules") << "Check:" << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl;
+  Debug("rewriterules::check") << "RewriteRules::Check start " << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl;
 
   /** Test each rewrite rule */
   for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) {
     RewriteRule * r = d_rules[rid];
     if (level!=EFFORT_FULL && r->d_split) continue;
-    Debug("rewriterules") << "  rule: " << r << std::endl;
+    Debug("rewriterules::check") << "RewriteRules::Check  rule: " << *r << std::endl;
     Trigger & tr = r->trigger;
     //reset instantiation round for trigger (set up match production)
     tr.resetInstantiationRound();
-    //begin iterating from the first match produced by the trigger
-    tr.reset( Node::null() );
 
     /** Test the possible matching one by one */
-    InstMatch im;
-    while(tr.getNextMatch( im )){
+    while(tr.getNextMatch()){
+      InstMatch im = tr.getInstMatch();
       addMatchRuleTrigger(r, im, true);
-      im.clear();
     }
   }
 
   const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL;
   bool polldone = false;
 
+  if(level==EFFORT_FULL) ++d_statistics.d_full_check;
+  else ++d_statistics.d_check;
+
   GuardedMap::const_iterator p = d_guardeds.begin();
   do{
 
@@ -221,7 +230,7 @@ void TheoryRewriteRules::check(Effort level) {
     //dequeue instantiated rules
     for(; !d_ruleinsts_to_add.empty();){
       RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back();
-      if(simulateRewritting && ri->alreadyRewritten(*this)) break;
+      if(simulateRewritting && ri->alreadyRewritten(*this)) continue;
       if(ri->findGuard(*this, 0) != ri->rule->guards.size())
         d_ruleinsts.push_back(ri);
       else delete(ri);
@@ -239,7 +248,7 @@ void TheoryRewriteRules::check(Effort level) {
       bool value;
       if(getValuation().hasSatValue(g,value)){
         if(value) polldone = true; //One guard is true so pass n check
-        Debug("rewriterules") << "Poll value:" << g
+        Debug("rewriterules::guards") << "Poll value:" << g
                              << " is " << (value ? "true" : "false") << std::endl;
         notification(g,value);
         //const Guarded & glast2 = (*l)[l->size()-1];
@@ -266,14 +275,14 @@ void TheoryRewriteRules::check(Effort level) {
       // If it has a value it should already has been notified
       bool value; value = value; // avoiding the warning in non debug mode
       Assert(!getValuation().hasSatValue(g,value));
-      Debug("rewriterules") << "Narrowing on:" << g << std::endl;
+      Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
       /** Can split on already rewritten instrule... but... */
       getOutputChannel().split(g);
     }
   }
 
   Assert(d_ruleinsts_to_add.empty());
-  Debug("rewriterules") << "Check done:" << d_checkLevel << std::endl;
+  Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl;
 
 };
 
@@ -283,7 +292,13 @@ Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern
   //  Debug("rewriterules") << "createTrigger:";
   getQuantifiersEngine()->registerPattern(pattern);
   return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern,
-                             match_gen_kind, true);
+                             Options::current()->efficientEMatching?
+                             Trigger::MATCH_GEN_EFFICIENT_E_MATCH :
+                             Trigger::MATCH_GEN_DEFAULT,
+                             true,
+                             Trigger::TR_MAKE_NEW,
+                             false);
+  //                             Options::current()->smartMultiTriggers);
 };
 
 bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested,
@@ -299,9 +314,9 @@ bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested,
 
 void TheoryRewriteRules::notification(GList * const lpropa, bool b){
   if (b){
-    for(GList::const_iterator g = lpropa->begin();
-        g != lpropa->end(); ++g) {
-      (*g).nextGuard(*this);
+    for(size_t ig = 0;
+        ig != lpropa->size(); ++ig) {
+      (*lpropa)[ig].nextGuard(*this);
     };
     lpropa->push_back(Guarded(RULEINST_TRUE,0));
   }else{
@@ -315,16 +330,6 @@ void TheoryRewriteRules::notification(GList * const lpropa, bool b){
 
 Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri,
                                               const size_t gid){
-  /** TODO: Should use the representative of g, but should I keep the
-      mapping for myself? */
-  //AJR: removed this code after talking with Francois
-  ///* If it false in one model (current valuation) it's false for all */
-  //if (useCurrentModel){
-  //  Node val = getValuation().getValue(g0);
-  //  Debug("rewriterules") << "getValue:" << g0 << " = "
-  //                        << val << " is " << (val == d_false) << std::endl;
-  //  if (val == d_false) return AFALSE;
-  //};
   /** Currently create a node with a literal */
   Node g = getValuation().ensureLiteral(g0);
   GuardedMap::iterator l_i = d_guardeds.find(g);
@@ -384,68 +389,119 @@ void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) {
 };
 
 
+Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){
+  Assert(conjunction.getKind() == kind::AND);
+  switch(conjunction.getNumChildren()){
+  case 0:
+    return d_true;
+  case 1:
+    return conjunction[0];
+  default:
+    return conjunction;
+  }
+
+}
+
+void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){
+  TypeNode booleanType = NodeManager::currentNM()->booleanType();
+  // if the rule is directly applied by the rewriter,
+  // we should take care to use the representative that can't be directly rewritable:
+  // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't
+  // add the constraint car(cons(x,l) = x because it is rewritten to x = x.
+  // But we should say cons(a) = x
+  Assert(!inst->d_matched.isNull());
+  Assert( inst->d_matched.getKind() == kind::APPLY_UF);
+  Assert( substHead.getKind() == kind::APPLY_UF );
+  Assert( inst->d_matched.getOperator() == substHead.getOperator() );
+  Assert(conjunction.getKind() == kind::AND);
+  // replace the left hand side by the term really matched
+  NodeBuilder<2> nb;
+  for(size_t i = 0,
+        iend = inst->d_matched.getNumChildren(); i < iend; ++i){
+    nb.clear( inst->d_matched[i].getType(false) == booleanType ?
+              kind::IFF : kind::EQUAL );
+    nb << inst->d_matched[i] << substHead[i];
+    conjunction << static_cast<Node>(nb);
+  }
+}
+
+Node skolemizeBody( Node f ){
+  /*TODO skolemize the subformula of s with constant or skolemize
+    directly in the body of the rewrite rule with an uninterpreted
+    function.
+   */
+  if ( f.getKind()!=EXISTS ) return f;
+  std::vector< Node > vars;
+  std::vector< Node > csts;
+  for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+    csts.push_back( NodeManager::currentNM()->mkSkolem( f[0][i].getType()) );
+    vars.push_back( f[0][i] );
+  }
+  return f[ 1 ].substitute( vars.begin(), vars.end(),
+                            csts.begin(), csts.end() );
+}
+
+
 void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){
   //   Debug("rewriterules") << "A rewrite rules is verified. Add lemma:";
-  Debug("rewriterules") << "propagateRule" << *inst << std::endl;
+  Debug("rewriterules::propagate") << "propagateRule" << *inst << std::endl;
   const RewriteRule * rule = inst->rule;
   ++rule->nb_applied;
   // Can be more something else than an equality in fact (eg. propagation rule)
-  Node equality = inst->substNode(*this,rule->body,cache);
+  Node equality = skolemizeBody(inst->substNode(*this,rule->body,cache));
   if(propagate_as_lemma){
     Node lemma = equality;
-    if(rule->guards.size() > 0){
-      // TODO: problem with reduction rule => instead of <=>
-      lemma = substGuards(inst, cache).impNode(equality);
-    };
     if(rule->directrr){
-      TypeNode booleanType = NodeManager::currentNM()->booleanType();
-      // if the rule is directly applied by the rewriter,
-      // we should take care to use the representative that can't be directly rewritable:
-      // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't
-      // add the constraint car(cons(x,l) = x because it is rewritten to x = x.
-      // But we should say cons(a) = x
-      Assert(lemma.getKind() == kind::EQUAL ||
-             lemma.getKind() == kind::IMPLIES);
-      Assert(!inst->d_matched.isNull());
-      Assert( inst->d_matched.getOperator() == lemma[0].getOperator() );
-      // replace the left hand side by the term really matched
+      NodeBuilder<> conjunction(kind::AND);
+      explainInstantiation(inst,
+                           rule->guards.size() > 0?
+                           inst->substNode(*this,rule->guards[0],cache) : equality[0],
+                           conjunction);
       Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched;
-      Node hyp;
-      NodeBuilder<2> nb;
-      if(inst->d_matched.getNumChildren() == 1){
-        nb.clear( inst->d_matched[0].getType(false) == booleanType ?
-                  kind::IFF : kind::EQUAL );
-        nb << inst->d_matched[0] << lemma[0][0];
-        hyp = nb;
-      }else{
-        NodeBuilder<> andb(kind::AND);
-        for(size_t i = 0,
-              iend = inst->d_matched.getNumChildren(); i < iend; ++i){
-          nb.clear( inst->d_matched[i].getType(false) == booleanType ?
-                    kind::IFF : kind::EQUAL );
-          nb << inst->d_matched[i] << lemma[0][i];
-          andb << static_cast<Node>(nb);
-        }
-        hyp = andb;
-      };
-      nb.clear(lemma.getKind());
-      nb << inst->d_matched << lemma[1];
-      lemma = hyp.impNode(static_cast<Node>(nb));
+      //rewrite rule
+      TypeNode booleanType = NodeManager::currentNM()->booleanType();
+      if(equality[1].getType(false) == booleanType)
+        equality = inst->d_matched.iffNode(equality[1]);
+      else equality = inst->d_matched.eqNode(equality[1]);
+      lemma = normalizeConjunction(conjunction).impNode(equality);
       Debug("rewriterules-directrr") << " -> " << lemma << std::endl;
-    };
-    // Debug("rewriterules") << "lemma:" << lemma << std::endl;
+    }
+    else if(rule->guards.size() > 0){
+      // We can use implication for reduction rules since the head is known
+      // to be true
+      NodeBuilder<> conjunction(kind::AND);
+      substGuards(inst,cache,conjunction);
+      lemma = normalizeConjunction(conjunction).impNode(equality);
+    }
+    Debug("rewriterules::propagate") << "propagated " << lemma << std::endl;
     getOutputChannel().lemma(lemma);
   }else{
-    Assert(!direct_rewrite);
-    Node lemma_lit = getValuation().ensureLiteral(equality);
+    Node lemma_lit = equality;
+    if(rule->directrr && rule->guards.size() == 0)
+      lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules
+    lemma_lit = getValuation().ensureLiteral(lemma_lit);
     ExplanationMap::const_iterator p = d_explanations.find(lemma_lit);
     if(p!=d_explanations.end()) return; //Already propagated
     bool value;
     if(getValuation().hasSatValue(lemma_lit,value)){
       /* Already assigned */
       if (!value){
-        Node conflict = substGuards(inst,cache,lemma_lit);
-        getOutputChannel().conflict(conflict);
+        NodeBuilder<> conflict(kind::AND);
+
+        if(rule->directrr){
+          explainInstantiation(inst,
+                               rule->guards.size() > 0?
+                               inst->substNode(*this,rule->guards[0],cache) : equality[0],
+                               conflict);
+          if(rule->guards.size() > 0){
+            //reduction rule
+            Assert(rule->guards.size() == 1);
+            conflict << inst->d_matched; //this one will be two times
+          }
+        }
+        substGuards(inst,cache,conflict);
+        conflict << lemma_lit;
+        getOutputChannel().conflict(normalizeConjunction(conflict));
       };
     }else{
       getOutputChannel().propagate(lemma_lit);
@@ -456,57 +512,79 @@ void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){
   if(simulateRewritting){
     static NoMatchAttribute rewrittenNodeAttribute;
     // Tag the rewritted terms
-    for(std::vector<Node>::iterator i = rule->to_remove.begin();
-        i == rule->to_remove.end(); ++i){
-      (*i).setAttribute(rewrittenNodeAttribute,true);
+    // for(std::vector<Node>::iterator i = rule->to_remove.begin();
+    //     i == rule->to_remove.end(); ++i){
+    //   (*i).setAttribute(rewrittenNodeAttribute,true);
+    // };
+    for(size_t i = 0; i < rule->to_remove.size(); ++i){
+      Node rewritten = inst->substNode(*this,rule->to_remove[i],cache);
+      Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl;
+      rewritten.setAttribute(rewrittenNodeAttribute,true);
     };
+
   };
 
-  //Verify that this instantiation can't immediately fire another rule
-  for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin();
-      p != rule->body_match.end(); ++p){
-    RewriteRule * r = (*p).second;
-    // Debug("rewriterules") << "  rule: " << r << std::endl;
-    // Use trigger2 since we can be in check
-    Trigger & tr = r->trigger_for_body_match;
-    InstMatch im;
-    TNode m = inst->substNode(*this,(*p).first, cache);
-    tr.getMatch(m,im);
-    if(!im.empty()){
-      im.d_matched = m;
-      addMatchRuleTrigger(r, im);
+  if ( compute_opt && !rule->body_match.empty() ){
+
+    uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->getTheory( theory::THEORY_UF ));
+    eq::EqualityEngine* ee =
+      static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
+
+    //Verify that this instantiation can't immediately fire another rule
+    for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin();
+        p != rule->body_match.end(); ++p){
+      RewriteRule * r = (*p).second;
+      // Use trigger2 since we can be in check
+      ApplyMatcher * tr = r->trigger_for_body_match;
+      Assert(tr != NULL);
+      tr->resetInstantiationRound(getQuantifiersEngine());
+      InstMatch im;
+      TNode m = inst->substNode(*this,(*p).first, cache);
+      Assert( m.getKind() == kind::APPLY_UF );
+      ee->addTerm(m);
+      if( tr->reset(m,im,getQuantifiersEngine()) ){
+        im.d_matched = m;
+        Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl;
+        addMatchRuleTrigger(r, im);
+      }
     }
+
   }
 };
 
-
-Node TheoryRewriteRules::substGuards(const RuleInst *inst,
+void TheoryRewriteRules::substGuards(const RuleInst *inst,
                                      TCache cache,
-                                     /* Already substituted */
-                                     Node last){
+                                     NodeBuilder<> & conjunction){
   const RewriteRule * r = inst->rule;
-  /** No guards */
-  const size_t size = r->guards.size();
-  if(size == 0) return (last.isNull()?d_true:last);
-  /** One guard */
-  if(size == 1 && last.isNull()) return inst->substNode(*this,r->guards[0],cache);
   /** Guards */ /* TODO remove the duplicate with a set like in uf? */
-  NodeBuilder<> conjunction(kind::AND);
   for(std::vector<Node>::const_iterator p = r->guards.begin();
       p != r->guards.end(); ++p) {
     Assert(!p->isNull());
     conjunction << inst->substNode(*this,*p,cache);
   };
-  if (!last.isNull()) conjunction << last;
-  return conjunction;
 }
 
 Node TheoryRewriteRules::explain(TNode n){
   ExplanationMap::const_iterator p = d_explanations.find(n);
   Assert(p!=d_explanations.end(),"I forget the explanation...");
-  RuleInst i = (*p).second;
-  //Notice() << n << "<-" << *(i.rule) << std::endl;
-  return substGuards(&i, TCache ());
+  RuleInst inst = (*p).second;
+  const RewriteRule * rule = inst.rule;
+  TCache cache;
+  NodeBuilder<> explanation(kind::AND);
+  if(rule->directrr){
+    explainInstantiation(&inst,
+                         rule->guards.size() > 0?
+                         inst.substNode(*this,rule->guards[0],cache):
+                         inst.substNode(*this,rule->body[0]  ,cache),
+                         explanation);
+    if(rule->guards.size() > 0){
+      //reduction rule
+      Assert(rule->guards.size() == 1);
+      explanation << inst.d_matched; //this one will be two times
+    }
+  };
+  substGuards(&inst, cache ,explanation);
+  return normalizeConjunction(explanation);
 }
 
 void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){
@@ -515,9 +593,39 @@ void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){
 
 Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   addRewriteRule(in);
+  d_ppAssert_on = true;
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
+TheoryRewriteRules::Statistics::Statistics():
+  d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0),
+  d_check("TheoryRewriteRules::Check", 0),
+  d_full_check("TheoryRewriteRules::FullCheck", 0),
+  d_poll("TheoryRewriteRules::Poll", 0),
+  d_match_found("TheoryRewriteRules::MatchFound", 0),
+  d_cache_hit("TheoryRewriteRules::CacheHit", 0),
+  d_cache_miss("TheoryRewriteRules::CacheMiss", 0)
+{
+  StatisticsRegistry::registerStat(&d_num_rewriterules);
+  StatisticsRegistry::registerStat(&d_check);
+  StatisticsRegistry::registerStat(&d_full_check);
+  StatisticsRegistry::registerStat(&d_poll);
+  StatisticsRegistry::registerStat(&d_match_found);
+  StatisticsRegistry::registerStat(&d_cache_hit);
+  StatisticsRegistry::registerStat(&d_cache_miss);
+}
+
+TheoryRewriteRules::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_num_rewriterules);
+  StatisticsRegistry::unregisterStat(&d_check);
+  StatisticsRegistry::unregisterStat(&d_full_check);
+  StatisticsRegistry::unregisterStat(&d_poll);
+  StatisticsRegistry::unregisterStat(&d_match_found);
+  StatisticsRegistry::unregisterStat(&d_cache_hit);
+  StatisticsRegistry::unregisterStat(&d_cache_miss);
+}
+
+
 }/* CVC4::theory::rewriterules namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */