GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/atom_requests.cpp Lines: 27 31 87.1 %
Date: 2021-03-22 Branches: 45 112 40.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file atom_requests.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds
6
 ** This file is part of the CVC4 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.\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 "theory/atom_requests.h"
19
20
using namespace CVC4;
21
22
8995
AtomRequests::AtomRequests(context::Context* context)
23
: d_allRequests(context)
24
, d_requests(context)
25
8995
, d_triggerToRequestMap(context)
26
8995
{}
27
28
4648634
AtomRequests::element_index AtomRequests::getList(TNode trigger) const {
29
4648634
  trigger_to_list_map::const_iterator find = d_triggerToRequestMap.find(trigger);
30
4648634
  if (find == d_triggerToRequestMap.end()) {
31
4643613
    return null_index;
32
  } else {
33
5021
    return (*find).second;
34
  }
35
}
36
37
bool AtomRequests::isTrigger(TNode atom) const {
38
  return getList(atom) != null_index;
39
}
40
41
4644177
AtomRequests::atom_iterator AtomRequests::getAtomIterator(TNode trigger) const {
42
4644177
  return atom_iterator(*this, getList(trigger));
43
}
44
45
4457
void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory) {
46
47
4457
  Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << ")" << std::endl;
48
49
8914
  Request request(atomToSend, toTheory);
50
51
4457
  if (d_allRequests.find(request) != d_allRequests.end()) {
52
    // Have it already
53
    Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): already there" << std::endl;
54
    return;
55
  }
56
4457
  Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): adding" << std::endl;
57
58
  /// Mark the new request
59
4457
  d_allRequests.insert(request);
60
61
  // Index of the new request in the list of trigger
62
4457
  element_index index = d_requests.size();
63
4457
  element_index previous = getList(triggerAtom);
64
4457
  d_requests.push_back(Element(request, previous));
65
4457
  d_triggerToRequestMap[triggerAtom] = index;
66
}
67
68
4649262
bool AtomRequests::atom_iterator::done() const { return d_index == null_index; }
69
70
5085
void AtomRequests::atom_iterator::next() {
71
5085
  d_index = d_requests.d_requests[d_index].d_previous;
72
5085
}
73
74
5085
const AtomRequests::Request& AtomRequests::atom_iterator::get() const {
75
5085
  return d_requests.d_requests[d_index].d_request;
76
26676
}
77