diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-28 20:35:56 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 20:35:56 -0500 |
commit | 0675545dde7ed679b7045a37470148c7e1bdfd25 (patch) | |
tree | 3f397a984f57d30110d4027922aa2e5c1e822575 /src/expr/term_context_stack.h | |
parent | d48e117199b766a9a55eaf951d4d5ed80c9b8dc0 (diff) |
(proof-new) More term context utilities. (#4912)
These utilities will be used for making some of the core proof utilities term-context-sensitve.
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 */ |