Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/icp/icp_solver.cpp	Lines:	171	203	84.2 %
Date:	2021-11-07	Branches:	268	613	43.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * Implements a ICP-based solver for nonlinear arithmetic.
 */

#include "theory/arith/nl/icp/icp_solver.h"

#include <iostream>

#include "base/check.h"
#include "base/output.h"
#include "expr/node_algorithm.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/poly_conversion.h"
#include "theory/arith/normal_form.h"
#include "theory/rewriter.h"
#include "util/poly_util.h"

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {
namespace icp {

#ifdef CVC5_POLY_IMP

namespace {
/** A simple wrapper to nicely print an interval assignment. */
struct IAWrapper
{
  const poly::IntervalAssignment& ia;
  const VariableMapper& vm;
};
inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw)
{
  os << "{ ";
  bool first = true;
  for (const auto& v : iaw.vm.mVarpolyCVC)
  {
    if (iaw.ia.has(v.first))
    {
      if (first)
      {
        first = false;
      }
      else
      {
        os << ", ";
      }
      os << v.first << " -> " << iaw.ia.get(v.first);
    }
  }
  return os << " }";
}
}  // namespace

ICPSolver::ICPSolver(Env& env, InferenceManager& im)
    : EnvObj(env), d_im(im), d_state(d_mapper)
{
}

std::vector<Node> ICPSolver::collectVariables(const Node& n) const
{
  std::unordered_set<TNode> tmp;
  expr::getVariables(n, tmp);
  std::vector<Node> res;
  for (const auto& t : tmp)
  {
    res.emplace_back(t);
  }
  return res;
}

std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
{
  Node tmp = rewrite(n);
  if (tmp.isConst())
  {
    return {};
  }
  auto comp = Comparison::parseNormalForm(tmp).decompose(false);
  Kind k = std::get<1>(comp);
  if (k == Kind::DISTINCT)
  {
    return {};
  }
  auto poly = std::get<0>(comp);

  std::vector<Candidate> result;
  std::unordered_set<TNode> vars;
  expr::getVariables(n, vars);
  for (const auto& v : vars)
  {
    Trace("nl-icp") << "\tChecking " << n << " for " << v << std::endl;

    std::map<Node, Node> msum;
    ArithMSum::getMonomialSum(poly.getNode(), msum);

    Node veq_c;
    Node val;

    int isolated = ArithMSum::isolate(v, msum, veq_c, val, k);
    if (isolated == 1)
    {
      poly::Variable lhs = d_mapper(v);
      poly::SignCondition rel = poly::SignCondition::EQ;
      switch (k)
      {
        case Kind::LT: rel = poly::SignCondition::LT; break;
        case Kind::LEQ: rel = poly::SignCondition::LE; break;
        case Kind::EQUAL: rel = poly::SignCondition::EQ; break;
        case Kind::DISTINCT: rel = poly::SignCondition::NE; break;
        case Kind::GT: rel = poly::SignCondition::GT; break;
        case Kind::GEQ: rel = poly::SignCondition::GE; break;
        default: Assert(false) << "Unexpected kind: " << k;
      }
      poly::Rational rhsmult;
      poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult);
      rhsmult = poly::Rational(1) / rhsmult;
      // only correct up to a constant (denominator is thrown away!)
      if (!veq_c.isNull())
      {
        rhsmult = poly_utils::toRational(veq_c.getConst<Rational>());
      }
      Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)};
      Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl;
      result.emplace_back(res);
    }
    else if (isolated == -1)
    {
      poly::Variable lhs = d_mapper(v);
      poly::SignCondition rel = poly::SignCondition::EQ;
      switch (k)
      {
        case Kind::LT: rel = poly::SignCondition::GT; break;
        case Kind::LEQ: rel = poly::SignCondition::GE; break;
        case Kind::EQUAL: rel = poly::SignCondition::EQ; break;
        case Kind::DISTINCT: rel = poly::SignCondition::NE; break;
        case Kind::GT: rel = poly::SignCondition::LT; break;
        case Kind::GEQ: rel = poly::SignCondition::LE; break;
        default: Assert(false) << "Unexpected kind: " << k;
      }
      poly::Rational rhsmult;
      poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult);
      rhsmult = poly::Rational(1) / rhsmult;
      if (!veq_c.isNull())
      {
        rhsmult = poly_utils::toRational(veq_c.getConst<Rational>());
      }
      Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)};
      Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl;
      result.emplace_back(res);
    }
  }
  return result;
}

