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 |
|
namespace cvc5 { |
19 |
|
|
20 |
|
uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const |
21 |
|
{ |
22 |
|
// default is no change |
23 |
|
return tval; |
24 |
|
} |
25 |
|
|
26 |
577943 |
uint32_t RtfTermContext::initialValue() const |
27 |
|
{ |
28 |
|
// by default, not in a term context or a quantifier |
29 |
577943 |
return 0; |
30 |
|
} |
31 |
|
|
32 |
4772094 |
uint32_t RtfTermContext::computeValue(TNode t, |
33 |
|
uint32_t tval, |
34 |
|
size_t child) const |
35 |
|
{ |
36 |
4772094 |
if (t.isClosure()) |
37 |
|
{ |
38 |
|
if (tval % 2 == 0) |
39 |
|
{ |
40 |
|
return tval + 1; |
41 |
|
} |
42 |
|
} |
43 |
4772094 |
else if (hasNestedTermChildren(t)) |
44 |
|
{ |
45 |
2870276 |
if (tval < 2) |
46 |
|
{ |
47 |
1564098 |
return tval + 2; |
48 |
|
} |
49 |
|
} |
50 |
3207996 |
return tval; |
51 |
|
} |
52 |
|
|
53 |
|
uint32_t RtfTermContext::getValue(bool inQuant, bool inTerm) |
54 |
|
{ |
55 |
|
return (inQuant ? 1 : 0) + 2 * (inTerm ? 1 : 0); |
56 |
|
} |
57 |
|
|
58 |
1217798 |
void RtfTermContext::getFlags(uint32_t val, bool& inQuant, bool& inTerm) |
59 |
|
{ |
60 |
1217798 |
inQuant = val % 2 == 1; |
61 |
1217798 |
inTerm = val >= 2; |
62 |
1217798 |
} |
63 |
|
|
64 |
4772094 |
bool RtfTermContext::hasNestedTermChildren(TNode t) |
65 |
|
{ |
66 |
4772094 |
Kind k = t.getKind(); |
67 |
|
// dont' worry about FORALL or EXISTS, these are part of inQuant. |
68 |
8850188 |
return theory::kindToTheoryId(k) != theory::THEORY_BOOL && k != kind::EQUAL |
69 |
2873394 |
&& k != kind::SEP_STAR && k != kind::SEP_WAND && k != kind::SEP_LABEL |
70 |
7642906 |
&& k != kind::BITVECTOR_EAGER_ATOM; |
71 |
|
} |
72 |
|
|
73 |
5518 |
uint32_t InQuantTermContext::initialValue() const { return 0; } |
74 |
|
|
75 |
456198 |
uint32_t InQuantTermContext::computeValue(TNode t, |
76 |
|
uint32_t tval, |
77 |
|
size_t index) const |
78 |
|
{ |
79 |
456198 |
return t.isClosure() ? 1 : tval; |
80 |
|
} |
81 |
|
|
82 |
|
uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; } |
83 |
|
|
84 |
|
bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant) |
85 |
|
{ |
86 |
|
return val == 1; |
87 |
|
} |
88 |
|
|
89 |
1520 |
uint32_t PolarityTermContext::initialValue() const |
90 |
|
{ |
91 |
|
// by default, we have true polarity |
92 |
1520 |
return 2; |
93 |
|
} |
94 |
|
|
95 |
104619 |
uint32_t PolarityTermContext::computeValue(TNode t, |
96 |
|
uint32_t tval, |
97 |
|
size_t index) const |
98 |
|
{ |
99 |
104619 |
switch (t.getKind()) |
100 |
|
{ |
101 |
10219 |
case kind::AND: |
102 |
|
case kind::OR: |
103 |
|
case kind::SEP_STAR: |
104 |
|
// polarity preserved |
105 |
10219 |
return tval; |
106 |
|
case kind::IMPLIES: |
107 |
|
// first child reverses, otherwise we preserve |
108 |
|
return index == 0 ? (tval == 0 ? 0 : (3 - tval)) : tval; |
109 |
9071 |
case kind::NOT: |
110 |
|
// polarity reversed |
111 |
9071 |
return tval == 0 ? 0 : (3 - tval); |
112 |
1185 |
case kind::ITE: |
113 |
|
// head has no polarity, branches preserve |
114 |
1185 |
return index == 0 ? 0 : tval; |
115 |
|
case kind::FORALL: |
116 |
|
// body preserves, others have no polarity. |
117 |
|
return index == 1 ? tval : 0; |
118 |
84144 |
default: |
119 |
|
// no polarity |
120 |
84144 |
break; |
121 |
|
} |
122 |
84144 |
return 0; |
123 |
|
} |
124 |
|
|
125 |
|
uint32_t PolarityTermContext::getValue(bool hasPol, bool pol) |
126 |
|
{ |
127 |
|
return hasPol ? (pol ? 2 : 1) : 0; |
128 |
|
} |
129 |
|
|
130 |
35486 |
void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol) |
131 |
|
{ |
132 |
35486 |
hasPol = val == 0; |
133 |
35486 |
pol = val == 2; |
134 |
35486 |
} |
135 |
|
|
136 |
28191 |
} // namespace cvc5 |