1 /********************* */ 2 /*! \file term_registration_visitor.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Dejan Jovanovic, Morgan Deters, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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::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 PreRegisterVisitor(TheoryEngine * engine,context::Context * context)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 */ start(TNode node)86 void start(TNode node) { } 87 88 /** 89 * Notifies the engine of all the theories used. 90 */ done(TNode node)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::unordered_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 SharedTermsVisitor(SharedTermsDatabase & sharedTerms)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 } 156