GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/pseudo_boolean_processor.cpp Lines: 147 196 75.0 %
Date: 2021-03-23 Branches: 262 933 28.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file pseudo_boolean_processor.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andres Noetzli
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "preprocessing/passes/pseudo_boolean_processor.h"
19
20
#include "base/output.h"
21
#include "preprocessing/assertion_pipeline.h"
22
#include "preprocessing/preprocessing_pass_context.h"
23
#include "theory/arith/arith_utilities.h"
24
#include "theory/arith/normal_form.h"
25
#include "theory/rewriter.h"
26
27
namespace CVC4 {
28
namespace preprocessing {
29
namespace passes {
30
31
using namespace CVC4::theory;
32
using namespace CVC4::theory::arith;
33
34
8997
PseudoBooleanProcessor::PseudoBooleanProcessor(
35
8997
    PreprocessingPassContext* preprocContext)
36
    : PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
37
      d_pbBounds(preprocContext->getUserContext()),
38
      d_subCache(preprocContext->getUserContext()),
39
8997
      d_pbs(preprocContext->getUserContext(), 0)
40
{
41
8997
}
42
43
2
PreprocessingPassResult PseudoBooleanProcessor::applyInternal(
44
    AssertionPipeline* assertionsToPreprocess)
45
{
46
2
  learn(assertionsToPreprocess->ref());
47
2
  if (likelyToHelp())
48
  {
49
2
    applyReplacements(assertionsToPreprocess);
50
  }
51
52
2
  return PreprocessingPassResult::NO_CONFLICT;
53
}
54
55
202
bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated)
56
{
57
202
  if (assertion.getKind() != kind::GEQ)
58
  {
59
    return false;
60
  }
61
202
  Assert(assertion.getKind() == kind::GEQ);
62
63
202
  Debug("pbs::rewrites") << "decomposeAssertion" << assertion << std::endl;
64
65
404
  Node l = assertion[0];
66
404
  Node r = assertion[1];
67
68
202
  if (r.getKind() != kind::CONST_RATIONAL)
69
  {
70
    Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl;
71
    return false;
72
  }
73
  // don't bother matching on anything other than + on the left hand side
74
202
  if (l.getKind() != kind::PLUS)
75
  {
76
200
    Debug("pbs::rewrites") << "not plus" << assertion << std::endl;
77
200
    return false;
78
  }
79
80
2
  if (!Polynomial::isMember(l))
81
  {
82
    Debug("pbs::rewrites") << "not polynomial" << assertion << std::endl;
83
    return false;
84
  }
85
86
4
  Polynomial p = Polynomial::parsePolynomial(l);
87
2
  clear();
88
2
  if (negated)
89
  {
90
    // (not (>= p r))
91
    // (< p r)
92
    // (> (-p) (-r))
93
    // (>= (-p) (-r +1))
94
    d_off = (-r.getConst<Rational>());
95
96
    if (d_off.value().isIntegral())
97
    {
98
      d_off = d_off.value() + Rational(1);
99
    }
100
    else
101
    {
102
      d_off = Rational(d_off.value().ceiling());
103
    }
104
  }
105
  else
106
  {
107
    // (>= p r)
108
2
    d_off = r.getConst<Rational>();
109
2
    d_off = Rational(d_off.value().ceiling());
110
  }
111
2
  Assert(d_off.value().isIntegral());
112
113
2
  int adj = negated ? -1 : 1;
114
6
  for (Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i)
115
  {
116
8
    Monomial m = *i;
117
4
    const Rational& coeff = m.getConstant().getValue();
118
4
    if (!(coeff.isOne() || coeff.isNegativeOne()))
119
    {
120
      return false;
121
    }
122
4
    Assert(coeff.sgn() != 0);
123
124
4
    const VarList& vl = m.getVarList();
125
8
    Node v = vl.getNode();
126
127
4
    if (!isPseudoBoolean(v))
128
    {
129
      return false;
130
    }
131
4
    int sgn = adj * coeff.sgn();
132
4
    if (sgn > 0)
133
    {
134
2
      d_pos.push_back(v);
135
    }
136
    else
137
    {
138
2
      d_neg.push_back(v);
139
    }
140
  }
141
  // all of the variables are pseudoboolean
142
  // with coefficients +/- and the offsetoff
143
2
  return true;
144
}
145
146
204
bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const
147
{
148
204
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
149
204
  if (ci != d_pbBounds.end())
150
  {
151
204
    const std::pair<Node, Node>& p = (*ci).second;
152
204
    return !(p.first).isNull() && !(p.second).isNull();
153
  }
154
  return false;
155
}
156
157
200
void PseudoBooleanProcessor::addGeqZero(Node v, Node exp)
158
{
159
200
  Assert(isIntVar(v));
160
200
  Assert(!exp.isNull());
161
200
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
162
163
200
  Debug("pbs::rewrites") << "addGeqZero " << v << std::endl;
164
165
200
  if (ci == d_pbBounds.end())
166
  {
167
200
    d_pbBounds.insert(v, std::make_pair(exp, Node::null()));
168
  }
169
  else
170
  {
171
    const std::pair<Node, Node>& p = (*ci).second;
172
    if (p.first.isNull())
173
    {
174
      Assert(!p.second.isNull());
175
      d_pbBounds.insert(v, std::make_pair(exp, p.second));
176
      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
177
      Assert(isPseudoBoolean(v));
178
      d_pbs = d_pbs + 1;
179
    }
180
  }
181
200
}
182
183
200
void PseudoBooleanProcessor::addLeqOne(Node v, Node exp)
184
{
185
200
  Assert(isIntVar(v));
186
200
  Assert(!exp.isNull());
187
200
  Debug("pbs::rewrites") << "addLeqOne " << v << std::endl;
188
200
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
189
200
  if (ci == d_pbBounds.end())
190
  {
191
    d_pbBounds.insert(v, std::make_pair(Node::null(), exp));
192
  }
193
  else
194
  {
195
200
    const std::pair<Node, Node>& p = (*ci).second;
196
200
    if (p.second.isNull())
197
    {
198
200
      Assert(!p.first.isNull());
199
200
      d_pbBounds.insert(v, std::make_pair(p.first, exp));
200
200
      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
201
200
      Assert(isPseudoBoolean(v));
202
200
      d_pbs = d_pbs + 1;
203
    }
204
  }
205
200
}
206
207
402
void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
208
                                               bool negated,
209
                                               Node orig)
210
{
211
402
  Assert(assertion.getKind() == kind::GEQ);
212
402
  Assert(assertion == Rewriter::rewrite(assertion));
213
214
  // assume assertion is rewritten
215
804
  Node l = assertion[0];
216
804
  Node r = assertion[1];
217
218
402
  if (r.getKind() == kind::CONST_RATIONAL)
219
  {
220
402
    const Rational& rc = r.getConst<Rational>();
221
402
    if (isIntVar(l))
222
    {
223
400
      if (!negated && rc.isZero())
224
      {  // (>= x 0)
225
200
        addGeqZero(l, orig);
226
      }
227
200
      else if (negated && rc == Rational(2))
228
      {
229
200
        addLeqOne(l, orig);
230
      }
231
    }
232
2
    else if (l.getKind() == kind::MULT && l.getNumChildren() == 2)
233
    {
234
      Node c = l[0], v = l[1];
235
      if (c.getKind() == kind::CONST_RATIONAL
236
          && c.getConst<Rational>().isNegativeOne())
237
      {
238
        if (isIntVar(v))
239
        {
240
          if (!negated && rc.isNegativeOne())
241
          {  // (>= (* -1 x) -1)
242
            addLeqOne(v, orig);
243
          }
244
        }
245
      }
246
    }
247
  }
248
249
402
  if (!negated)
250
  {
251
202
    learnGeqSub(assertion);
252
  }
253
402
}
254
255
604
void PseudoBooleanProcessor::learnInternal(Node assertion,
256
                                           bool negated,
257
                                           Node orig)
258
{
259
604
  switch (assertion.getKind())
260
  {
261
402
    case kind::GEQ:
262
    case kind::GT:
263
    case kind::LEQ:
264
    case kind::LT:
265
    {
266
804
      Node rw = Rewriter::rewrite(assertion);
267
402
      if (assertion == rw)
268
      {
269
402
        if (assertion.getKind() == kind::GEQ)
270
        {
271
402
          learnRewrittenGeq(assertion, negated, orig);
272
        }
273
      }
274
      else
275
      {
276
        learnInternal(rw, negated, orig);
277
402
      }
278
    }
279
402
    break;
280
200
    case kind::NOT: learnInternal(assertion[0], !negated, orig); break;
281
2
    default: break;  // do nothing
282
  }
283
604
}
284
285
404
void PseudoBooleanProcessor::learn(Node assertion)
286
{
287
404
  if (assertion.getKind() == kind::AND)
288
  {
289
    Node::iterator ci = assertion.begin(), cend = assertion.end();
290
    for (; ci != cend; ++ci)
291
    {
292
      learn(*ci);
293
    }
294
  }
295
  else
296
  {
297
404
    learnInternal(assertion, false, assertion);
298
  }
299
404
}
300
301
4
Node PseudoBooleanProcessor::mkGeqOne(Node v)
302
{
303
4
  NodeManager* nm = NodeManager::currentNM();
304
4
  return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1)));
