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-2014  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 QuantInfo;
  33
  34 class RewriteEngine : public QuantifiersModule
  35 {
  36   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  37   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  38   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  39   std::vector< Node > d_rr_quant;
  40   std::vector< Node > d_priority_order;
  41   std::map< Node, Node > d_rr;
  42   Node d_true;
  43   /** explicitly provided patterns */
  44   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
  45   /** get the quantifer info object */
  46   std::map< Node, Node > d_qinfo_n;
  47   std::map< Node, QuantInfo > d_qinfo;
  48   double getPriority( Node f );
  49   bool d_needsSort;
  50   std::map< Node, std::map< Node, Node > > d_inst_const_node;
  51   Node getInstConstNode( Node n, Node q );
  52 private:
  53   int checkRewriteRule( Node f, Theory::Effort e );
  54 public:
  55   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
  56
  57   bool needsCheck( Theory::Effort e );
  58   void check( Theory::Effort e, unsigned quant_e );
  59   void registerQuantifier( Node f );
  60   void assertNode( Node n );
  61   /** Identify this module */
  62   std::string identify() const { return "RewriteEngine"; }
  63 };
  64
  65 }
  66 }
  67 }
  68
  69 #endif