src/theory/quantifiers/rewrite_engine.h

   1 /*********************                                                        */
   2 /*! \file rewrite_engine.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14 **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef __CVC4__REWRITE_ENGINE_H
  19 #define __CVC4__REWRITE_ENGINE_H
  20
  21 #include "theory/quantifiers_engine.h"
  22 #include "theory/quantifiers/trigger.h"
  23
  24 #include "context/context.h"
  25 #include "context/context_mm.h"
  26 #include "context/cdchunk_list.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace quantifiers {
  31
  32 class RewriteEngine : public QuantifiersModule
  33 {
  34   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  35   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  36   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  37   std::vector< Node > d_rr_quant;
  38   std::map< Node, Node > d_rr_guard;
  39   Node d_true;
  40   /** explicitly provided patterns */
  41   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
  42   double getPriority( Node f );
  43 private:
  44   int checkRewriteRule( Node f );
  45 public:
  46   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
  47
  48   void check( Theory::Effort e );
  49   void registerQuantifier( Node f );
  50   void assertNode( Node n );
  51 };
  52
  53 }
  54 }
  55 }
  56
  57 #endif