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 |
|
* Implementation of term context utilities. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/term_context.h" |
17 |
|
|
18 |
|
#include "theory/theory.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
|
uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const |
23 |
|
{ |
24 |
|
// default is no change |
25 |
|
return tval; |
26 |
|
} |
27 |
|
|
28 |
659970 |
uint32_t RtfTermContext::initialValue() const |
29 |
|
{ |
30 |
|
// by default, not in a term context or a quantifier |
31 |
659970 |
return 0; |
32 |
|
} |
33 |
|
|
34 |
4603450 |
uint32_t RtfTermContext::computeValue(TNode t, |
35 |
|
uint32_t tval, |
36 |
|
size_t child) const |
37 |
|
{ |
38 |
4603450 |
if (t.isClosure()) |
39 |
|
{ |
40 |
|
if (tval % 2 == 0) |
41 |
|
{ |
42 |
|
return tval + 1; |
43 |
|
} |
44 |
|
} |
45 |
4603450 |
else if (hasNestedTermChildren(t)) |
46 |
|
{ |
47 |
3101384 |
if (tval < 2) |
48 |
|
{ |
49 |
1758476 |
return tval + 2; |
50 |
|
} |
51 |
|
} |
52 |
2844974 |
return tval; |
53 |
|
} |
54 |
|
|
55 |
|
uint32_t RtfTermContext::getValue(bool inQuant, bool inTerm) |
56 |
|
{ |
57 |
|
return (inQuant ? 1 : 0) + 2 * (inTerm ? 1 : 0); |
58 |
|
} |
59 |
|
|
60 |
1327968 |
void RtfTermContext::getFlags(uint32_t val, bool& inQuant, bool& inTerm) |
61 |
|
{ |
62 |
1327968 |
inQuant = val % 2 == 1; |
63 |
1327968 |
inTerm = val >= 2; |
64 |
1327968 |
} |
65 |
|
|
66 |
4603450 |
bool RtfTermContext::hasNestedTermChildren(TNode t) |
67 |
|
{ |
68 |
4603450 |
Kind k = t.getKind(); |
69 |
|
// dont' worry about FORALL or EXISTS, these are part of inQuant. |
70 |
8973126 |
return theory::kindToTheoryId(k) != theory::THEORY_BOOL && k != kind::EQUAL |
71 |
3104396 |
&& k != kind::SEP_STAR && k != kind::SEP_WAND && k != kind::SEP_LABEL |
72 |
7705264 |
&& k != kind::BITVECTOR_EAGER_ATOM; |
73 |
|
} |
74 |
|
|
75 |
5520 |
uint32_t InQuantTermContext::initialValue() const { return 0; } |
76 |
|
|
77 |
427782 |
uint32_t InQuantTermContext::computeValue(TNode t, |
78 |
|
uint32_t tval, |
79 |
|
size_t index) const |
80 |
|
{ |
81 |
427782 |
return t.isClosure() ? 1 : tval; |
82 |
|
} |
83 |
|
|
84 |
|
uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; } |
85 |
|
|
86 |
|
bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant) |
87 |
|
{ |
88 |
|
return val == 1; |
89 |
|
} |
90 |
|
|
91 |
1079 |
uint32_t PolarityTermContext::initialValue() const |
92 |
|
{ |
93 |
|
// by default, we have true polarity |
94 |
1079 |
return 2; |
95 |
|
} |
96 |
|
|
97 |
99528 |
uint32_t PolarityTermContext::computeValue(TNode t, |
98 |
|
uint32_t tval, |
99 |
|
size_t index) const |
100 |
|
{ |
101 |
99528 |
switch (t.getKind()) |
102 |
|
{ |
103 |
10017 |
case kind::AND: |
104 |
|
case kind::OR: |
105 |
|
case kind::SEP_STAR: |
106 |
|
// polarity preserved |
107 |
10017 |
return tval; |
108 |
|
case kind::IMPLIES: |
109 |
|
// first child reverses, otherwise we preserve |
110 |
|
return index == 0 ? (tval == 0 ? 0 : (3 - tval)) : tval; |
111 |
8958 |
case kind::NOT: |
112 |
|
// polarity reversed |
113 |
8958 |
return tval == 0 ? 0 : (3 - tval); |
114 |
282 |
case kind::ITE: |
115 |
|
// head has no polarity, branches preserve |
116 |
282 |
return index == 0 ? 0 : tval; |
117 |
|
case kind::FORALL: |
118 |
|
// body preserves, others have no polarity. |
119 |
|
return index == 1 ? tval : 0; |
120 |
80271 |
default: |
121 |
|
// no polarity |
122 |
80271 |
break; |
123 |
|
} |
124 |
80271 |
return 0; |
125 |
|
} |
126 |
|
|
127 |
|
uint32_t PolarityTermContext::getValue(bool hasPol, bool pol) |
128 |
|
{ |
129 |
|
return hasPol ? (pol ? 2 : 1) : 0; |
130 |
|
} |
131 |
|
|
132 |
31179 |
void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol) |
133 |
|
{ |
134 |
31179 |
hasPol = val == 0; |
135 |
31179 |
pol = val == 2; |
136 |
31179 |
} |
137 |
|
|
138 |
6270 |
uint32_t TheoryLeafTermContext::initialValue() const { return 0; } |
139 |
|
|
140 |
39474 |
uint32_t TheoryLeafTermContext::computeValue(TNode t, |
141 |
|
uint32_t tval, |
142 |
|
size_t index) const |
143 |
|
{ |
144 |
39474 |
return theory::Theory::isLeafOf(t, d_theoryId) ? 1 : tval; |
145 |
|
} |
146 |
|
|
147 |
29502 |
} // namespace cvc5 |