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