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