GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_context_stack.cpp Lines: 26 36 72.2 %
Date: 2021-03-23 Branches: 38 134 28.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_context_stack.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Term context stack
13
 **/
14
15
#include "expr/term_context_stack.h"
16
17
#include "expr/term_context.h"
18
19
namespace CVC4 {
20
21
552782
TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {}
22
23
552782
void TCtxStack::pushInitial(Node t)
24
{
25
552782
  Assert(d_stack.empty());
26
552782
  d_stack.push_back(std::pair<Node, uint32_t>(t, d_tctx->initialValue()));
27
552782
}
28
29
118281
void TCtxStack::pushChildren(Node t, uint32_t tval)
30
{
31
277900
  for (size_t i = 0, nchild = t.getNumChildren(); i < nchild; i++)
32
  {
33
159619
    pushChild(t, tval, i);
34
  }
35
118281
}
36
37
2160256
void TCtxStack::pushChild(Node t, uint32_t tval, size_t index)
38
{
39
2160256
  Assert(index < t.getNumChildren());
40
4320512
  Trace("tctx-debug") << "TCtxStack::pushChild: computing " << t << "[" << index
41
2160256
                      << "] / " << tval << std::endl;
42
2160256
  uint32_t tcval = d_tctx->computeValue(t, tval, index);
43
4320512
  Trace("tctx-debug") << "TCtxStack::pushChild: returned " << t << "[" << index
44
2160256
                      << "] / " << tval << " ---> " << tcval << std::endl;
45
2160256
  d_stack.push_back(std::pair<Node, uint32_t>(t[index], tcval));
46
2160256
}
47
48
void TCtxStack::pushOp(Node t, uint32_t tval)
49
{
50
  Assert(t.hasOperator());
51
  uint32_t toval = d_tctx->computeValueOp(t, tval);
52
  d_stack.push_back(std::pair<Node, uint32_t>(t.getOperator(), toval));
53
}
54
55
166188
void TCtxStack::push(Node t, uint32_t tval)
56
{
57
166188
  d_stack.push_back(std::pair<Node, uint32_t>(t, tval));
58
166188
}
59
60
2879226
void TCtxStack::pop() { d_stack.pop_back(); }
61
62
void TCtxStack::clear() { d_stack.clear(); }
63
size_t TCtxStack::size() const { return d_stack.size(); }
64
65
4362072
bool TCtxStack::empty() const { return d_stack.empty(); }
66
67
4362072
std::pair<Node, uint32_t> TCtxStack::getCurrent() const
68
{
69
4362072
  return d_stack.back();
70
}
71
72
TCtxNode TCtxStack::getCurrentNode() const
73
{
74
  std::pair<Node, uint32_t> curr = TCtxStack::getCurrent();
75
  return TCtxNode(curr.first, curr.second, d_tctx);
76
}
77
78
26685
}  // namespace CVC4