void ICPSolver::addCandidate(const Node& n)
{
  auto it = d_candidateCache.find(n);
  if (it != d_candidateCache.end())
  {
    for (const auto& c : it->second)
    {
      d_state.d_candidates.emplace_back(c);
    }
  }
  else
  {
    auto cands = constructCandidates(n);
    d_candidateCache.emplace(n, cands);
    for (const auto& c : cands)
    {
      d_state.d_candidates.emplace_back(c);
      Trace("nl-icp") << "Bumping budget because of the new candidate"
                      << std::endl;
      d_budget += d_budgetIncrement;
    }
  }
}

void ICPSolver::initOrigins()
{
  for (const auto& vars : d_state.d_bounds.get())
  {
    const Bounds& i = vars.second;
    Trace("nl-icp") << "Adding initial " << vars.first << " -> " << i
                    << std::endl;
    if (!i.lower_origin.isNull())
    {
      Trace("nl-icp") << "\tAdding lower " << i.lower_origin << std::endl;
      d_state.d_origins.add(vars.first, i.lower_origin, {});
    }
    if (!i.upper_origin.isNull())
    {
      Trace("nl-icp") << "\tAdding upper " << i.upper_origin << std::endl;
      d_state.d_origins.add(vars.first, i.upper_origin, {});
    }
  }
}

PropagationResult ICPSolver::doPropagationRound()
{
  if (d_budget <= 0)
  {
    Trace("nl-icp") << "ICP budget exceeded" << std::endl;
    return PropagationResult::NOT_CHANGED;
  }
  d_state.d_conflict.clear();
  Trace("nl-icp") << "Starting propagation with "
                  << IAWrapper{d_state.d_assignment, d_mapper} << std::endl;
  Trace("nl-icp") << "Current budget: " << d_budget << std::endl;
  PropagationResult res = PropagationResult::NOT_CHANGED;
  for (const auto& c : d_state.d_candidates)
  {
    --d_budget;
    PropagationResult cres = c.propagate(d_state.d_assignment, 100);
    switch (cres)
    {
      case PropagationResult::NOT_CHANGED: break;
      case PropagationResult::CONTRACTED:
      case PropagationResult::CONTRACTED_STRONGLY:
        d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables);
        res = PropagationResult::CONTRACTED;
        break;
      case PropagationResult::CONTRACTED_WITHOUT_CURRENT:
      case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
        d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables, false);
        res = PropagationResult::CONTRACTED;
        break;
      case PropagationResult::CONFLICT:
        d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables);
        d_state.d_conflict = d_state.d_origins.getOrigins(d_mapper(c.lhs));
        return PropagationResult::CONFLICT;
    }
    switch (cres)
    {
      case PropagationResult::CONTRACTED_STRONGLY:
      case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
        Trace("nl-icp") << "Bumping budget because of a strong contraction"
                        << std::endl;
        d_budget += d_budgetIncrement;
        break;
      default: break;
    }
  }
  return res;
}