305
}
306
307
2
void PseudoBooleanProcessor::learn(const std::vector<Node>& assertions)
308
{
309
2
  std::vector<Node>::const_iterator ci, cend;
310
2
  ci = assertions.begin();
311
2
  cend = assertions.end();
312
810
  for (; ci != cend; ++ci)
313
  {
314
404
    learn(*ci);
315
  }
316
2
}
317
318
2
void PseudoBooleanProcessor::addSub(Node from, Node to)
319
{
320
2
  if (!d_subCache.hasSubstitution(from))
321
  {
322
4
    Node rw_to = Rewriter::rewrite(to);
323
2
    d_subCache.addSubstitution(from, rw_to);
324
  }
325
2
}
326
327
202
void PseudoBooleanProcessor::learnGeqSub(Node geq)
328
{
329
202
  Assert(geq.getKind() == kind::GEQ);
330
202
  const bool negated = false;
331
202
  bool success = decomposeAssertion(geq, negated);
332
202
  if (!success)
333
  {
334
200
    Debug("pbs::rewrites") << "failed " << std::endl;
335
200
    return;
336
  }
337
2
  Assert(d_off.value().isIntegral());
338
4
  Integer off = d_off.value().ceiling();
339
340
  // \sum pos >= \sum neg + off
341
342
  // for now special case everything we want
343
  // target easy clauses
344
2
  if (d_pos.size() == 1 && d_neg.size() == 1 && off.isZero())
345
  {
346
    // x >= y
347
    // |- (y >= 1) => (x >= 1)
348
4
    Node x = d_pos.front();
349
4
    Node y = d_neg.front();
350
351
4
    Node xGeq1 = mkGeqOne(x);
352
4
    Node yGeq1 = mkGeqOne(y);
353
4
    Node imp = yGeq1.impNode(xGeq1);
354
2
    addSub(geq, imp);
355
  }
356
  else if (d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne())
357
  {
358
    // 0 >= (x + y -1)
359
    // |- 1 >= x + y
360
    // |- (or (not (x >= 1)) (not (y >= 1)))
361
    Node x = d_neg[0];
362
    Node y = d_neg[1];
363
364
    Node xGeq1 = mkGeqOne(x);
365
    Node yGeq1 = mkGeqOne(y);
366
    Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode());
367
    addSub(geq, cases);
368
  }
369
  else if (d_pos.size() == 2 && d_neg.size() == 1 && off.isZero())
370
  {
371
    // (x + y) >= z
372
    // |- (z >= 1) => (or (x >= 1) (y >=1 ))
373
    Node x = d_pos[0];
374
    Node y = d_pos[1];
375
    Node z = d_neg[0];
376
377
    Node xGeq1 = mkGeqOne(x);
378
    Node yGeq1 = mkGeqOne(y);
379
    Node zGeq1 = mkGeqOne(z);
380
    NodeManager* nm = NodeManager::currentNM();
381
    Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1);
382
    addSub(geq, dis);
383
  }
384
}
385
386
404
Node PseudoBooleanProcessor::applyReplacements(Node pre)
387
{
388
808
  Node assertion = Rewriter::rewrite(pre);
389
390
404
  Node result = d_subCache.apply(assertion);
391
404
  if (Debug.isOn("pbs::rewrites") && result != assertion)
392
  {
393
    Debug("pbs::rewrites") << "applyReplacements" << assertion << "-> "
394
                           << result << std::endl;
395
  }
396
808
  return result;
397
}
398
399
2
bool PseudoBooleanProcessor::likelyToHelp() const { return d_pbs >= 100; }
400
401
2
void PseudoBooleanProcessor::applyReplacements(
402
    AssertionPipeline* assertionsToPreprocess)
403
{
404
406
  for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
405
  {
406
404
    assertionsToPreprocess->replace(
407
808
        i, applyReplacements((*assertionsToPreprocess)[i]));
408
  }
409
2
}
410
411
2
void PseudoBooleanProcessor::clear()
412
{
413
2
  d_off.clear();
414
2
  d_pos.clear();
415
2
  d_neg.clear();
416
2
}
417
418
419
}  // namespace passes
420
}  // namespace preprocessing
421
26685
}  // namespace CVC4