GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/icp/icp_solver.cpp Lines: 1 5 20.0 %
Date: 2021-03-22 Branches: 2 16 12.5 %

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