std::vector<Node> ICPSolver::generateLemmas() const
{
  auto nm = NodeManager::currentNM();
  std::vector<Node> lemmas;

  for (const auto& vars : d_mapper.mVarCVCpoly)
  {
    if (!d_state.d_assignment.has(vars.second)) continue;
    Node v = vars.first;
    poly::Interval i = d_state.d_assignment.get(vars.second);
    if (!is_minus_infinity(get_lower(i)))
    {
      Kind rel = get_lower_open(i) ? Kind::GT : Kind::GEQ;
      Node c = nm->mkNode(rel, v, value_to_node(get_lower(i), v));
      if (!d_state.d_origins.isInOrigins(v, c))
      {
        Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
        Trace("nl-icp") << premise << " => " << c << std::endl;
        Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
        if (lemma.isConst())
        {
          Assert(lemma == nm->mkConst<bool>(true));
        }
        else
        {
          Trace("nl-icp") << "Adding lemma " << lemma << std::endl;
          lemmas.emplace_back(lemma);
        }
      }
    }
    if (!is_plus_infinity(get_upper(i)))
    {
      Kind rel = get_upper_open(i) ? Kind::LT : Kind::LEQ;
      Node c = nm->mkNode(rel, v, value_to_node(get_upper(i), v));
      if (!d_state.d_origins.isInOrigins(v, c))
      {
        Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
        Trace("nl-icp") << premise << " => " << c << std::endl;
        Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
        if (lemma.isConst())
        {
          Assert(lemma == nm->mkConst<bool>(true));
        }
        else
        {
          Trace("nl-icp") << "Adding lemma " << lemma << std::endl;
          lemmas.emplace_back(lemma);
        }
      }
    }
  }
  return lemmas;
}

void ICPSolver::reset(const std::vector<Node>& assertions)
{
  d_state.reset();
  for (const auto& n : assertions)
  {
    Trace("nl-icp") << "Adding " << n << std::endl;
    if (n.getKind() != Kind::CONST_BOOLEAN)
    {
      if (!d_state.d_bounds.add(n))
      {
        addCandidate(n);
      }
    }
  }
}

void ICPSolver::check()
{
  initOrigins();
  d_state.d_assignment = getBounds(d_mapper, d_state.d_bounds);
  bool did_progress = false;
  bool progress = false;
  do
  {
    switch (doPropagationRound())
    {
      case icp::PropagationResult::NOT_CHANGED: progress = false; break;
      case icp::PropagationResult::CONTRACTED:
      case icp::PropagationResult::CONTRACTED_STRONGLY:
      case icp::PropagationResult::CONTRACTED_WITHOUT_CURRENT:
      case icp::PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
        did_progress = true;
        progress = true;
        break;
      case icp::PropagationResult::CONFLICT:
        Trace("nl-icp") << "Found a conflict: " << d_state.d_conflict
                        << std::endl;

        std::vector<Node> mis;
        for (const auto& n : d_state.d_conflict)
        {
          mis.emplace_back(n.negate());
        }
        d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis),
                             InferenceId::ARITH_NL_ICP_CONFLICT);
        did_progress = true;
        progress = false;
        break;
    }
  } while (progress);
  if (did_progress)
  {
    std::vector<Node> lemmas = generateLemmas();
    for (const auto& l : lemmas)
    {
      d_im.addPendingLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION);
    }
  }
}

#else /* CVC5_POLY_IMP */

void ICPSolver::reset(const std::vector<Node>& assertions)
{
  Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
}

void ICPSolver::check()
{
  Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
}

