1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 multi-linear inst match generator class. |
14 |
|
*/ |
15 |
|
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" |
16 |
|
|
17 |
|
#include "options/quantifiers_options.h" |
18 |
|
#include "theory/quantifiers/ematching/trigger_trie.h" |
19 |
|
#include "theory/quantifiers/term_util.h" |
20 |
|
|
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace quantifiers { |
26 |
|
namespace inst { |
27 |
|
|
28 |
1300 |
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( |
29 |
1300 |
Trigger* tparent, Node q, std::vector<Node>& pats) |
30 |
1300 |
: InstMatchGenerator(tparent, Node::null()) |
31 |
|
{ |
32 |
|
// order patterns to maximize eager matching failures |
33 |
2600 |
std::map<Node, std::vector<Node> > var_contains; |
34 |
4178 |
for (const Node& pat : pats) |
35 |
|
{ |
36 |
2878 |
TermUtil::computeInstConstContainsForQuant(q, pat, var_contains[pat]); |
37 |
|
} |
38 |
2600 |
std::map<Node, std::vector<Node> > var_to_node; |
39 |
4178 |
for (std::pair<const Node, std::vector<Node> >& vc : var_contains) |
40 |
|
{ |
41 |
8251 |
for (const Node& n : vc.second) |
42 |
|
{ |
43 |
5373 |
var_to_node[n].push_back(vc.first); |
44 |
|
} |
45 |
|
} |
46 |
2600 |
std::vector<Node> pats_ordered; |
47 |
2600 |
std::vector<bool> pats_ordered_independent; |
48 |
2600 |
std::map<Node, bool> var_bound; |
49 |
1300 |
size_t patsSize = pats.size(); |
50 |
7056 |
while (pats_ordered.size() < patsSize) |
51 |
|
{ |
52 |
|
// score is lexographic ( bound vars, shared vars ) |
53 |
2878 |
int score_max_1 = -1; |
54 |
2878 |
int score_max_2 = -1; |
55 |
2878 |
unsigned score_index = 0; |
56 |
2878 |
bool set_score_index = false; |
57 |
9618 |
for (size_t i = 0; i < patsSize; i++) |
58 |
|
{ |
59 |
13480 |
Node p = pats[i]; |
60 |
20220 |
if (std::find(pats_ordered.begin(), pats_ordered.end(), p) |
61 |
20220 |
== pats_ordered.end()) |
62 |
|
{ |
63 |
4809 |
int score_1 = 0; |
64 |
4809 |
int score_2 = 0; |
65 |
13516 |
for (unsigned j = 0; j < var_contains[p].size(); j++) |
66 |
|
{ |
67 |
17414 |
Node v = var_contains[p][j]; |
68 |
8707 |
if (var_bound.find(v) != var_bound.end()) |
69 |
|
{ |
70 |
818 |
score_1++; |
71 |
|
} |
72 |
7889 |
else if (var_to_node[v].size() > 1) |
73 |
|
{ |
74 |
1492 |
score_2++; |
75 |
|
} |
76 |
|
} |
77 |
4809 |
if (!set_score_index || score_1 > score_max_1 |
78 |
1817 |
|| (score_1 == score_max_1 && score_2 > score_max_2)) |
79 |
|
{ |
80 |
3022 |
score_index = i; |
81 |
3022 |
set_score_index = true; |
82 |
3022 |
score_max_1 = score_1; |
83 |
3022 |
score_max_2 = score_2; |
84 |
|
} |
85 |
|
} |
86 |
|
} |
87 |
2878 |
Assert(set_score_index); |
88 |
|
// update the variable bounds |
89 |
5756 |
Node mp = pats[score_index]; |
90 |
2878 |
std::vector<Node>& vcm = var_contains[mp]; |
91 |
8251 |
for (const Node& vc : vcm) |
92 |
|
{ |
93 |
5373 |
var_bound[vc] = true; |
94 |
|
} |
95 |
2878 |
pats_ordered.push_back(mp); |
96 |
2878 |
pats_ordered_independent.push_back(score_max_1 == 0); |
97 |
|
} |
98 |
|
|
99 |
2600 |
Trace("multi-trigger-linear") |
100 |
1300 |
<< "Make children for linear multi trigger." << std::endl; |
101 |
4178 |
for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++) |
102 |
|
{ |
103 |
5756 |
Node po = pats_ordered[i]; |
104 |
2878 |
Trace("multi-trigger-linear") << "...make for " << po << std::endl; |
105 |
2878 |
InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po); |
106 |
2878 |
Assert(cimg != nullptr); |
107 |
2878 |
d_children.push_back(cimg); |
108 |
|
// this could be improved |
109 |
2878 |
if (i == 0) |
110 |
|
{ |
111 |
1300 |
cimg->setIndependent(); |
112 |
|
} |
113 |
|
} |
114 |
1300 |
} |
115 |
|
|
116 |
7354 |
int InstMatchGeneratorMultiLinear::resetChildren() |
117 |
|
{ |
118 |
17364 |
for (InstMatchGenerator* c : d_children) |
119 |
|
{ |
120 |
12828 |
if (!c->reset(Node::null())) |
121 |
|
{ |
122 |
2818 |
return -2; |
123 |
|
} |
124 |
|
} |
125 |
4536 |
return 1; |
126 |
|
} |
127 |
|
|
128 |
10862 |
bool InstMatchGeneratorMultiLinear::reset(Node eqc) |
129 |
|
{ |
130 |
10862 |
Assert(eqc.isNull()); |
131 |
10862 |
if (options::multiTriggerLinear()) |
132 |
|
{ |
133 |
10862 |
return true; |
134 |
|
} |
135 |
|
return resetChildren() > 0; |
136 |
|
} |
137 |
|
|
138 |
7354 |
int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) |
139 |
|
{ |
140 |
14708 |
Trace("multi-trigger-linear-debug") |
141 |
7354 |
<< "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; |
142 |
7354 |
if (options::multiTriggerLinear()) |
143 |
|
{ |
144 |
|
// reset everyone |
145 |
7354 |
int rc_ret = resetChildren(); |
146 |
7354 |
if (rc_ret < 0) |
147 |
|
{ |
148 |
2818 |
return rc_ret; |
149 |
|
} |
150 |
|
} |
151 |
9072 |
Trace("multi-trigger-linear-debug") |
152 |
4536 |
<< "InstMatchGeneratorMultiLinear::getNextMatch : continue match " |
153 |
4536 |
<< std::endl; |
154 |
4536 |
Assert(d_next != nullptr); |
155 |
|
int ret_val = |
156 |
4536 |
continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL); |
157 |
4536 |
if (ret_val > 0) |
158 |
|
{ |
159 |
7412 |
Trace("multi-trigger-linear") |
160 |
3706 |
<< "Successful multi-trigger instantiation." << std::endl; |
161 |
3706 |
if (options::multiTriggerLinear()) |
162 |
|
{ |
163 |
|
// now, restrict everyone |
164 |
11311 |
for (size_t i = 0, csize = d_children.size(); i < csize; i++) |
165 |
|
{ |
166 |
15210 |
Node mi = d_children[i]->getCurrentMatch(); |
167 |
15210 |
Trace("multi-trigger-linear") |
168 |
7605 |
<< " child " << i << " match : " << mi << std::endl; |
169 |
7605 |
d_children[i]->excludeMatch(mi); |
170 |
|
} |
171 |
|
} |
172 |
|
} |
173 |
4536 |
return ret_val; |
174 |
|
} |
175 |
|
|
176 |
|
} // namespace inst |
177 |
|
} // namespace quantifiers |
178 |
|
} // namespace theory |
179 |
29577 |
} // namespace cvc5 |