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 |
35116 |
void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq) |
28 |
|
{ |
29 |
35116 |
if (d_fv.empty()) |
30 |
|
{ |
31 |
34938 |
quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv); |
32 |
|
} |
33 |
35116 |
if (d_reqPol == 0) |
34 |
|
{ |
35 |
35074 |
d_reqPol = reqPol; |
36 |
35074 |
d_reqPolEq = reqPolEq; |
37 |
|
} |
38 |
|
else |
39 |
|
{ |
40 |
|
// determined a ground (dis)equality must hold or else q is a tautology? |
41 |
|
} |
42 |
35116 |
d_weight = getTriggerWeight(n); |
43 |
35116 |
} |
44 |
|
|
45 |
1546452 |
bool TriggerTermInfo::isAtomicTrigger(Node n) |
46 |
|
{ |
47 |
1546452 |
return isAtomicTriggerKind(n.getKind()); |
48 |
|
} |
49 |
|
|
50 |
3607069 |
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 |
1601545 |
return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR |
56 |
1047383 |
|| k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL |
57 |
1021141 |
|| k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET |
58 |
980083 |
|| k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO |
59 |
968626 |
|| k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY |
60 |
4556842 |
|| k == STRING_LENGTH || k == SEQ_NTH; |
61 |
|
} |
62 |
|
|
63 |
138788 |
bool TriggerTermInfo::isRelationalTrigger(Node n) |
64 |
|
{ |
65 |
138788 |
return isRelationalTriggerKind(n.getKind()); |
66 |
|
} |
67 |
|
|
68 |
138788 |
bool TriggerTermInfo::isRelationalTriggerKind(Kind k) |
69 |
|
{ |
70 |
138788 |
return k == EQUAL || k == GEQ; |
71 |
|
} |
72 |
|
|
73 |
8321 |
bool TriggerTermInfo::isSimpleTrigger(Node n) |
74 |
|
{ |
75 |
16642 |
Node t = n.getKind() == NOT ? n[0] : n; |
76 |
8321 |
if (t.getKind() == EQUAL) |
77 |
|
{ |
78 |
1092 |
if (!quantifiers::TermUtil::hasInstConstAttr(t[1])) |
79 |
|
{ |
80 |
1087 |
t = t[0]; |
81 |
|
} |
82 |
|
} |
83 |
8321 |
if (!isAtomicTrigger(t)) |
84 |
|
{ |
85 |
25 |
return false; |
86 |
|
} |
87 |
20126 |
for (const Node& tc : t) |
88 |
|
{ |
89 |
29770 |
if (tc.getKind() != INST_CONSTANT |
90 |
29770 |
&& quantifiers::TermUtil::hasInstConstAttr(tc)) |
91 |
|
{ |
92 |
3055 |
return false; |
93 |
|
} |
94 |
|
} |
95 |
5241 |
if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT) |
96 |
|
{ |
97 |
3 |
return false; |
98 |
|
} |
99 |
5238 |
return true; |
100 |
|
} |
101 |
|
|
102 |
63255 |
int32_t TriggerTermInfo::getTriggerWeight(Node n) |
103 |
|
{ |
104 |
63255 |
if (n.getKind() == APPLY_UF) |
105 |
|
{ |
106 |
50519 |
return 0; |
107 |
|
} |
108 |
12736 |
if (isAtomicTrigger(n)) |
109 |
|
{ |
110 |
4585 |
return 1; |
111 |
|
} |
112 |
8151 |
return 2; |
113 |
|
} |
114 |
|
|
115 |
|
} // namespace inst |
116 |
|
} // namespace quantifiers |
117 |
|
} // namespace theory |
118 |
22746 |
} // namespace cvc5 |