src/theory/term_registration_visitor.h

   1 /*********************                                                        */
   2 /*! \file node_visitor.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors:
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #pragma once
  18
  19 #include "context/context.h"
  20 #include "theory/shared_terms_database.h"
  21
  22 #include <ext/hash_map>
  23
  24 namespace CVC4 {
  25
  26 class TheoryEngine;
  27
  28 /**
  29  * Visitor that calls the apropriate theory to preregister the term.
  30  */
  31 class PreRegisterVisitor {
  32
  33   /** The engine */
  34   TheoryEngine* d_engine;
  35
  36   /**
  37    * Map from nodes to the theories that have already seen them.
  38    */
  39   typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
  40   TNodeVisitedMap d_visited;
  41
  42   /**
  43    * All the theories of the visitation.
  44    */
  45   theory::Theory::Set d_theories;
  46
  47   /**
  48    * String representation of the visited map, for debugging purposes.
  49    */
  50   std::string toString() const;
  51
  52   /**
  53    * Is there more than one theory involved.
  54    */
  55   bool d_multipleTheories;
  56
  57 public:
  58
  59   /** Return type tells us if there are more than one theory or not */
  60   typedef bool return_type;
  61
  62   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
  63   : d_engine(engine), d_visited(context), d_theories(0) {}
  64
  65   /**
  66    * Returns true is current has already been pre-registered with both current and parent theories.
  67    */
  68   bool alreadyVisited(TNode current, TNode parent) const;
  69
  70   /**
  71    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
  72    */
  73   void visit(TNode current, TNode parent);
  74
  75   /**
  76    * Marks the node as the starting literal.
  77    */
  78   void start(TNode node);
  79
  80   /**
  81    * Notifies the engine of all the theories used.
  82    */
  83   bool done(TNode node);
  84
  85 };
  86
  87
  88 /**
  89  * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
  90  * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
  91  * been visited already, we need to visit it again, since we need to associate it with both atoms.
  92  */
  93 class SharedTermsVisitor {
  94
  95   /** The shared terms database */
  96   SharedTermsDatabase& d_sharedTerms;
  97
  98   /**
  99    * Cache from proprocessing of atoms.
 100    */
 101   typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
 102   TNodeVisitedMap d_visited;
 103
 104   /**
 105    * String representation of the visited map, for debugging purposes.
 106    */
 107   std::string toString() const;
 108
 109   /**
 110    * The initial atom.
 111    */
 112   TNode d_atom;
 113
 114 public:
 115
 116   typedef void return_type;
 117
 118   SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
 119   : d_sharedTerms(sharedTerms) {}
 120
 121   /**
 122    * Returns true is current has already been pre-registered with both current and parent theories.
 123    */
 124   bool alreadyVisited(TNode current, TNode parent) const;
 125
 126   /**
 127    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
 128    */
 129   void visit(TNode current, TNode parent);
 130
 131   /**
 132    * Marks the node as the starting literal.
 133    */
 134   void start(TNode node);
 135
 136   /**
 137    * Just clears the state.
 138    */
 139   void done(TNode node);
 140
 141   /**
 142    * Clears the internal state.
 143    */
 144   void clear();
 145 };
 146
 147
 148 }