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