1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Yoni Zohar |
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 trigger term info class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/ematching/trigger_term_info.h" |
17 |
|
|
18 |
|
#include "theory/quantifiers/term_util.h" |
19 |
|
|
20 |
|
using namespace cvc5::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace quantifiers { |
25 |
|
namespace inst { |
26 |
|
|
27 |
94017 |
void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq) |
28 |
|
{ |
29 |
94017 |
if (d_fv.empty()) |
30 |
|
{ |
31 |
93523 |
quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv); |
32 |
|
} |
33 |
94017 |
if (d_reqPol == 0) |
34 |
|
{ |
35 |
93899 |
d_reqPol = reqPol; |
36 |
93899 |
d_reqPolEq = reqPolEq; |
37 |
|
} |
38 |
|
else |
39 |
|
{ |
40 |
|
// determined a ground (dis)equality must hold or else q is a tautology? |
41 |
|
} |
42 |
94017 |
d_weight = getTriggerWeight(n); |
43 |
94017 |
} |
44 |
|
|
45 |
3747863 |
bool TriggerTermInfo::isAtomicTrigger(Node n) |
46 |
|
{ |
47 |
3747863 |
return isAtomicTriggerKind(n.getKind()); |
48 |
|
} |
49 |
|
|
50 |
11027332 |
bool TriggerTermInfo::isAtomicTriggerKind(Kind k) |
51 |
|
{ |
52 |
|
// we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this |
53 |
|
// method is used both for trigger selection and for ground term registration, |
54 |
|
// where these two things require those kinds respectively. |
55 |
4197147 |
return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR |
56 |
2524034 |
|| k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL |
57 |
2445030 |
|| k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET |
58 |
2364962 |
|| k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO |
59 |
2325585 |
|| k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY |
60 |
13332741 |
|| k == STRING_LENGTH || k == SEQ_NTH; |
61 |
|
} |
62 |
|
|
63 |
368414 |
bool TriggerTermInfo::isRelationalTrigger(Node n) |
64 |
|
{ |
65 |
368414 |
return isRelationalTriggerKind(n.getKind()); |
66 |
|
} |
67 |
|
|
68 |
368414 |
bool TriggerTermInfo::isRelationalTriggerKind(Kind k) |
69 |
|
{ |
70 |
368414 |
return k == EQUAL || k == GEQ; |
71 |
|
} |
72 |
|
|
73 |
22753 |
bool TriggerTermInfo::isUsableRelationTrigger(Node n) |
74 |
|
{ |
75 |
|
bool hasPol, pol; |
76 |
45506 |
Node lit; |
77 |
45506 |
return isUsableRelationTrigger(n, hasPol, pol, lit); |
78 |
|
} |
79 |
58451 |
bool TriggerTermInfo::isUsableRelationTrigger(Node n, |
80 |
|
bool& hasPol, |
81 |
|
bool& pol, |
82 |
|
Node& lit) |
83 |
|
{ |
84 |
|
// relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }. |
85 |
58451 |
hasPol = false; |
86 |
58451 |
pol = n.getKind() != NOT; |
87 |
58451 |
lit = pol ? n : n[0]; |
88 |
121771 |
if (lit.getKind() == EQUAL && lit[1].getType().isBoolean() |
89 |
118587 |
&& lit[1].isConst()) |
90 |
|
{ |
91 |
1685 |
hasPol = true; |
92 |
1685 |
pol = lit[1].getConst<bool>() ? pol : !pol; |
93 |
1685 |
lit = lit[0]; |
94 |
|
} |
95 |
|
// is it a relational trigger? |
96 |
120086 |
if ((lit.getKind() == EQUAL && lit[0].getType().isReal()) |
97 |
175281 |
|| lit.getKind() == GEQ) |
98 |
|
{ |
99 |
|
// if one side of the relation is a variable and the other side is a ground |
100 |
|
// term, we can treat this using the relational match generator |
101 |
2039 |
for (size_t i = 0; i < 2; i++) |
102 |
|
{ |
103 |
4140 |
if (lit[i].getKind() == INST_CONSTANT |
104 |
4140 |
&& !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i])) |
105 |
|
{ |
106 |
62 |
return true; |
107 |
|
} |
108 |
|
} |
109 |
|
} |
110 |
58389 |
return false; |
111 |
|
} |
112 |
|
|
113 |
24494 |
bool TriggerTermInfo::isSimpleTrigger(Node n) |
114 |
|
{ |
115 |
48988 |
Node t = n.getKind() == NOT ? n[0] : n; |
116 |
24494 |
if (t.getKind() == EQUAL) |
117 |
|
{ |
118 |
3019 |
if (!quantifiers::TermUtil::hasInstConstAttr(t[1])) |
119 |
|
{ |
120 |
3001 |
t = t[0]; |
121 |
|
} |
122 |
|
} |
123 |
24494 |
if (!isAtomicTrigger(t)) |
124 |
|
{ |
125 |
96 |
return false; |
126 |
|
} |
127 |
62560 |
for (const Node& tc : t) |
128 |
|
{ |
129 |
92572 |
if (tc.getKind() != INST_CONSTANT |
130 |
92572 |
&& quantifiers::TermUtil::hasInstConstAttr(tc)) |
131 |
|
{ |
132 |
8124 |
return false; |
133 |
|
} |
134 |
|
} |
135 |
16274 |
if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT) |
136 |
|
{ |
137 |
12 |
return false; |
138 |
|
} |
139 |
16262 |
return true; |
140 |
|
} |
141 |
|
|
142 |
170584 |
int32_t TriggerTermInfo::getTriggerWeight(Node n) |
143 |
|
{ |
144 |
170584 |
if (n.getKind() == APPLY_UF) |
145 |
|
{ |
146 |
134428 |
return 0; |
147 |
|
} |
148 |
36156 |
if (isAtomicTrigger(n) || isUsableRelationTrigger(n)) |
149 |
|
{ |
150 |
13511 |
return 1; |
151 |
|
} |
152 |
22645 |
return 2; |
153 |
|
} |
154 |
|
|
155 |
|
} // namespace inst |
156 |
|
} // namespace quantifiers |
157 |
|
} // namespace theory |
158 |
31137 |
} // namespace cvc5 |