src/theory/term_registration_visitor.h

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