src/theory/quantifiers/rewrite_engine.h

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