Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/pseudo_boolean_processor.cpp	Lines:	147	196	75.0 %
Date:	2021-05-22	Branches:	262	933	28.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Andres Noetzli, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "preprocessing/passes/pseudo_boolean_processor.h"

#include "base/output.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {

using namespace cvc5::theory;
using namespace cvc5::theory::arith;

PseudoBooleanProcessor::PseudoBooleanProcessor(
    PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
      d_pbBounds(preprocContext->getUserContext()),
      d_subCache(preprocContext->getUserContext()),
      d_pbs(preprocContext->getUserContext(), 0)
{
}

PreprocessingPassResult PseudoBooleanProcessor::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  learn(assertionsToPreprocess->ref());
  if (likelyToHelp())
  {
    applyReplacements(assertionsToPreprocess);
  }

  return PreprocessingPassResult::NO_CONFLICT;
}

bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated)
{
  if (assertion.getKind() != kind::GEQ)
  {
    return false;
  }
  Assert(assertion.getKind() == kind::GEQ);

  Debug("pbs::rewrites") << "decomposeAssertion" << assertion << std::endl;

  Node l = assertion[0];
  Node r = assertion[1];

  if (r.getKind() != kind::CONST_RATIONAL)
  {
    Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl;
    return false;
  }
  // don't bother matching on anything other than + on the left hand side
  if (l.getKind() != kind::PLUS)
  {
    Debug("pbs::rewrites") << "not plus" << assertion << std::endl;
    return false;
  }

  if (!Polynomial::isMember(l))
  {
    Debug("pbs::rewrites") << "not polynomial" << assertion << std::endl;
    return false;
  }

  Polynomial p = Polynomial::parsePolynomial(l);
  clear();
  if (negated)
  {
    // (not (>= p r))
    // (< p r)
    // (> (-p) (-r))
    // (>= (-p) (-r +1))
    d_off = (-r.getConst<Rational>());

    if (d_off.value().isIntegral())
    {
      d_off = d_off.value() + Rational(1);
    }
    else
    {
      d_off = Rational(d_off.value().ceiling());
    }
  }
  else
  {
    // (>= p r)
    d_off = r.getConst<Rational>();
    d_off = Rational(d_off.value().ceiling());
  }
  Assert(d_off.value().isIntegral());

  int adj = negated ? -1 : 1;
  for (Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i)
  {
    Monomial m = *i;
    const Rational& coeff = m.getConstant().getValue();
    if (!(coeff.isOne() || coeff.isNegativeOne()))
    {
      return false;
    }
    Assert(coeff.sgn() != 0);

    const VarList& vl = m.getVarList();
    Node v = vl.getNode();

    if (!isPseudoBoolean(v))
    {
      return false;
    }
    int sgn = adj * coeff.sgn();
    if (sgn > 0)
    {
      d_pos.push_back(v);
    }
    else
    {
      d_neg.push_back(v);
    }
  }
  // all of the variables are pseudoboolean
  // with coefficients +/- and the offsetoff
  return true;
}

bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const
{
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
  if (ci != d_pbBounds.end())
  {
    const std::pair<Node, Node>& p = (*ci).second;
    return !(p.first).isNull() && !(p.second).isNull();
  }
  return false;
}

void PseudoBooleanProcessor::addGeqZero(Node v, Node exp)
{
  Assert(isIntVar(v));
  Assert(!exp.isNull());
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);

  Debug("pbs::rewrites") << "addGeqZero " << v << std::endl;

  if (ci == d_pbBounds.end())
  {
    d_pbBounds.insert(v, std::make_pair(exp, Node::null()));
  }
  else
  {
    const std::pair<Node, Node>& p = (*ci).second;
    if (p.first.isNull())
    {
      Assert(!p.second.isNull());
      d_pbBounds.insert(v, std::make_pair(exp, p.second));
      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
      Assert(isPseudoBoolean(v));
      d_pbs = d_pbs + 1;
    }
  }
}

void PseudoBooleanProcessor::addLeqOne(Node v, Node exp)
{
  Assert(isIntVar(v));
  Assert(!exp.isNull());
  Debug("pbs::rewrites") << "addLeqOne " << v << std::endl;
  CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
  if (ci == d_pbBounds.end())
  {
    d_pbBounds.insert(v, std::make_pair(Node::null(), exp));
  }
  else
  {
    const std::pair<Node, Node>& p = (*ci).second;
    if (p.second.isNull())
    {
      Assert(!p.first.isNull());
      d_pbBounds.insert(v, std::make_pair(p.first, exp));
      Debug("pbs::rewrites") << "add pbs " << v << std::endl;
      Assert(isPseudoBoolean(v));
      d_pbs = d_pbs + 1;
    }
  }
}

