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 appropriate theory to pre-register the term. The visitor also keeps track
  30  * of the sets of theories that are involved in the terms, so that it can say if there are multiple
  31  * theories involved.
  32  *
  33  * A sub-term has been visited if the theories of both the parent and the term itself have already
  34  * visited this term.
  35  *
  36  * Computation of the set of theories in the original term are computed in the alreadyVisited method
  37  * so as no to skip any theories.
  38  */
  39 class PreRegisterVisitor {
  40
  41   /** The engine */
  42   TheoryEngine* d_engine;
  43
  44   typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
  45
  46   /**
  47    * Map from terms to the theories that have already had this term pre-registered.
  48    */
  49   TNodeToTheorySetMap d_visited;
  50
  51   /**
  52    * A set of all theories in the term
  53    */
  54   theory::Theory::Set d_theories;
  55
  56   /**
  57    * Is true if the term we're traversing involves multiple theories.
  58    */
  59   bool d_multipleTheories;
  60
  61   /**
  62    * String representation of the visited map, for debugging purposes.
  63    */
  64   std::string toString() const;
  65
  66 public:
  67
  68   /** Return type tells us if there are more than one theory or not */
  69   typedef bool return_type;
  70
  71   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
  72   : d_engine(engine)
  73   , d_visited(context)
  74   , d_theories(0)
  75   , d_multipleTheories(false)
  76   {}
  77
  78   /**
  79    * Returns true is current has already been pre-registered with both current and parent theories.
  80    */
  81   bool alreadyVisited(TNode current, TNode parent);
  82
  83   /**
  84    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
  85    */
  86   void visit(TNode current, TNode parent);
  87
  88   /**
  89    * Marks the node as the starting literal.
  90    */
  91   void start(TNode node);
  92
  93   /**
  94    * Notifies the engine of all the theories used.
  95    */
  96   bool done(TNode node);
  97
  98 };
  99
 100
 101 /**
 102  * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
 103  * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
 104  * been visited already, we need to visit it again, since we need to associate it with both atoms.
 105  */
 106 class SharedTermsVisitor {
 107
 108   /** The shared terms database */
 109   SharedTermsDatabase& d_sharedTerms;
 110
 111   /**
 112    * Cache from proprocessing of atoms.
 113    */
 114   typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
 115   TNodeVisitedMap d_visited;
 116
 117   /**
 118    * String representation of the visited map, for debugging purposes.
 119    */
 120   std::string toString() const;
 121
 122   /**
 123    * The initial atom.
 124    */
 125   TNode d_atom;
 126
 127 public:
 128
 129   typedef void return_type;
 130
 131   SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
 132   : d_sharedTerms(sharedTerms) {}
 133
 134   /**
 135    * Returns true is current has already been pre-registered with both current and parent theories.
 136    */
 137   bool alreadyVisited(TNode current, TNode parent) const;
 138
 139   /**
 140    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
 141    */
 142   void visit(TNode current, TNode parent);
 143
 144   /**
 145    * Marks the node as the starting literal.
 146    */
 147   void start(TNode node);
 148
 149   /**
 150    * Just clears the state.
 151    */
 152   void done(TNode node);
 153
 154   /**
 155    * Clears the internal state.
 156    */
 157   void clear();
 158 };
 159
 160
 161 }