1 /********************* */ 2 /*! \file atom_requests.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Dejan Jovanovic 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 ** \brief [[ Add one-line brief description here ]] 13 ** 14 ** [[ Add lengthier description here ]] 15 ** \todo document this file 16 **/ 17 18 #include "cvc4_private.h" 19 20 #pragma once 21 22 #include "expr/node.h" 23 #include "theory/theory.h" 24 #include "context/cdlist.h" 25 #include "context/cdhashset.h" 26 #include "context/cdhashmap.h" 27 28 namespace CVC4 { 29 30 class AtomRequests { 31 32 public: 33 34 /** Which atom and where to send it */ 35 struct Request { 36 /** Atom */ 37 Node atom; 38 /** Where to send it */ 39 theory::TheoryId toTheory; 40 RequestRequest41 Request(TNode atom, theory::TheoryId toTheory) 42 : atom(atom), toTheory(toTheory) {} RequestRequest43 Request() 44 : toTheory(theory::THEORY_LAST) 45 {} 46 47 bool operator == (const Request& other) const { 48 return atom == other.atom && toTheory == other.toTheory; 49 } 50 hashRequest51 size_t hash() const { 52 return atom.getId(); 53 } 54 55 }; 56 57 AtomRequests(context::Context* context); 58 59 /** Mark the atom to be sent to a theory, when the trigger atom gets assigned */ 60 void add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory); 61 62 /** Returns true if the node is a trigger and has a list of atoms to send */ 63 bool isTrigger(TNode atom) const; 64 65 /** Indices in lists */ 66 typedef size_t element_index; 67 68 class atom_iterator { 69 const AtomRequests& requests; 70 element_index index; 71 friend class AtomRequests; atom_iterator(const AtomRequests & requests,element_index start)72 atom_iterator(const AtomRequests& requests, element_index start) 73 : requests(requests), index(start) {} 74 public: 75 /** Is this iterator done */ 76 bool done() const; 77 /** Go to the next element */ 78 void next(); 79 /** Get the actual request */ 80 const Request& get() const; 81 }; 82 83 atom_iterator getAtomIterator(TNode trigger) const; 84 85 private: 86 87 struct RequestHashFunction { operatorRequestHashFunction88 size_t operator () (const Request& r) const { 89 return r.hash(); 90 } 91 }; 92 93 /** Set of all requests so we don't add twice */ 94 context::CDHashSet<Request, RequestHashFunction> d_allRequests; 95 96 static const element_index null_index = -1; 97 98 struct Element { 99 /** Current request */ 100 Request request; 101 /** Previous request */ 102 element_index previous; 103 ElementElement104 Element(const Request& request, element_index previous) 105 : request(request), previous(previous) 106 {} 107 }; 108 109 /** We index the requests in this vector, it's a list */ 110 context::CDList<Element> d_requests; 111 112 typedef context::CDHashMap<Node, element_index, NodeHashFunction> trigger_to_list_map; 113 114 /** Map from triggers, to the list of elements they trigger */ 115 trigger_to_list_map d_triggerToRequestMap; 116 117 /** Get the list index of the trigger */ 118 element_index getList(TNode trigger) const; 119 120 }; 121 122 } 123 124 125 126 127