1 /******************************************************************************
2 * Top contributors (to current version):
3 * Dejan Jovanovic, Andrew Reynolds
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * [[ Add one-line brief description here ]]
15 * [[ Add lengthier description here ]]
16 * \todo document this file
19 #include "cvc5_private.h"
23 #include "expr/node.h"
24 #include "theory/theory_id.h"
25 #include "context/cdlist.h"
26 #include "context/cdhashset.h"
27 #include "context/cdhashmap.h"
35 /** Which atom and where to send it */
39 /** Where to send it */
40 theory::TheoryId d_toTheory
;
42 Request(TNode a
, theory::TheoryId tt
) : d_atom(a
), d_toTheory(tt
) {}
43 Request() : d_toTheory(theory::THEORY_LAST
) {}
45 bool operator == (const Request
& other
) const {
46 return d_atom
== other
.d_atom
&& d_toTheory
== other
.d_toTheory
;
49 size_t hash() const { return d_atom
.getId(); }
52 AtomRequests(context::Context
* context
);
54 /** Mark the atom to be sent to a theory, when the trigger atom gets assigned */
55 void add(TNode triggerAtom
, TNode atomToSend
, theory::TheoryId toTheory
);
57 /** Returns true if the node is a trigger and has a list of atoms to send */
58 bool isTrigger(TNode atom
) const;
60 /** Indices in lists */
61 typedef size_t element_index
;
64 const AtomRequests
& d_requests
;
65 element_index d_index
;
66 friend class AtomRequests
;
67 atom_iterator(const AtomRequests
& requests
, element_index start
)
68 : d_requests(requests
), d_index(start
)
73 /** Is this iterator done */
75 /** Go to the next element */
77 /** Get the actual request */
78 const Request
& get() const;
81 atom_iterator
getAtomIterator(TNode trigger
) const;
85 struct RequestHashFunction
{
86 size_t operator () (const Request
& r
) const {
91 /** Set of all requests so we don't add twice */
92 context::CDHashSet
<Request
, RequestHashFunction
> d_allRequests
;
94 static const element_index null_index
= -1;
97 /** Current request */
99 /** Previous request */
100 element_index d_previous
;
102 Element(const Request
& r
, element_index p
) : d_request(r
), d_previous(p
) {}
105 /** We index the requests in this vector, it's a list */
106 context::CDList
<Element
> d_requests
;
108 typedef context::CDHashMap
<Node
, element_index
> trigger_to_list_map
;
110 /** Map from triggers, to the list of elements they trigger */
111 trigger_to_list_map d_triggerToRequestMap
;
113 /** Get the list index of the trigger */
114 element_index
getList(TNode trigger
) const;