#endif /* CVC5_POLY_IMP */

}  // namespace icp
}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer, Andres Noetzli
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		* Implements a ICP-based solver for nonlinear arithmetic.
14		*/
15
16		#include "theory/arith/nl/icp/icp_solver.h"
17
18		#include <iostream>
19
20		#include "base/check.h"
21		#include "base/output.h"
22		#include "expr/node_algorithm.h"
23		#include "theory/arith/arith_msum.h"
24		#include "theory/arith/inference_manager.h"
25		#include "theory/arith/nl/poly_conversion.h"
26		#include "theory/arith/normal_form.h"
27		#include "theory/rewriter.h"
28		#include "util/poly_util.h"
29
30		namespace cvc5 {
31		namespace theory {
32		namespace arith {
33		namespace nl {
34		namespace icp {
35
36		#ifdef CVC5_POLY_IMP
37
38		namespace {
39		/** A simple wrapper to nicely print an interval assignment. */
40		struct IAWrapper
41		{
42		const poly::IntervalAssignment& ia;
43		const VariableMapper& vm;
44		};
45		inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw)
46		{
47		os << "{ ";
48		bool first = true;
49		for (const auto& v : iaw.vm.mVarpolyCVC)
50		{
51		if (iaw.ia.has(v.first))
52		{
53		if (first)
54		{
55		first = false;
56		}
57		else
58		{
59		os << ", ";
60		}
61		os << v.first << " -> " << iaw.ia.get(v.first);
62		}
63		}
64		return os << " }";
65		}
66		} // namespace
67
68	9696	ICPSolver::ICPSolver(Env& env, InferenceManager& im)
69	9696	: EnvObj(env), d_im(im), d_state(d_mapper)
70		{
71	9696	}
72
73	30	std::vector<Node> ICPSolver::collectVariables(const Node& n) const
74		{
75	60	std::unordered_set<TNode> tmp;
76	30	expr::getVariables(n, tmp);
77	30	std::vector<Node> res;
78	62	for (const auto& t : tmp)
79		{
80	32	res.emplace_back(t);
81		}
82	60	return res;
83		}
84
85	92	std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
86		{
87	184	Node tmp = rewrite(n);
88	92	if (tmp.isConst())
89		{
90		return {};
91		}
92	184	auto comp = Comparison::parseNormalForm(tmp).decompose(false);
93	92	Kind k = std::get<1>(comp);
94	92	if (k == Kind::DISTINCT)
95		{
96	54	return {};
97		}
98	76	auto poly = std::get<0>(comp);
99
100	76	std::vector<Candidate> result;
101	76	std::unordered_set<TNode> vars;
102	38	expr::getVariables(n, vars);
103	104	for (const auto& v : vars)
104		{
105	66	Trace("nl-icp") << "\tChecking " << n << " for " << v << std::endl;
106
107	132	std::map<Node, Node> msum;
108	66	ArithMSum::getMonomialSum(poly.getNode(), msum);
109
110	132	Node veq_c;
111	132	Node val;
112
113	66	int isolated = ArithMSum::isolate(v, msum, veq_c, val, k);
114	66	if (isolated == 1)
115		{
116	20	poly::Variable lhs = d_mapper(v);
117	20	poly::SignCondition rel = poly::SignCondition::EQ;
118	20	switch (k)
119		{
120	6	case Kind::LT: rel = poly::SignCondition::LT; break;
121		case Kind::LEQ: rel = poly::SignCondition::LE; break;
122	14	case Kind::EQUAL: rel = poly::SignCondition::EQ; break;
123		case Kind::DISTINCT: rel = poly::SignCondition::NE; break;
124		case Kind::GT: rel = poly::SignCondition::GT; break;
125		case Kind::GEQ: rel = poly::SignCondition::GE; break;
126		default: Assert(false) << "Unexpected kind: " << k;
127		}
128	40	poly::Rational rhsmult;
129	40	poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult);
130	20	rhsmult = poly::Rational(1) / rhsmult;
131		// only correct up to a constant (denominator is thrown away!)
132	20	if (!veq_c.isNull())
133		{
134		rhsmult = poly_utils::toRational(veq_c.getConst<Rational>());
135		}
136	40	Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)};
137	20	Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl;
138	20	result.emplace_back(res);
139		}
140	46	else if (isolated == -1)
141		{
142	10	poly::Variable lhs = d_mapper(v);
143	10	poly::SignCondition rel = poly::SignCondition::EQ;
144	10	switch (k)
145		{
146	10	case Kind::LT: rel = poly::SignCondition::GT; break;
147		case Kind::LEQ: rel = poly::SignCondition::GE; break;
148		case Kind::EQUAL: rel = poly::SignCondition::EQ; break;
149		case Kind::DISTINCT: rel = poly::SignCondition::NE; break;
150		case Kind::GT: rel = poly::SignCondition::LT; break;
151		case Kind::GEQ: rel = poly::SignCondition::LE; break;
152		default: Assert(false) << "Unexpected kind: " << k;
153		}
154	20	poly::Rational rhsmult;
155	20	poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult);
156	10	rhsmult = poly::Rational(1) / rhsmult;
157	10	if (!veq_c.isNull())
158		{
159		rhsmult = poly_utils::toRational(veq_c.getConst<Rational>());
160		}
161	20	Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)};
162	10	Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl;
163	10	result.emplace_back(res);
164		}
165		}
166	38	return result;
167		}
168
169	848	void ICPSolver::addCandidate(const Node& n)
170		{
171	848	auto it = d_candidateCache.find(n);
172	848	if (it != d_candidateCache.end())
173		{
174	884	for (const auto& c : it->second)
175		{
176	128	d_state.d_candidates.emplace_back(c);
177		}
178		}
179		else
180		{
181	184	auto cands = constructCandidates(n);
182	92	d_candidateCache.emplace(n, cands);
183	122	for (const auto& c : cands)
184		{
185	30	d_state.d_candidates.emplace_back(c);
186	60	Trace("nl-icp") << "Bumping budget because of the new candidate"
187	30	<< std::endl;
188	30	d_budget += d_budgetIncrement;
189		}
190		}
191	848	}
192
193	48	void ICPSolver::initOrigins()
194		{
195	140	for (const auto& vars : d_state.d_bounds.get())
196		{
197	92	const Bounds& i = vars.second;
198	184	Trace("nl-icp") << "Adding initial " << vars.first << " -> " << i
199	92	<< std::endl;
200	92	if (!i.lower_origin.isNull())
201		{
202	80	Trace("nl-icp") << "\tAdding lower " << i.lower_origin << std::endl;
203	80	d_state.d_origins.add(vars.first, i.lower_origin, {});
204		}
205	92	if (!i.upper_origin.isNull())
206		{
207	72	Trace("nl-icp") << "\tAdding upper " << i.upper_origin << std::endl;
208	72	d_state.d_origins.add(vars.first, i.upper_origin, {});
209		}
210		}
211	48	}
212
213	52	PropagationResult ICPSolver::doPropagationRound()
214		{
215	52	if (d_budget <= 0)
216		{
217		Trace("nl-icp") << "ICP budget exceeded" << std::endl;
218		return PropagationResult::NOT_CHANGED;
219		}
220	52	d_state.d_conflict.clear();
221	104	Trace("nl-icp") << "Starting propagation with "
222	52	<< IAWrapper{d_state.d_assignment, d_mapper} << std::endl;
223	52	Trace("nl-icp") << "Current budget: " << d_budget << std::endl;
224	52	PropagationResult res = PropagationResult::NOT_CHANGED;
225	216	for (const auto& c : d_state.d_candidates)
226		{
227	166	--d_budget;
228	166	PropagationResult cres = c.propagate(d_state.d_assignment, 100);
229	166	switch (cres)
230		{
231	160	case PropagationResult::NOT_CHANGED: break;
232		case PropagationResult::CONTRACTED:
233		case PropagationResult::CONTRACTED_STRONGLY:
234		d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables);
235		res = PropagationResult::CONTRACTED;
236		break;
237	4	case PropagationResult::CONTRACTED_WITHOUT_CURRENT:
238		case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
239	4	d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables, false);
240	4	res = PropagationResult::CONTRACTED;
241	4	break;
242	2	case PropagationResult::CONFLICT:
243	2	d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables);
244	2	d_state.d_conflict = d_state.d_origins.getOrigins(d_mapper(c.lhs));
245	2	return PropagationResult::CONFLICT;
246		}
247	164	switch (cres)
248		{
249	4	case PropagationResult::CONTRACTED_STRONGLY:
250		case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
251	8	Trace("nl-icp") << "Bumping budget because of a strong contraction"
252	4	<< std::endl;
253	4	d_budget += d_budgetIncrement;
254	4	break;
255	160	default: break;
256		}
257		}
258	50	return res;
259		}
260
261	6	std::vector<Node> ICPSolver::generateLemmas() const
262		{
263	6	auto nm = NodeManager::currentNM();
264	6	std::vector<Node> lemmas;
265
266	18	for (const auto& vars : d_mapper.mVarCVCpoly)
267		{
268	12	if (!d_state.d_assignment.has(vars.second)) continue;
269	24	Node v = vars.first;
270	24	poly::Interval i = d_state.d_assignment.get(vars.second);
271	12	if (!is_minus_infinity(get_lower(i)))
272		{
273	12	Kind rel = get_lower_open(i) ? Kind::GT : Kind::GEQ;
274	24	Node c = nm->mkNode(rel, v, value_to_node(get_lower(i), v));
275	12	if (!d_state.d_origins.isInOrigins(v, c))
276		{
277	24	Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
278	12	Trace("nl-icp") << premise << " => " << c << std::endl;
279	24	Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
280	12	if (lemma.isConst())
281		{
282		Assert(lemma == nm->mkConst<bool>(true));
283		}
284		else
285		{
286	12	Trace("nl-icp") << "Adding lemma " << lemma << std::endl;
287	12	lemmas.emplace_back(lemma);
288		}
289		}
290		}
291	12	if (!is_plus_infinity(get_upper(i)))
292		{
293	10	Kind rel = get_upper_open(i) ? Kind::LT : Kind::LEQ;
294	20	Node c = nm->mkNode(rel, v, value_to_node(get_upper(i), v));
295	10	if (!d_state.d_origins.isInOrigins(v, c))
296		{
297	20	Node premise = nm->mkAnd(d_state.d_origins.getOrigins(v));
298	10	Trace("nl-icp") << premise << " => " << c << std::endl;
299	20	Node lemma = rewrite(nm->mkNode(Kind::IMPLIES, premise, c));
300	10	if (lemma.isConst())
301		{
302		Assert(lemma == nm->mkConst<bool>(true));
303		}
304		else
305		{
306	10	Trace("nl-icp") << "Adding lemma " << lemma << std::endl;
307	10	lemmas.emplace_back(lemma);
308		}
309		}
310		}
311		}
312	6	return lemmas;
313		}
314
315	48	void ICPSolver::reset(const std::vector<Node>& assertions)
316		{
317	48	d_state.reset();
318	1038	for (const auto& n : assertions)
319		{
320	990	Trace("nl-icp") << "Adding " << n << std::endl;
321	990	if (n.getKind() != Kind::CONST_BOOLEAN)
322		{
323	990	if (!d_state.d_bounds.add(n))
324		{
325	848	addCandidate(n);
326		}
327		}
328		}
329	48	}
330
331	48	void ICPSolver::check()
332		{
333	48	initOrigins();
334	48	d_state.d_assignment = getBounds(d_mapper, d_state.d_bounds);
335	48	bool did_progress = false;
336	48	bool progress = false;
337	52	do
338		{
339	52	switch (doPropagationRound())
340		{
341	46	case icp::PropagationResult::NOT_CHANGED: progress = false; break;
342	4	case icp::PropagationResult::CONTRACTED:
343		case icp::PropagationResult::CONTRACTED_STRONGLY:
344		case icp::PropagationResult::CONTRACTED_WITHOUT_CURRENT:
345		case icp::PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT:
346	4	did_progress = true;
347	4	progress = true;
348	4	break;
349	2	case icp::PropagationResult::CONFLICT:
350	4	Trace("nl-icp") << "Found a conflict: " << d_state.d_conflict
351	2	<< std::endl;
352
353	4	std::vector<Node> mis;
354	8	for (const auto& n : d_state.d_conflict)
355		{
356	6	mis.emplace_back(n.negate());
357		}
358	2	d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis),
359		InferenceId::ARITH_NL_ICP_CONFLICT);
360	2	did_progress = true;
361	2	progress = false;
362	2	break;
363		}
364		} while (progress);
365	48	if (did_progress)
366		{
367	12	std::vector<Node> lemmas = generateLemmas();
368	28	for (const auto& l : lemmas)
369		{
370	22	d_im.addPendingLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION);
371		}
372		}
373	48	}
374
375		#else /* CVC5_POLY_IMP */
376
377		void ICPSolver::reset(const std::vector<Node>& assertions)
378		{
379		Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
380		}
381
382		void ICPSolver::check()
383		{
384		Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
385		}
386
387		#endif /* CVC5_POLY_IMP */
388
389		} // namespace icp
390		} // namespace nl
391		} // namespace arith
392		} // namespace theory
393	31137	} // namespace cvc5