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