src/theory/term_registration_visitor.h

   1 /*********************                                                        */
   2 /*! \file term_registration_visitor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 <unordered_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::TheoryIdSet, TNodeHashFunction>
  46       TNodeToTheorySetMap;
  47
  48   /**
  49    * Map from terms to the theories that have already had this term pre-registered.
  50    */
  51   TNodeToTheorySetMap d_visited;
  52
  53   /**
  54    * A set of all theories in the term
  55    */
  56   theory::TheoryIdSet d_theories;
  57
  58   /**
  59    * String representation of the visited map, for debugging purposes.
  60    */
  61   std::string toString() const;
  62
  63  public:
  64   /** Returned set tells us which theories there are */
  65   typedef theory::TheoryIdSet return_type;
  66
  67   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
  68       : d_engine(engine), d_visited(context), d_theories(0)
  69   {
  70   }
  71
  72   /**
  73    * Returns true is current has already been pre-registered with both current
  74    * 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
  80    * haven't seen the term yet.
  81    */
  82   void visit(TNode current, TNode parent);
  83
  84   /**
  85    * Marks the node as the starting literal.
  86    */
  87   void start(TNode node) {}
  88
  89   /**
  90    * Notifies the engine of all the theories used.
  91    */
  92   theory::TheoryIdSet done(TNode node) { return d_theories; }
  93 };
  94
  95
  96 /**
  97  * The reason why we need to make this outside of the pre-registration loop is because we need a shared term x to
  98  * be associated with every atom that contains it. For example, if given f(x) >= 0 and f(x) + 1 >= 0, although f(x) has
  99  * been visited already, we need to visit it again, since we need to associate it with both atoms.
 100  */
 101 class SharedTermsVisitor {
 102
 103   /** The shared terms database */
 104   SharedTermsDatabase& d_sharedTerms;
 105
 106   /**
 107    * Cache from preprocessing of atoms.
 108    */
 109   typedef std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>
 110       TNodeVisitedMap;
 111   TNodeVisitedMap d_visited;
 112
 113   /**
 114    * String representation of the visited map, for debugging purposes.
 115    */
 116   std::string toString() const;
 117
 118   /**
 119    * The initial atom.
 120    */
 121   TNode d_atom;
 122
 123 public:
 124
 125   typedef void return_type;
 126
 127   SharedTermsVisitor(SharedTermsDatabase& sharedTerms)
 128   : d_sharedTerms(sharedTerms) {}
 129
 130   /**
 131    * Returns true is current has already been pre-registered with both current and parent theories.
 132    */
 133   bool alreadyVisited(TNode current, TNode parent) const;
 134
 135   /**
 136    * Pre-registeres current with any of the current and parent theories that haven't seen the term yet.
 137    */
 138   void visit(TNode current, TNode parent);
 139
 140   /**
 141    * Marks the node as the starting literal.
 142    */
 143   void start(TNode node);
 144
 145   /**
 146    * Just clears the state.
 147    */
 148   void done(TNode node);
 149
 150   /**
 151    * Clears the internal state.
 152    */
 153   void clear();
 154 };
 155
 156
 157 }