diff options
Diffstat (limited to 'src/expr/term_context_stack.h')
-rw-r--r-- | src/expr/term_context_stack.h | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h new file mode 100644 index 000000000..9aeea04c2 --- /dev/null +++ b/src/expr/term_context_stack.h @@ -0,0 +1,68 @@ +/********************* */ +/*! \file term_context_stack.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Term context + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__TERM_CONTEXT_STACK_H +#define CVC4__EXPR__TERM_CONTEXT_STACK_H + +#include "expr/term_context_node.h" + +namespace CVC4 { + +/** + * A stack for term-context-sensitive terms. Its main advantage is that + * it does not rely on explicit construction of TCtxNode for efficiency. + */ +class TCtxStack +{ + public: + TCtxStack(const TermContext* tctx); + virtual ~TCtxStack() {} + /** Push t to the stack */ + void pushInitial(Node t); + /** + * Push all children of t to the stack, where tval is the term context hash + * of t. */ + void pushChildren(Node t, uint32_t tval); + /** + * Push the child of t with the given index to the stack, where tval is + * the term context hash of t. + */ + void pushChild(Node t, uint32_t tval, size_t index); + /** Push t to the stack with term context hash tval. */ + void push(Node t, uint32_t tval); + /** Pop a term from the context */ + void pop(); + /** Clear the stack */ + void clear(); + /** Return the size of the stack */ + size_t size() const; + /** Return true if the stack is empty */ + bool empty() const; + /** Get the current stack element */ + std::pair<Node, uint32_t> getCurrent() const; + /** Get the current stack element, node version */ + TCtxNode getCurrentNode() const; + + private: + /** The stack */ + std::vector<std::pair<Node, uint32_t>> d_stack; + /** The term context */ + const TermContext* d_tctx; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */ |