1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Andrew Reynolds, Morgan Deters |
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 |
|
* The MIPLIB trick preprocessing pass. |
14 |
|
* |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "preprocessing/passes/miplib_trick.h" |
18 |
|
|
19 |
|
#include <sstream> |
20 |
|
#include <vector> |
21 |
|
|
22 |
|
#include "expr/node_self_iterator.h" |
23 |
|
#include "expr/skolem_manager.h" |
24 |
|
#include "options/arith_options.h" |
25 |
|
#include "options/base_options.h" |
26 |
|
#include "preprocessing/assertion_pipeline.h" |
27 |
|
#include "preprocessing/preprocessing_pass_context.h" |
28 |
|
#include "smt/smt_statistics_registry.h" |
29 |
|
#include "smt_util/boolean_simplification.h" |
30 |
|
#include "theory/booleans/circuit_propagator.h" |
31 |
|
#include "theory/theory_engine.h" |
32 |
|
#include "theory/theory_model.h" |
33 |
|
#include "theory/trust_substitutions.h" |
34 |
|
#include "util/rational.h" |
35 |
|
|
36 |
|
namespace cvc5 { |
37 |
|
namespace preprocessing { |
38 |
|
namespace passes { |
39 |
|
|
40 |
|
using namespace std; |
41 |
|
using namespace cvc5::theory; |
42 |
|
|
43 |
|
namespace { |
44 |
|
|
45 |
|
/** |
46 |
|
* Trace nodes back to their assertions using CircuitPropagator's |
47 |
|
* BackEdgesMap. |
48 |
|
*/ |
49 |
16312 |
void traceBackToAssertions(booleans::CircuitPropagator* propagator, |
50 |
|
const std::vector<Node>& nodes, |
51 |
|
std::vector<TNode>& assertions) |
52 |
|
{ |
53 |
|
const booleans::CircuitPropagator::BackEdgesMap& backEdges = |
54 |
16312 |
propagator->getBackEdges(); |
55 |
48636 |
for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) |
56 |
|
{ |
57 |
|
booleans::CircuitPropagator::BackEdgesMap::const_iterator j = |
58 |
32324 |
backEdges.find(*i); |
59 |
|
// term must appear in map, otherwise how did we get here?! |
60 |
32324 |
Assert(j != backEdges.end()); |
61 |
|
// if term maps to empty, that means it's a top-level assertion |
62 |
32324 |
if (!(*j).second.empty()) |
63 |
|
{ |
64 |
16036 |
traceBackToAssertions(propagator, (*j).second, assertions); |
65 |
|
} |
66 |
|
else |
67 |
|
{ |
68 |
16288 |
assertions.push_back(*i); |
69 |
|
} |
70 |
|
} |
71 |
16312 |
} |
72 |
|
|
73 |
|
} // namespace |
74 |
|
|
75 |
15338 |
MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) |
76 |
|
: PreprocessingPass(preprocContext, "miplib-trick"), |
77 |
15338 |
d_statistics(statisticsRegistry()) |
78 |
|
{ |
79 |
15338 |
} |
80 |
|
|
81 |
30666 |
MipLibTrick::~MipLibTrick() |
82 |
|
{ |
83 |
30666 |
} |
84 |
|
|
85 |
|
/** |
86 |
|
* Remove conjuncts in toRemove from conjunction n. Return # of removed |
87 |
|
* conjuncts. |
88 |
|
*/ |
89 |
8 |
size_t MipLibTrick::removeFromConjunction( |
90 |
|
Node& n, const std::unordered_set<unsigned long>& toRemove) |
91 |
|
{ |
92 |
8 |
Assert(n.getKind() == kind::AND); |
93 |
16 |
Node trueNode = NodeManager::currentNM()->mkConst(true); |
94 |
8 |
size_t removals = 0; |
95 |
2488 |
for (Node::iterator j = n.begin(); j != n.end(); ++j) |
96 |
|
{ |
97 |
2484 |
size_t subremovals = 0; |
98 |
4964 |
Node sub = *j; |
99 |
4968 |
if (toRemove.find(sub.getId()) != toRemove.end() |
100 |
2488 |
|| (sub.getKind() == kind::AND |
101 |
|
&& (subremovals = removeFromConjunction(sub, toRemove)) > 0)) |
102 |
|
{ |
103 |
8 |
NodeBuilder b(kind::AND); |
104 |
4 |
b.append(n.begin(), j); |
105 |
4 |
if (subremovals > 0) |
106 |
|
{ |
107 |
|
removals += subremovals; |
108 |
|
b << sub; |
109 |
|
} |
110 |
|
else |
111 |
|
{ |
112 |
4 |
++removals; |
113 |
|
} |
114 |
3136 |
for (++j; j != n.end(); ++j) |
115 |
|
{ |
116 |
3132 |
if (toRemove.find((*j).getId()) != toRemove.end()) |
117 |
|
{ |
118 |
3132 |
++removals; |
119 |
|
} |
120 |
|
else if ((*j).getKind() == kind::AND) |
121 |
|
{ |
122 |
|
sub = *j; |
123 |
|
if ((subremovals = removeFromConjunction(sub, toRemove)) > 0) |
124 |
|
{ |
125 |
|
removals += subremovals; |
126 |
|
b << sub; |
127 |
|
} |
128 |
|
else |
129 |
|
{ |
130 |
|
b << *j; |
131 |
|
} |
132 |
|
} |
133 |
|
else |
134 |
|
{ |
135 |
|
b << *j; |
136 |
|
} |
137 |
|
} |
138 |
4 |
if (b.getNumChildren() == 0) |
139 |
|
{ |
140 |
|
n = trueNode; |
141 |
|
b.clear(); |
142 |
|
} |
143 |
4 |
else if (b.getNumChildren() == 1) |
144 |
|
{ |
145 |
|
n = b[0]; |
146 |
|
b.clear(); |
147 |
|
} |
148 |
|
else |
149 |
|
{ |
150 |
4 |
n = b; |
151 |
|
} |
152 |
4 |
n = rewrite(n); |
153 |
4 |
return removals; |
154 |
|
} |
155 |
|
} |
156 |
|
|
157 |
4 |
Assert(removals == 0); |
158 |
4 |
return 0; |
159 |
|
} |
160 |
|
|
161 |
12 |
void MipLibTrick::collectBooleanVariables( |
162 |
|
AssertionPipeline* assertionsToPreprocess) |
163 |
|
{ |
164 |
12 |
d_boolVars.clear(); |
165 |
24 |
std::unordered_set<TNode> visited; |
166 |
12 |
std::unordered_set<TNode>::iterator it; |
167 |
24 |
std::vector<TNode> visit; |
168 |
24 |
TNode cur; |
169 |
120 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
170 |
|
{ |
171 |
108 |
visit.push_back((*assertionsToPreprocess)[i]); |
172 |
|
} |
173 |
37424 |
do |
174 |
|
{ |
175 |
37436 |
cur = visit.back(); |
176 |
37436 |
visit.pop_back(); |
177 |
37436 |
it = visited.find(cur); |
178 |
|
|
179 |
37436 |
if (it == visited.end()) |
180 |
|
{ |
181 |
11730 |
visited.insert(cur); |
182 |
11730 |
if (cur.isVar() && cur.getType().isBoolean()) |
183 |
|
{ |
184 |
276 |
d_boolVars.push_back(cur); |
185 |
|
} |
186 |
11730 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
187 |
|
} |
188 |
37436 |
} while (!visit.empty()); |
189 |
12 |
} |
190 |
|
|
191 |
12 |
PreprocessingPassResult MipLibTrick::applyInternal( |
192 |
|
AssertionPipeline* assertionsToPreprocess) |
193 |
|
{ |
194 |
12 |
Assert(assertionsToPreprocess->getRealAssertionsEnd() |
195 |
|
== assertionsToPreprocess->size()); |
196 |
12 |
Assert(!options().base.incrementalSolving); |
197 |
|
|
198 |
|
// collect Boolean variables |
199 |
12 |
collectBooleanVariables(assertionsToPreprocess); |
200 |
|
|
201 |
24 |
context::Context fakeContext; |
202 |
12 |
TheoryEngine* te = d_preprocContext->getTheoryEngine(); |
203 |
|
booleans::CircuitPropagator* propagator = |
204 |
12 |
d_preprocContext->getCircuitPropagator(); |
205 |
|
const booleans::CircuitPropagator::BackEdgesMap& backEdges = |
206 |
12 |
propagator->getBackEdges(); |
207 |
24 |
unordered_set<unsigned long> removeAssertions; |
208 |
|
|
209 |
|
theory::TrustSubstitutionMap& tlsm = |
210 |
12 |
d_preprocContext->getTopLevelSubstitutions(); |
211 |
12 |
SubstitutionMap& top_level_substs = tlsm.get(); |
212 |
|
|
213 |
12 |
NodeManager* nm = NodeManager::currentNM(); |
214 |
12 |
SkolemManager* sm = nm->getSkolemManager(); |
215 |
24 |
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); |
216 |
24 |
Node trueNode = nm->mkConst(true); |
217 |
|
|
218 |
24 |
unordered_map<TNode, Node> intVars; |
219 |
288 |
for (TNode v0 : d_boolVars) |
220 |
|
{ |
221 |
276 |
if (propagator->isAssigned(v0)) |
222 |
|
{ |
223 |
|
Debug("miplib") << "ineligible: " << v0 << " because assigned " |
224 |
|
<< propagator->getAssignment(v0) << endl; |
225 |
|
continue; |
226 |
|
} |
227 |
|
|
228 |
552 |
vector<TNode> assertions; |
229 |
|
booleans::CircuitPropagator::BackEdgesMap::const_iterator j0 = |
230 |
276 |
backEdges.find(v0); |
231 |
|
// if not in back edges map, the bool var is unconstrained, showing up in no |
232 |
|
// assertions. if maps to an empty vector, that means the bool var was |
233 |
|
// asserted itself. |
234 |
276 |
if (j0 != backEdges.end()) |
235 |
|
{ |
236 |
276 |
if (!(*j0).second.empty()) |
237 |
|
{ |
238 |
276 |
traceBackToAssertions(propagator, (*j0).second, assertions); |
239 |
|
} |
240 |
|
else |
241 |
|
{ |
242 |
|
assertions.push_back(v0); |
243 |
|
} |
244 |
|
} |
245 |
276 |
Debug("miplib") << "for " << v0 << endl; |
246 |
276 |
bool eligible = true; |
247 |
552 |
map<pair<Node, Node>, uint64_t> marks; |
248 |
552 |
map<pair<Node, Node>, vector<Rational> > coef; |
249 |
552 |
map<pair<Node, Node>, vector<Rational> > checks; |
250 |
552 |
map<pair<Node, Node>, vector<TNode> > asserts; |
251 |
16532 |
for (vector<TNode>::const_iterator j1 = assertions.begin(); |
252 |
16532 |
j1 != assertions.end(); |
253 |
|
++j1) |
254 |
|
{ |
255 |
16260 |
Debug("miplib") << " found: " << *j1 << endl; |
256 |
16260 |
if ((*j1).getKind() != kind::IMPLIES) |
257 |
|
{ |
258 |
|
eligible = false; |
259 |
|
Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl; |
260 |
4 |
break; |
261 |
|
} |
262 |
32516 |
Node conj = BooleanSimplification::simplify((*j1)[0]); |
263 |
16260 |
if (conj.getKind() == kind::AND && conj.getNumChildren() > 6) |
264 |
|
{ |
265 |
|
eligible = false; |
266 |
|
Debug("miplib") << " -- INELIGIBLE -- (N-ary /\\ too big)" << endl; |
267 |
|
break; |
268 |
|
} |
269 |
33032 |
if (conj.getKind() != kind::AND && !conj.isVar() |
270 |
32776 |
&& !(conj.getKind() == kind::NOT && conj[0].isVar())) |
271 |
|
{ |
272 |
|
eligible = false; |
273 |
|
Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl; |
274 |
|
break; |
275 |
|
} |
276 |
48780 |
if ((*j1)[1].getKind() != kind::EQUAL |
277 |
65040 |
|| !(((*j1)[1][0].isVar() |
278 |
32520 |
&& (*j1)[1][1].getKind() == kind::CONST_RATIONAL) |
279 |
16260 |
|| ((*j1)[1][0].getKind() == kind::CONST_RATIONAL |
280 |
16260 |
&& (*j1)[1][1].isVar()))) |
281 |
|
{ |
282 |
|
eligible = false; |
283 |
|
Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; |
284 |
|
break; |
285 |
|
} |
286 |
16260 |
if (conj.getKind() == kind::AND) |
287 |
|
{ |
288 |
31492 |
vector<Node> posv; |
289 |
15748 |
bool found_x = false; |
290 |
31492 |
map<TNode, bool> neg; |
291 |
109188 |
for (Node::iterator ii = conj.begin(); ii != conj.end(); ++ii) |
292 |
|
{ |
293 |
93444 |
if ((*ii).isVar()) |
294 |
|
{ |
295 |
46720 |
posv.push_back(*ii); |
296 |
46720 |
neg[*ii] = false; |
297 |
46720 |
found_x = found_x || v0 == *ii; |
298 |
|
} |
299 |
46724 |
else if ((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) |
300 |
|
{ |
301 |
46724 |
posv.push_back((*ii)[0]); |
302 |
46724 |
neg[(*ii)[0]] = true; |
303 |
46724 |
found_x = found_x || v0 == (*ii)[0]; |
304 |
|
} |
305 |
|
else |
306 |
|
{ |
307 |
|
eligible = false; |
308 |
|
Debug("miplib") |
309 |
|
<< " -- INELIGIBLE -- (non-var: " << *ii << ")" << endl; |
310 |
|
break; |
311 |
|
} |
312 |
93444 |
if (propagator->isAssigned(posv.back())) |
313 |
|
{ |
314 |
4 |
eligible = false; |
315 |
8 |
Debug("miplib") << " -- INELIGIBLE -- (" << posv.back() |
316 |
4 |
<< " asserted)" << endl; |
317 |
4 |
break; |
318 |
|
} |
319 |
|
} |
320 |
15748 |
if (!eligible) |
321 |
|
{ |
322 |
4 |
break; |
323 |
|
} |
324 |
15744 |
if (!found_x) |
325 |
|
{ |
326 |
|
eligible = false; |
327 |
|
Debug("miplib") << " --INELIGIBLE -- (couldn't find " << v0 |
328 |
|
<< " in conjunction)" << endl; |
329 |
|
break; |
330 |
|
} |
331 |
15744 |
sort(posv.begin(), posv.end()); |
332 |
31488 |
const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); |
333 |
31488 |
const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) |
334 |
|
? (*j1)[1][1] |
335 |
31488 |
: (*j1)[1][0]; |
336 |
31488 |
const pair<Node, Node> pos_var(pos, var); |
337 |
|
const Rational& constant = |
338 |
31488 |
((*j1)[1][0].getKind() == kind::CONST_RATIONAL) |
339 |
47232 |
? (*j1)[1][0].getConst<Rational>() |
340 |
31488 |
: (*j1)[1][1].getConst<Rational>(); |
341 |
15744 |
uint64_t mark = 0; |
342 |
15744 |
unsigned countneg = 0, thepos = 0; |
343 |
109184 |
for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii) |
344 |
|
{ |
345 |
93440 |
if (neg[pos[ii]]) |
346 |
|
{ |
347 |
46720 |
++countneg; |
348 |
|
} |
349 |
|
else |
350 |
|
{ |
351 |
46720 |
thepos = ii; |
352 |
46720 |
mark |= (0x1 << ii); |
353 |
|
} |
354 |
|
} |
355 |
15744 |
if ((marks[pos_var] & (1lu << mark)) != 0) |
356 |
|
{ |
357 |
|
eligible = false; |
358 |
|
Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; |
359 |
|
break; |
360 |
|
} |
361 |
31488 |
Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark) |
362 |
15744 |
<< endl; |
363 |
15744 |
marks[pos_var] |= (1lu << mark); |
364 |
31488 |
Debug("miplib") << "marks[" << pos << "," << var << "] now " |
365 |
15744 |
<< marks[pos_var] << endl; |
366 |
15744 |
if (countneg == pos.getNumChildren()) |
367 |
|
{ |
368 |
288 |
if (constant != 0) |
369 |
|
{ |
370 |
|
eligible = false; |
371 |
|
Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; |
372 |
|
break; |
373 |
|
} |
374 |
|
} |
375 |
15456 |
else if (countneg == pos.getNumChildren() - 1) |
376 |
|
{ |
377 |
1568 |
Assert(coef[pos_var].size() <= 6 && thepos < 6); |
378 |
1568 |
if (coef[pos_var].size() <= thepos) |
379 |
|
{ |
380 |
828 |
coef[pos_var].resize(thepos + 1); |
381 |
|
} |
382 |
1568 |
coef[pos_var][thepos] = constant; |
383 |
|
} |
384 |
|
else |
385 |
|
{ |
386 |
13888 |
if (checks[pos_var].size() <= mark) |
387 |
|
{ |
388 |
5340 |
checks[pos_var].resize(mark + 1); |
389 |
|
} |
390 |
13888 |
checks[pos_var][mark] = constant; |
391 |
|
} |
392 |
15744 |
asserts[pos_var].push_back(*j1); |
393 |
|
} |
394 |
|
else |
395 |
|
{ |
396 |
1024 |
TNode x = conj; |
397 |
512 |
if (x != v0 && x != (v0).notNode()) |
398 |
|
{ |
399 |
|
eligible = false; |
400 |
|
Debug("miplib") |
401 |
|
<< " -- INELIGIBLE -- (x not present where I expect it)" << endl; |
402 |
|
break; |
403 |
|
} |
404 |
512 |
const bool xneg = (x.getKind() == kind::NOT); |
405 |
512 |
x = xneg ? x[0] : x; |
406 |
512 |
Debug("miplib") << " x:" << x << " " << xneg << endl; |
407 |
1024 |
const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) |
408 |
|
? (*j1)[1][1] |
409 |
1024 |
: (*j1)[1][0]; |
410 |
1024 |
const pair<Node, Node> x_var(x, var); |
411 |
|
const Rational& constant = |
412 |
1024 |
((*j1)[1][0].getKind() == kind::CONST_RATIONAL) |
413 |
1536 |
? (*j1)[1][0].getConst<Rational>() |
414 |
1024 |
: (*j1)[1][1].getConst<Rational>(); |
415 |
512 |
unsigned mark = (xneg ? 0 : 1); |
416 |
512 |
if ((marks[x_var] & (1u << mark)) != 0) |
417 |
|
{ |
418 |
|
eligible = false; |
419 |
|
Debug("miplib") << " -- INELIGIBLE -- (remarked)" << endl; |
420 |
|
break; |
421 |
|
} |
422 |
512 |
marks[x_var] |= (1u << mark); |
423 |
512 |
if (xneg) |
424 |
|
{ |
425 |
256 |
if (constant != 0) |
426 |
|
{ |
427 |
|
eligible = false; |
428 |
|
Debug("miplib") << " -- INELIGIBLE -- (nonzero constant)" << endl; |
429 |
|
break; |
430 |
|
} |
431 |
|
} |
432 |
|
else |
433 |
|
{ |
434 |
256 |
Assert(coef[x_var].size() <= 6); |
435 |
256 |
coef[x_var].resize(6); |
436 |
256 |
coef[x_var][0] = constant; |
437 |
|
} |
438 |
512 |
asserts[x_var].push_back(*j1); |
439 |
|
} |
440 |
|
} |
441 |
276 |
if (eligible) |
442 |
|
{ |
443 |
816 |
for (map<pair<Node, Node>, uint64_t>::const_iterator j = marks.begin(); |
444 |
816 |
j != marks.end(); |
445 |
|
++j) |
446 |
|
{ |
447 |
1084 |
const TNode pos = (*j).first.first; |
448 |
1084 |
const TNode var = (*j).first.second; |
449 |
544 |
const pair<Node, Node>& pos_var = (*j).first; |
450 |
544 |
const uint64_t mark = (*j).second; |
451 |
|
const unsigned numVars = |
452 |
544 |
pos.getKind() == kind::AND ? pos.getNumChildren() : 1; |
453 |
544 |
uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1; |
454 |
544 |
expected = (expected == 0) ? -1 : expected; // fix for overflow |
455 |
1088 |
Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " |
456 |
544 |
<< expected << dec << endl; |
457 |
544 |
Assert(pos.getKind() == kind::AND || pos.isVar()); |
458 |
544 |
if (mark != expected) |
459 |
|
{ |
460 |
|
Debug("miplib") << " -- INELIGIBLE " << pos |
461 |
|
<< " -- (insufficiently marked, got " << mark |
462 |
|
<< " for " << numVars << " vars, expected " |
463 |
|
<< expected << endl; |
464 |
|
} |
465 |
|
else |
466 |
|
{ |
467 |
544 |
if (mark != 3) |
468 |
|
{ // exclude single-var case; nothing to check there |
469 |
288 |
uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1; |
470 |
288 |
sz = (sz == 0) ? -1 : sz; // fix for overflow |
471 |
288 |
Assert(sz == mark) << "expected size " << sz << " == mark " << mark; |
472 |
16028 |
for (size_t k = 0; k < checks[pos_var].size(); ++k) |
473 |
|
{ |
474 |
15744 |
if ((k & (k - 1)) != 0) |
475 |
|
{ |
476 |
27772 |
Rational sum = 0; |
477 |
13888 |
Debug("miplib") << k << " => " << checks[pos_var][k] << endl; |
478 |
86576 |
for (size_t v1 = 1, kk = k; kk != 0; ++v1, kk >>= 1) |
479 |
|
{ |
480 |
72688 |
if ((kk & 0x1) == 1) |
481 |
|
{ |
482 |
45152 |
Assert(pos.getKind() == kind::AND); |
483 |
90304 |
Debug("miplib") |
484 |
90304 |
<< "var " << v1 << " : " << pos[v1 - 1] |
485 |
45152 |
<< " coef:" << coef[pos_var][v1 - 1] << endl; |
486 |
45152 |
sum += coef[pos_var][v1 - 1]; |
487 |
|
} |
488 |
|
} |
489 |
27776 |
Debug("miplib") << "checkSum is " << sum << " input says " |
490 |
13888 |
<< checks[pos_var][k] << endl; |
491 |
13888 |
if (sum != checks[pos_var][k]) |
492 |
|
{ |
493 |
4 |
eligible = false; |
494 |
8 |
Debug("miplib") << " -- INELIGIBLE " << pos |
495 |
4 |
<< " -- (nonlinear combination)" << endl; |
496 |
4 |
break; |
497 |
|
} |
498 |
|
} |
499 |
|
else |
500 |
|
{ |
501 |
3712 |
Assert(checks[pos_var][k] == 0) |
502 |
1856 |
<< "checks[(" << pos << "," << var << ")][" << k |
503 |
|
<< "] should be 0, but it's " |
504 |
|
<< checks[pos_var] |
505 |
|
[k]; // we never set for single-positive-var |
506 |
|
} |
507 |
|
} |
508 |
|
} |
509 |
548 |
if (!eligible) |
510 |
|
{ |
511 |
4 |
eligible = true; // next is still eligible |
512 |
4 |
continue; |
513 |
|
} |
514 |
|
|
515 |
1080 |
Debug("miplib") << " -- ELIGIBLE " << v0 << " , " << pos << " --" |
516 |
540 |
<< endl; |
517 |
1080 |
vector<Node> newVars; |
518 |
1080 |
expr::NodeSelfIterator ii, iiend; |
519 |
540 |
if (pos.getKind() == kind::AND) |
520 |
|
{ |
521 |
284 |
ii = pos.begin(); |
522 |
284 |
iiend = pos.end(); |
523 |
|
} |
524 |
|
else |
525 |
|
{ |
526 |
256 |
ii = expr::NodeSelfIterator::self(pos); |
527 |
256 |
iiend = expr::NodeSelfIterator::selfEnd(pos); |
528 |
|
} |
529 |
4172 |
for (; ii != iiend; ++ii) |
530 |
|
{ |
531 |
1816 |
Node& varRef = intVars[*ii]; |
532 |
1816 |
if (varRef.isNull()) |
533 |
|
{ |
534 |
536 |
stringstream ss; |
535 |
268 |
ss << "mipvar_" << *ii; |
536 |
|
Node newVar = sm->mkDummySkolem( |
537 |
536 |
ss.str(), |
538 |
536 |
nm->integerType(), |
539 |
1072 |
"a variable introduced due to scrubbing a miplib encoding"); |
540 |
536 |
Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero)); |
541 |
536 |
Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one)); |
542 |
536 |
TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr); |
543 |
536 |
TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr); |
544 |
|
|
545 |
536 |
Node n = rewrite(geq.andNode(leq)); |
546 |
268 |
assertionsToPreprocess->push_back(n); |
547 |
536 |
TrustSubstitutionMap tnullMap(&fakeContext, nullptr); |
548 |
268 |
CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get(); |
549 |
|
Theory::PPAssertStatus status CVC5_UNUSED; // just for assertions |
550 |
268 |
status = te->solve(tgeq, tnullMap); |
551 |
268 |
Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED) |
552 |
|
<< "unexpected solution from arith's ppAssert()"; |
553 |
268 |
Assert(nullMap.empty()) |
554 |
|
<< "unexpected substitution from arith's ppAssert()"; |
555 |
268 |
status = te->solve(tleq, tnullMap); |
556 |
268 |
Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED) |
557 |
|
<< "unexpected solution from arith's ppAssert()"; |
558 |
268 |
Assert(nullMap.empty()) |
559 |
|
<< "unexpected substitution from arith's ppAssert()"; |
560 |
268 |
newVars.push_back(newVar); |
561 |
268 |
varRef = newVar; |
562 |
|
} |
563 |
|
else |
564 |
|
{ |
565 |
1548 |
newVars.push_back(varRef); |
566 |
|
} |
567 |
|
} |
568 |
1080 |
Node sum; |
569 |
540 |
if (pos.getKind() == kind::AND) |
570 |
|
{ |
571 |
568 |
NodeBuilder sumb(kind::PLUS); |
572 |
1844 |
for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) |
573 |
|
{ |
574 |
7800 |
sumb << nm->mkNode( |
575 |
7800 |
kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]); |
576 |
|
} |
577 |
284 |
sum = sumb; |
578 |
|
} |
579 |
|
else |
580 |
|
{ |
581 |
768 |
sum = nm->mkNode( |
582 |
768 |
kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); |
583 |
|
} |
584 |
1080 |
Debug("miplib") << "vars[] " << var << endl |
585 |
540 |
<< " eq " << rewrite(sum) << endl; |
586 |
1080 |
Node newAssertion = var.eqNode(rewrite(sum)); |
587 |
540 |
if (top_level_substs.hasSubstitution(newAssertion[0])) |
588 |
|
{ |
589 |
|
Assert(top_level_substs.getSubstitution(newAssertion[0]) |
590 |
|
== newAssertion[1]); |
591 |
|
} |
592 |
1080 |
else if (pos.getNumChildren() |
593 |
540 |
<= options().arith.arithMLTrickSubstitutions) |
594 |
|
{ |
595 |
256 |
top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); |
596 |
512 |
Debug("miplib") << "addSubs: " << newAssertion[0] << " to " |
597 |
256 |
<< newAssertion[1] << endl; |
598 |
|
} |
599 |
|
else |
600 |
|
{ |
601 |
568 |
Debug("miplib") |
602 |
568 |
<< "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] |
603 |
284 |
<< " (threshold is " |
604 |
284 |
<< options().arith.arithMLTrickSubstitutions << ")" << endl; |
605 |
|
} |
606 |
540 |
newAssertion = rewrite(newAssertion); |
607 |
540 |
Debug("miplib") << " " << newAssertion << endl; |
608 |
|
|
609 |
540 |
assertionsToPreprocess->push_back(newAssertion); |
610 |
540 |
Debug("miplib") << " assertions to remove: " << endl; |
611 |
16780 |
for (vector<TNode>::const_iterator k = asserts[pos_var].begin(), |
612 |
540 |
k_end = asserts[pos_var].end(); |
613 |
16780 |
k != k_end; |
614 |
|
++k) |
615 |
|
{ |
616 |
16240 |
Debug("miplib") << " " << *k << endl; |
617 |
16240 |
removeAssertions.insert((*k).getId()); |
618 |
|
} |
619 |
|
} |
620 |
|
} |
621 |
|
} |
622 |
|
} |
623 |
12 |
if (!removeAssertions.empty()) |
624 |
|
{ |
625 |
8 |
Debug("miplib") << " scrubbing miplib encoding..." << endl; |
626 |
76 |
for (size_t i = 0, size = assertionsToPreprocess->getRealAssertionsEnd(); |
627 |
76 |
i < size; |
628 |
|
++i) |
629 |
|
{ |
630 |
136 |
Node assertion = (*assertionsToPreprocess)[i]; |
631 |
68 |
if (removeAssertions.find(assertion.getId()) != removeAssertions.end()) |
632 |
|
{ |
633 |
56 |
Debug("miplib") << " - removing " << assertion << endl; |
634 |
56 |
assertionsToPreprocess->replace(i, trueNode); |
635 |
56 |
++d_statistics.d_numMiplibAssertionsRemoved; |
636 |
|
} |
637 |
12 |
else if (assertion.getKind() == kind::AND) |
638 |
|
{ |
639 |
8 |
size_t removals = removeFromConjunction(assertion, removeAssertions); |
640 |
8 |
if (removals > 0) |
641 |
|
{ |
642 |
4 |
Debug("miplib") << " - reduced " << assertion << endl; |
643 |
4 |
Debug("miplib") << " - by " << removals << " conjuncts" << endl; |
644 |
4 |
d_statistics.d_numMiplibAssertionsRemoved += removals; |
645 |
|
} |
646 |
|
} |
647 |
68 |
Debug("miplib") << "had: " << assertion << endl; |
648 |
68 |
assertionsToPreprocess->replace( |
649 |
136 |
i, rewrite(top_level_substs.apply(assertion))); |
650 |
68 |
Debug("miplib") << "now: " << assertion << endl; |
651 |
|
} |
652 |
|
} |
653 |
|
else |
654 |
|
{ |
655 |
4 |
Debug("miplib") << " miplib pass found nothing." << endl; |
656 |
|
} |
657 |
12 |
assertionsToPreprocess->updateRealAssertionsEnd(); |
658 |
24 |
return PreprocessingPassResult::NO_CONFLICT; |
659 |
|
} |
660 |
|
|
661 |
15338 |
MipLibTrick::Statistics::Statistics(StatisticsRegistry& reg) |
662 |
|
: d_numMiplibAssertionsRemoved(reg.registerInt( |
663 |
15338 |
"preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved")) |
664 |
|
{ |
665 |
15338 |
} |
666 |
|
|
667 |
|
|
668 |
|
} // namespace passes |
669 |
|
} // namespace preprocessing |
670 |
31125 |
} // namespace cvc5 |