1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Dejan Jovanovic, Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "theory/atom_requests.h" |
20 |
|
|
21 |
|
using namespace cvc5; |
22 |
|
|
23 |
9459 |
AtomRequests::AtomRequests(context::Context* context) |
24 |
|
: d_allRequests(context) |
25 |
|
, d_requests(context) |
26 |
9459 |
, d_triggerToRequestMap(context) |
27 |
9459 |
{} |
28 |
|
|
29 |
3580303 |
AtomRequests::element_index AtomRequests::getList(TNode trigger) const { |
30 |
3580303 |
trigger_to_list_map::const_iterator find = d_triggerToRequestMap.find(trigger); |
31 |
3580303 |
if (find == d_triggerToRequestMap.end()) { |
32 |
3575113 |
return null_index; |
33 |
|
} else { |
34 |
5190 |
return (*find).second; |
35 |
|
} |
36 |
|
} |
37 |
|
|
38 |
|
bool AtomRequests::isTrigger(TNode atom) const { |
39 |
|
return getList(atom) != null_index; |
40 |
|
} |
41 |
|
|
42 |
3576609 |
AtomRequests::atom_iterator AtomRequests::getAtomIterator(TNode trigger) const { |
43 |
3576609 |
return atom_iterator(*this, getList(trigger)); |
44 |
|
} |
45 |
|
|
46 |
3694 |
void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory) { |
47 |
|
|
48 |
3694 |
Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << ")" << std::endl; |
49 |
|
|
50 |
7388 |
Request request(atomToSend, toTheory); |
51 |
|
|
52 |
3694 |
if (d_allRequests.find(request) != d_allRequests.end()) { |
53 |
|
// Have it already |
54 |
|
Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): already there" << std::endl; |
55 |
|
return; |
56 |
|
} |
57 |
3694 |
Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): adding" << std::endl; |
58 |
|
|
59 |
|
/// Mark the new request |
60 |
3694 |
d_allRequests.insert(request); |
61 |
|
|
62 |
|
// Index of the new request in the list of trigger |
63 |
3694 |
element_index index = d_requests.size(); |
64 |
3694 |
element_index previous = getList(triggerAtom); |
65 |
3694 |
d_requests.push_back(Element(request, previous)); |
66 |
3694 |
d_triggerToRequestMap[triggerAtom] = index; |
67 |
|
} |
68 |
|
|
69 |
3581884 |
bool AtomRequests::atom_iterator::done() const { return d_index == null_index; } |
70 |
|
|
71 |
5275 |
void AtomRequests::atom_iterator::next() { |
72 |
5275 |
d_index = d_requests.d_requests[d_index].d_previous; |
73 |
5275 |
} |
74 |
|
|
75 |
5275 |
const AtomRequests::Request& AtomRequests::atom_iterator::get() const { |
76 |
5275 |
return d_requests.d_requests[d_index].d_request; |
77 |
28191 |
} |
78 |
|
|