GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/icp/icp_solver.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file icp_solver.h
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
#ifndef CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
16
#define CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
17
18
#include "cvc4_private.h"
19
20
#ifdef CVC4_POLY_IMP
21
#include <poly/polyxx.h>
22
#endif /* CVC4_POLY_IMP */
23
24
#include "expr/node.h"
25
#include "theory/arith/bound_inference.h"
26
#include "theory/arith/nl/icp/candidate.h"
27
#include "theory/arith/nl/icp/contraction_origins.h"
28
#include "theory/arith/nl/icp/intersection.h"
29
#include "theory/arith/nl/poly_conversion.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
class InferenceManager;
36
37
namespace nl {
38
namespace icp {
39
40
#ifdef CVC4_POLY_IMP
41
42
/**
43
 * This class implements an ICP-based solver. As it is intended to be used in
44
 * conjunction with other solvers, it only performs contractions, but does not
45
 * issue splits.
46
 *
47
 * In essence, interval constraint propagation has candidates (like x = y^2-z),
48
 * evaluates their right hand side over the current (interval) assignment and
49
 * uses the resulting interval to make the interval of the left-hand side
50
 * variable smaller (contract it).
51
 *
52
 * These contractions can yield to a conflict (if the interval of some variable
53
 * becomes empty) or shrink the search space for a variable.
54
 */
55
class ICPSolver
56
{
57
  /**
58
   * This encapsulates the state of the ICP solver that is local to a single
59
   * theory call. It contains the variable bounds and candidates derived from
60
   * the assertions, the origins manager and the last conflict.
61
   */
62
  struct ICPState
63
  {
64
    /** The variable bounds extracted from the input assertions */
65
    BoundInference d_bounds;
66
    /** The contraction candidates generated from the theory atoms */
67
    std::vector<Candidate> d_candidates;
68
    /** The current assignment */
69
    poly::IntervalAssignment d_assignment;
70
    /** The origins for the current assignment */
71
    ContractionOriginManager d_origins;
72
    /** The conflict, if any way found. Initially empty */
73
    std::vector<Node> d_conflict;
74
75
    /** Initialized the variable bounds with a variable mapper */
76
    ICPState(VariableMapper& vm) {}
77
78
    /** Reset this state */
79
    void reset()
80
    {
81
      d_bounds = BoundInference();
82
      d_candidates.clear();
83
      d_assignment.clear();
84
      d_origins = ContractionOriginManager();
85
      d_conflict.clear();
86
    }
87
  };
88
89
  /** Maps Node (variables) to poly::Variable */
90
  VariableMapper d_mapper;
91
  /** The inference manager */
92
  InferenceManager& d_im;
93
  /** Cache candidates to avoid reconstruction for every theory call */
94
  std::map<Node, std::vector<Candidate>> d_candidateCache;
95
  /** The current state */
96
  ICPState d_state;
97
98
  /** The remaining budget */
99
  std::int64_t d_budget = 0;
100
  /** The budget increment for new candidates and strong contractions */
101
  static constexpr std::int64_t d_budgetIncrement = 10;
102
103
  /** Collect all variables from a node */
104
  std::vector<Node> collectVariables(const Node& n) const;
105
  /** Construct all possible candidates from a given theory atom */
106
  std::vector<Candidate> constructCandidates(const Node& n);
107
  /** Add the given node as candidate */
108
  void addCandidate(const Node& n);
109
  /** Initialize the origin manager from the variable bounds */
110
  void initOrigins();
111
112
  /**
113
   * Perform one contraction with every candidate.
114
   * If any candidate yields a conflict stops immediately and returns
115
   * PropagationResult::CONFLICT. If any candidate yields a contraction returns
116
   * PropagationResult::CONTRACTED. Otherwise returns
117
   * PropagationResult::NOT_CHANGED.
118
   */
119
  PropagationResult doPropagationRound();
120
121
  /**
122
   * Construct lemmas for all bounds that have been improved.
123
   * For every improved bound, all origins are collected and a lemma of the form
124
   *   (and origins)  ==>  (new bound)
125
   * is constructed.
126
   */
127
  std::vector<Node> generateLemmas() const;
128
129
 public:
130
  ICPSolver(InferenceManager& im) : d_im(im), d_state(d_mapper) {}
131
  /** Reset this solver for the next theory call */
132
  void reset(const std::vector<Node>& assertions);
133
134
  /**
135
   * Performs a full ICP check.
136
   */
137
  void check();
138
};
139
140
#else /* CVC4_POLY_IMP */
141
142
class ICPSolver
143
{
144
 public:
145
4391
  ICPSolver(InferenceManager& im) {}
146
  void reset(const std::vector<Node>& assertions);
147
  void check();
148
};
149
150
#endif /* CVC4_POLY_IMP */
151
152
}  // namespace icp
153
}  // namespace nl
154
}  // namespace arith
155
}  // namespace theory
156
}  // namespace CVC4
157
158
#endif