1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Term context node utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/term_context_node.h" |
17 |
|
|
18 |
|
#include "expr/term_context.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
|
TCtxNode::TCtxNode(Node n, const TermContext* tctx) |
23 |
|
: d_node(n), d_val(tctx->initialValue()), d_tctx(tctx) |
24 |
|
{ |
25 |
|
} |
26 |
|
|
27 |
|
TCtxNode::TCtxNode(Node n, uint32_t val, const TermContext* tctx) |
28 |
|
: d_node(n), d_val(val), d_tctx(tctx) |
29 |
|
{ |
30 |
|
} |
31 |
|
|
32 |
|
size_t TCtxNode::getNumChildren() const { return d_node.getNumChildren(); } |
33 |
|
|
34 |
|
TCtxNode TCtxNode::getChild(size_t i) const |
35 |
|
{ |
36 |
|
Assert(i < d_node.getNumChildren()); |
37 |
|
// we are still computing the same term context, with the given child, where |
38 |
|
// the hash has been updated based on the kind, node, current value and child |
39 |
|
// index. |
40 |
|
return TCtxNode(d_node[i], d_tctx->computeValue(d_node, d_val, i), d_tctx); |
41 |
|
} |
42 |
|
|
43 |
|
Node TCtxNode::getNode() const { return d_node; } |
44 |
|
|
45 |
|
uint32_t TCtxNode::getContextId() const { return d_val; } |
46 |
|
|
47 |
|
const TermContext* TCtxNode::getTermContext() const { return d_tctx; } |
48 |
|
|
49 |
|
Node TCtxNode::getNodeHash() const { return computeNodeHash(d_node, d_val); } |
50 |
|
|
51 |
1795675 |
Node TCtxNode::computeNodeHash(Node n, uint32_t val) |
52 |
|
{ |
53 |
1795675 |
NodeManager* nm = NodeManager::currentNM(); |
54 |
1795675 |
return nm->mkNode(kind::SEXPR, n, nm->mkConst(Rational(val))); |
55 |
|
} |
56 |
|
|
57 |
|
Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val) |
58 |
|
{ |
59 |
|
if (h.getKind() != kind::SEXPR || h.getNumChildren() != 2) |
60 |
|
{ |
61 |
|
Assert(false) << "TermContext::decomposeNodeHash: unexpected node " << h; |
62 |
|
return Node::null(); |
63 |
|
} |
64 |
|
Node ival = h[1]; |
65 |
|
if (!ival.isConst() || !ival.getType().isInteger() |
66 |
|
|| !ival.getConst<Rational>().getNumerator().fitsUnsignedInt()) |
67 |
|
{ |
68 |
|
Assert(false) << "TermContext::decomposeNodeHash: unexpected term context " |
69 |
|
"integer in hash " |
70 |
|
<< h; |
71 |
|
return Node::null(); |
72 |
|
} |
73 |
|
val = ival.getConst<Rational>().getNumerator().toUnsignedInt(); |
74 |
|
return h[0]; |
75 |
|
} |
76 |
|
|
77 |
28194 |
} // namespace cvc5 |