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