GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_context_stack.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_context_stack.h
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
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__TERM_CONTEXT_STACK_H
18
#define CVC4__EXPR__TERM_CONTEXT_STACK_H
19
20
#include "expr/term_context_node.h"
21
22
namespace CVC4 {
23
24
/**
25
 * A stack for term-context-sensitive terms. Its main advantage is that
26
 * it does not rely on explicit construction of TCtxNode for efficiency.
27
 */
28
class TCtxStack
29
{
30
 public:
31
  TCtxStack(const TermContext* tctx);
32
552380
  virtual ~TCtxStack() {}
33
  /** Push t to the stack */
34
  void pushInitial(Node t);
35
  /**
36
   * Push all children of t to the stack, where tval is the term context hash
37
   * of t. */
38
  void pushChildren(Node t, uint32_t tval);
39
  /**
40
   * Push the child of t with the given index to the stack, where tval is
41
   * the term context hash of t.
42
   */
43
  void pushChild(Node t, uint32_t tval, size_t index);
44
  /**
45
   * Push the operator of t to the stack, where tval is the term context has
46
   * of t.
47
   */
48
  void pushOp(Node t, uint32_t tval);
49
  /** Push t to the stack with term context hash tval. */
50
  void push(Node t, uint32_t tval);
51
  /** Pop a term from the context */
52
  void pop();
53
  /** Clear the stack */
54
  void clear();
55
  /** Return the size of the stack */
56
  size_t size() const;
57
  /** Return true if the stack is empty */
58
  bool empty() const;
59
  /** Get the current stack element */
60
  std::pair<Node, uint32_t> getCurrent() const;
61
  /** Get the current stack element, node version */
62
  TCtxNode getCurrentNode() const;
63
64
 private:
65
  /** The stack */
66
  std::vector<std::pair<Node, uint32_t>> d_stack;
67
  /** The term context */
68
  const TermContext* d_tctx;
69
};
70
71
}  // namespace CVC4
72
73
#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */