1 /********************* */
2 /*! \file pseudo_boolean_processor.cpp
4 ** Top contributors (to current version):
5 ** Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "preprocessing/passes/pseudo_boolean_processor.h"
20 #include "base/output.h"
21 #include "theory/arith/arith_utilities.h"
22 #include "theory/arith/normal_form.h"
23 #include "theory/rewriter.h"
26 namespace preprocessing
{
29 using namespace CVC4::theory
;
30 using namespace CVC4::theory::arith
;
32 PseudoBooleanProcessor::PseudoBooleanProcessor(
33 PreprocessingPassContext
* preprocContext
)
34 : PreprocessingPass(preprocContext
, "pseudo-boolean-processor"),
35 d_pbBounds(preprocContext
->getUserContext()),
36 d_subCache(preprocContext
->getUserContext()),
37 d_pbs(preprocContext
->getUserContext(), 0)
41 PreprocessingPassResult
PseudoBooleanProcessor::applyInternal(
42 AssertionPipeline
* assertionsToPreprocess
)
44 learn(assertionsToPreprocess
->ref());
47 applyReplacements(assertionsToPreprocess
);
50 return PreprocessingPassResult::NO_CONFLICT
;
53 bool PseudoBooleanProcessor::decomposeAssertion(Node assertion
, bool negated
)
55 if (assertion
.getKind() != kind::GEQ
)
59 Assert(assertion
.getKind() == kind::GEQ
);
61 Debug("pbs::rewrites") << "decomposeAssertion" << assertion
<< std::endl
;
63 Node l
= assertion
[0];
64 Node r
= assertion
[1];
66 if (r
.getKind() != kind::CONST_RATIONAL
)
68 Debug("pbs::rewrites") << "not rhs constant" << assertion
<< std::endl
;
71 // don't bother matching on anything other than + on the left hand side
72 if (l
.getKind() != kind::PLUS
)
74 Debug("pbs::rewrites") << "not plus" << assertion
<< std::endl
;
78 if (!Polynomial::isMember(l
))
80 Debug("pbs::rewrites") << "not polynomial" << assertion
<< std::endl
;
84 Polynomial p
= Polynomial::parsePolynomial(l
);
92 d_off
= (-r
.getConst
<Rational
>());
94 if (d_off
.value().isIntegral())
96 d_off
= d_off
.value() + Rational(1);
100 d_off
= Rational(d_off
.value().ceiling());
106 d_off
= r
.getConst
<Rational
>();
107 d_off
= Rational(d_off
.value().ceiling());
109 Assert(d_off
.value().isIntegral());
111 int adj
= negated
? -1 : 1;
112 for (Polynomial::iterator i
= p
.begin(), end
= p
.end(); i
!= end
; ++i
)
115 const Rational
& coeff
= m
.getConstant().getValue();
116 if (!(coeff
.isOne() || coeff
.isNegativeOne()))
120 Assert(coeff
.sgn() != 0);
122 const VarList
& vl
= m
.getVarList();
123 Node v
= vl
.getNode();
125 if (!isPseudoBoolean(v
))
129 int sgn
= adj
* coeff
.sgn();
139 // all of the variables are pseudoboolean
140 // with coefficients +/- and the offsetoff
144 bool PseudoBooleanProcessor::isPseudoBoolean(Node v
) const
146 CDNode2PairMap::const_iterator ci
= d_pbBounds
.find(v
);
147 if (ci
!= d_pbBounds
.end())
149 const std::pair
<Node
, Node
>& p
= (*ci
).second
;
150 return !(p
.first
).isNull() && !(p
.second
).isNull();
155 void PseudoBooleanProcessor::addGeqZero(Node v
, Node exp
)
158 Assert(!exp
.isNull());
159 CDNode2PairMap::const_iterator ci
= d_pbBounds
.find(v
);
161 Debug("pbs::rewrites") << "addGeqZero " << v
<< std::endl
;
163 if (ci
== d_pbBounds
.end())
165 d_pbBounds
.insert(v
, std::make_pair(exp
, Node::null()));
169 const std::pair
<Node
, Node
>& p
= (*ci
).second
;
170 if (p
.first
.isNull())
172 Assert(!p
.second
.isNull());
173 d_pbBounds
.insert(v
, std::make_pair(exp
, p
.second
));
174 Debug("pbs::rewrites") << "add pbs " << v
<< std::endl
;
175 Assert(isPseudoBoolean(v
));
181 void PseudoBooleanProcessor::addLeqOne(Node v
, Node exp
)
184 Assert(!exp
.isNull());
185 Debug("pbs::rewrites") << "addLeqOne " << v
<< std::endl
;
186 CDNode2PairMap::const_iterator ci
= d_pbBounds
.find(v
);
187 if (ci
== d_pbBounds
.end())
189 d_pbBounds
.insert(v
, std::make_pair(Node::null(), exp
));
193 const std::pair
<Node
, Node
>& p
= (*ci
).second
;
194 if (p
.second
.isNull())
196 Assert(!p
.first
.isNull());
197 d_pbBounds
.insert(v
, std::make_pair(p
.first
, exp
));
198 Debug("pbs::rewrites") << "add pbs " << v
<< std::endl
;
199 Assert(isPseudoBoolean(v
));
205 void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion
,
209 Assert(assertion
.getKind() == kind::GEQ
);
210 Assert(assertion
== Rewriter::rewrite(assertion
));
212 // assume assertion is rewritten
213 Node l
= assertion
[0];
214 Node r
= assertion
[1];
216 if (r
.getKind() == kind::CONST_RATIONAL
)
218 const Rational
& rc
= r
.getConst
<Rational
>();
221 if (!negated
&& rc
.isZero())
225 else if (negated
&& rc
== Rational(2))
230 else if (l
.getKind() == kind::MULT
&& l
.getNumChildren() == 2)
232 Node c
= l
[0], v
= l
[1];
233 if (c
.getKind() == kind::CONST_RATIONAL
234 && c
.getConst
<Rational
>().isNegativeOne())
238 if (!negated
&& rc
.isNegativeOne())
239 { // (>= (* -1 x) -1)
249 learnGeqSub(assertion
);
253 void PseudoBooleanProcessor::learnInternal(Node assertion
,
257 switch (assertion
.getKind())
264 Node rw
= Rewriter::rewrite(assertion
);
267 if (assertion
.getKind() == kind::GEQ
)
269 learnRewrittenGeq(assertion
, negated
, orig
);
274 learnInternal(rw
, negated
, orig
);
278 case kind::NOT
: learnInternal(assertion
[0], !negated
, orig
); break;
279 default: break; // do nothing
283 void PseudoBooleanProcessor::learn(Node assertion
)
285 if (assertion
.getKind() == kind::AND
)
287 Node::iterator ci
= assertion
.begin(), cend
= assertion
.end();
288 for (; ci
!= cend
; ++ci
)
295 learnInternal(assertion
, false, assertion
);
299 Node
PseudoBooleanProcessor::mkGeqOne(Node v
)
301 NodeManager
* nm
= NodeManager::currentNM();
302 return nm
->mkNode(kind::GEQ
, v
, mkRationalNode(Rational(1)));
305 void PseudoBooleanProcessor::learn(const std::vector
<Node
>& assertions
)
307 std::vector
<Node
>::const_iterator ci
, cend
;
308 ci
= assertions
.begin();
309 cend
= assertions
.end();
310 for (; ci
!= cend
; ++ci
)
316 void PseudoBooleanProcessor::addSub(Node from
, Node to
)
318 if (!d_subCache
.hasSubstitution(from
))
320 Node rw_to
= Rewriter::rewrite(to
);
321 d_subCache
.addSubstitution(from
, rw_to
);
325 void PseudoBooleanProcessor::learnGeqSub(Node geq
)
327 Assert(geq
.getKind() == kind::GEQ
);
328 const bool negated
= false;
329 bool success
= decomposeAssertion(geq
, negated
);
332 Debug("pbs::rewrites") << "failed " << std::endl
;
335 Assert(d_off
.value().isIntegral());
336 Integer off
= d_off
.value().ceiling();
338 // \sum pos >= \sum neg + off
340 // for now special case everything we want
341 // target easy clauses
342 if (d_pos
.size() == 1 && d_neg
.size() == 1 && off
.isZero())
345 // |- (y >= 1) => (x >= 1)
346 Node x
= d_pos
.front();
347 Node y
= d_neg
.front();
349 Node xGeq1
= mkGeqOne(x
);
350 Node yGeq1
= mkGeqOne(y
);
351 Node imp
= yGeq1
.impNode(xGeq1
);
354 else if (d_pos
.size() == 0 && d_neg
.size() == 2 && off
.isNegativeOne())
358 // |- (or (not (x >= 1)) (not (y >= 1)))
362 Node xGeq1
= mkGeqOne(x
);
363 Node yGeq1
= mkGeqOne(y
);
364 Node cases
= (xGeq1
.notNode()).orNode(yGeq1
.notNode());
367 else if (d_pos
.size() == 2 && d_neg
.size() == 1 && off
.isZero())
370 // |- (z >= 1) => (or (x >= 1) (y >=1 ))
375 Node xGeq1
= mkGeqOne(x
);
376 Node yGeq1
= mkGeqOne(y
);
377 Node zGeq1
= mkGeqOne(z
);
378 NodeManager
* nm
= NodeManager::currentNM();
379 Node dis
= nm
->mkNode(kind::OR
, zGeq1
.notNode(), xGeq1
, yGeq1
);
384 Node
PseudoBooleanProcessor::applyReplacements(Node pre
)
386 Node assertion
= Rewriter::rewrite(pre
);
388 Node result
= d_subCache
.apply(assertion
);
389 if (Debug
.isOn("pbs::rewrites") && result
!= assertion
)
391 Debug("pbs::rewrites") << "applyReplacements" << assertion
<< "-> "
392 << result
<< std::endl
;
397 bool PseudoBooleanProcessor::likelyToHelp() const { return d_pbs
>= 100; }
399 void PseudoBooleanProcessor::applyReplacements(
400 AssertionPipeline
* assertionsToPreprocess
)
402 for (size_t i
= 0, N
= assertionsToPreprocess
->size(); i
< N
; ++i
)
404 assertionsToPreprocess
->replace(
405 i
, applyReplacements((*assertionsToPreprocess
)[i
]));
409 void PseudoBooleanProcessor::clear()
417 } // namespace passes
418 } // namespace preprocessing