From: Andrew Reynolds Date: Sat, 29 Aug 2020 01:35:56 +0000 (-0500) Subject: (proof-new) More term context utilities. (#4912) X-Git-Tag: cvc5-1.0.0~2937 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0675545dde7ed679b7045a37470148c7e1bdfd25;p=cvc5.git (proof-new) More term context utilities. (#4912) These utilities will be used for making some of the core proof utilities term-context-sensitve. --- diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp new file mode 100644 index 000000000..519012ae8 --- /dev/null +++ b/src/expr/term_context_node.cpp @@ -0,0 +1,76 @@ +/********************* */ +/*! \file term_context_node.cpp + ** \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 node utility. + **/ + +#include "expr/term_context_node.h" + +#include "expr/term_context.h" + +namespace CVC4 { + +TCtxNode::TCtxNode(Node n, const TermContext* tctx) + : d_node(n), d_val(tctx->initialValue()), d_tctx(tctx) +{ +} + +TCtxNode::TCtxNode(Node n, uint32_t val, const TermContext* tctx) + : d_node(n), d_val(val), d_tctx(tctx) +{ +} + +size_t TCtxNode::getNumChildren() const { return d_node.getNumChildren(); } + +TCtxNode TCtxNode::getChild(size_t i) const +{ + Assert(i < d_node.getNumChildren()); + // we are still computing the same term context, with the given child, where + // the hash has been updated based on the kind, node, current value and child + // index. + return TCtxNode(d_node[i], d_tctx->computeValue(d_node, d_val, i), d_tctx); +} + +Node TCtxNode::getNode() const { return d_node; } + +uint32_t TCtxNode::getContextId() const { return d_val; } + +const TermContext* TCtxNode::getTermContext() const { return d_tctx; } + +Node TCtxNode::getNodeHash() const { return computeNodeHash(d_node, d_val); } + +Node TCtxNode::computeNodeHash(Node n, uint32_t val) +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::SEXPR, n, nm->mkConst(Rational(val))); +} + +Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val) +{ + if (h.getKind() != kind::SEXPR || h.getNumChildren() != 2) + { + Assert(false) << "TermContext::decomposeNodeHash: unexpected node " << h; + return Node::null(); + } + Node ival = h[1]; + if (!ival.isConst() || !ival.getType().isInteger() + || !ival.getConst().getNumerator().fitsUnsignedInt()) + { + Assert(false) << "TermContext::decomposeNodeHash: unexpected term context " + "integer in hash " + << h; + return Node::null(); + } + val = ival.getConst().getNumerator().toUnsignedInt(); + return h[0]; +} + +} // namespace CVC4 diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h new file mode 100644 index 000000000..028a590b1 --- /dev/null +++ b/src/expr/term_context_node.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file term_context.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 node utility. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__TERM_CONTEXT_NODE_H +#define CVC4__EXPR__TERM_CONTEXT_NODE_H + +#include "expr/node.h" +#include "expr/term_context.h" + +namespace CVC4 { + +class TCtxStack; + +/** + * A (term-context) sensitive term. This is a wrapper around a Node that + * additionally has a term context identifier, see getTermContext(). It depends + * on a pointer to a TermContext callback class (see term_context.h). + */ +class TCtxNode +{ + friend class TCtxStack; + + public: + TCtxNode(Node n, const TermContext* tctx); + /** get number of children */ + size_t getNumChildren() const; + /** get child at index i */ + TCtxNode getChild(size_t i) const; + /** get node */ + Node getNode() const; + /** get context */ + uint32_t getContextId() const; + /** get term context */ + const TermContext* getTermContext() const; + //---------------------- utility methods + /** + * Get node hash, which is a unique node representation of this TCtxNode. + * This method calls the method below on the data members of this class. + */ + Node getNodeHash() const; + /** + * Get node hash, which is a unique node representation of the pair (n, val). + * In particular, this returns (SEXPR n (CONST_RATIONAL val)). + */ + static Node computeNodeHash(Node n, uint32_t val); + /** + * Decompose node hash, which is an inverse of the above operation. In + * particular, given input h, this returns a node n and sets val to a value + * such that computeNodeHash(n, val) returns h. + */ + static Node decomposeNodeHash(Node h, uint32_t& val); + //---------------------- end utility methods + private: + /** private constructor */ + TCtxNode(Node n, uint32_t val, const TermContext* tctx); + /** The node */ + Node d_node; + /** The term context identifier */ + uint32_t d_val; + /** The term context */ + const TermContext* d_tctx; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp new file mode 100644 index 000000000..4c2e32033 --- /dev/null +++ b/src/expr/term_context_stack.cpp @@ -0,0 +1,69 @@ +/********************* */ +/*! \file term_context_stack.cpp + ** \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 stack + **/ + +#include "expr/term_context_stack.h" + +namespace CVC4 { + +TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {} + +void TCtxStack::pushInitial(Node t) +{ + Assert(d_stack.empty()); + d_stack.push_back(std::pair(t, d_tctx->initialValue())); +} + +void TCtxStack::pushChildren(Node t, uint32_t tval) +{ + for (size_t i = 0, nchild = t.getNumChildren(); i < nchild; i++) + { + pushChild(t, tval, i); + } +} + +void TCtxStack::pushChild(Node t, uint32_t tval, size_t index) +{ + Assert(index < t.getNumChildren()); + Trace("tctx-debug") << "TCtxStack::pushChild: computing " << t << "[" << index + << "] / " << tval << std::endl; + uint32_t tcval = d_tctx->computeValue(t, tval, index); + Trace("tctx-debug") << "TCtxStack::pushChild: returned " << t << "[" << index + << "] / " << tval << " ---> " << tcval << std::endl; + d_stack.push_back(std::pair(t[index], tcval)); +} + +void TCtxStack::push(Node t, uint32_t tval) +{ + d_stack.push_back(std::pair(t, tval)); +} + +void TCtxStack::pop() { d_stack.pop_back(); } + +void TCtxStack::clear() { d_stack.clear(); } +size_t TCtxStack::size() const { return d_stack.size(); } + +bool TCtxStack::empty() const { return d_stack.empty(); } + +std::pair TCtxStack::getCurrent() const +{ + return d_stack.back(); +} + +TCtxNode TCtxStack::getCurrentNode() const +{ + std::pair curr = TCtxStack::getCurrent(); + return TCtxNode(curr.first, curr.second, d_tctx); +} + +} // namespace CVC4 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 getCurrent() const; + /** Get the current stack element, node version */ + TCtxNode getCurrentNode() const; + + private: + /** The stack */ + std::vector> d_stack; + /** The term context */ + const TermContext* d_tctx; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */