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