void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
                                               bool negated,
                                               Node orig)
{
  Assert(assertion.getKind() == kind::GEQ);
  Assert(assertion == Rewriter::rewrite(assertion));

  // assume assertion is rewritten
  Node l = assertion[0];
  Node r = assertion[1];

  if (r.getKind() == kind::CONST_RATIONAL)
  {
    const Rational& rc = r.getConst<Rational>();
    if (isIntVar(l))
    {
      if (!negated && rc.isZero())
      {  // (>= x 0)
        addGeqZero(l, orig);
      }
      else if (negated && rc == Rational(2))
      {
        addLeqOne(l, orig);
      }
    }
    else if (l.getKind() == kind::MULT && l.getNumChildren() == 2)
    {
      Node c = l[0], v = l[1];
      if (c.getKind() == kind::CONST_RATIONAL
          && c.getConst<Rational>().isNegativeOne())
      {
        if (isIntVar(v))
        {
          if (!negated && rc.isNegativeOne())
          {  // (>= (* -1 x) -1)
            addLeqOne(v, orig);
          }
        }
      }
    }
  }

  if (!negated)
  {
    learnGeqSub(assertion);
  }
}

void PseudoBooleanProcessor::learnInternal(Node assertion,
                                           bool negated,
                                           Node orig)
{
  switch (assertion.getKind())
  {
    case kind::GEQ:
    case kind::GT:
    case kind::LEQ:
    case kind::LT:
    {
      Node rw = Rewriter::rewrite(assertion);
      if (assertion == rw)
      {
        if (assertion.getKind() == kind::GEQ)
        {
          learnRewrittenGeq(assertion, negated, orig);
        }
      }
      else
      {
        learnInternal(rw, negated, orig);
      }
    }
    break;
    case kind::NOT: learnInternal(assertion[0], !negated, orig); break;
    default: break;  // do nothing
  }
}

void PseudoBooleanProcessor::learn(Node assertion)
{
  if (assertion.getKind() == kind::AND)
  {
    Node::iterator ci = assertion.begin(), cend = assertion.end();
    for (; ci != cend; ++ci)
    {
      learn(*ci);
    }
  }
  else
  {
    learnInternal(assertion, false, assertion);
  }
}

Node PseudoBooleanProcessor::mkGeqOne(Node v)
{
  NodeManager* nm = NodeManager::currentNM();
  return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1)));
}

void PseudoBooleanProcessor::learn(const std::vector<Node>& assertions)
{
  std::vector<Node>::const_iterator ci, cend;
  ci = assertions.begin();
  cend = assertions.end();
  for (; ci != cend; ++ci)
  {
    learn(*ci);
  }
}

void PseudoBooleanProcessor::addSub(Node from, Node to)
{
  if (!d_subCache.hasSubstitution(from))
  {
    Node rw_to = Rewriter::rewrite(to);
    d_subCache.addSubstitution(from, rw_to);
  }
}

void PseudoBooleanProcessor::learnGeqSub(Node geq)
{
  Assert(geq.getKind() == kind::GEQ);
  const bool negated = false;
  bool success = decomposeAssertion(geq, negated);
  if (!success)
  {
    Debug("pbs::rewrites") << "failed " << std::endl;
    return;
  }
  Assert(d_off.value().isIntegral());
  Integer off = d_off.value().ceiling();

  // \sum pos >= \sum neg + off

  // for now special case everything we want
  // target easy clauses
  if (d_pos.size() == 1 && d_neg.size() == 1 && off.isZero())
  {
    // x >= y
    // |- (y >= 1) => (x >= 1)
    Node x = d_pos.front();
    Node y = d_neg.front();

    Node xGeq1 = mkGeqOne(x);
    Node yGeq1 = mkGeqOne(y);
    Node imp = yGeq1.impNode(xGeq1);
    addSub(geq, imp);
  }
  else if (d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne())
  {
    // 0 >= (x + y -1)
    // |- 1 >= x + y
    // |- (or (not (x >= 1)) (not (y >= 1)))
    Node x = d_neg[0];
    Node y = d_neg[1];

    Node xGeq1 = mkGeqOne(x);
    Node yGeq1 = mkGeqOne(y);
    Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode());
    addSub(geq, cases);
  }
  else if (d_pos.size() == 2 && d_neg.size() == 1 && off.isZero())
  {
    // (x + y) >= z
    // |- (z >= 1) => (or (x >= 1) (y >=1 ))
    Node x = d_pos[0];
    Node y = d_pos[1];
    Node z = d_neg[0];

    Node xGeq1 = mkGeqOne(x);
    Node yGeq1 = mkGeqOne(y);
    Node zGeq1 = mkGeqOne(z);
    NodeManager* nm = NodeManager::currentNM();
    Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1);
    addSub(geq, dis);
  }
}

Node PseudoBooleanProcessor::applyReplacements(Node pre)
{
  Node assertion = Rewriter::rewrite(pre);

  Node result = d_subCache.apply(assertion);
  if (Debug.isOn("pbs::rewrites") && result != assertion)
  {
    Debug("pbs::rewrites") << "applyReplacements" << assertion << "-> "
                           << result << std::endl;
  }
  return result;
}

bool PseudoBooleanProcessor::likelyToHelp() const { return d_pbs >= 100; }

void PseudoBooleanProcessor::applyReplacements(
    AssertionPipeline* assertionsToPreprocess)
{
  for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
  {
    assertionsToPreprocess->replace(
        i, applyReplacements((*assertionsToPreprocess)[i]));
  }
}

void PseudoBooleanProcessor::clear()
{
  d_off.clear();
  d_pos.clear();
  d_neg.clear();
}


}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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