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