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

Line Exec Source
1
/*********************                                                        */
2
/*! \file nonlinear_extension.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Tim King
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 Extensions for incomplete handling of nonlinear multiplication.
13
 **
14
 ** Extensions to the theory of arithmetic incomplete handling of nonlinear
15
 ** multiplication via axiom instantiations.
16
 **/
17
18
#ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
19
#define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
20
21
#include <map>
22
#include <vector>
23
24
#include "expr/node.h"
25
#include "theory/arith/nl/cad_solver.h"
26
#include "theory/arith/nl/ext/ext_state.h"
27
#include "theory/arith/nl/ext/factoring_check.h"
28
#include "theory/arith/nl/ext/monomial_bounds_check.h"
29
#include "theory/arith/nl/ext/monomial_check.h"
30
#include "theory/arith/nl/ext/proof_checker.h"
31
#include "theory/arith/nl/ext/split_zero_check.h"
32
#include "theory/arith/nl/ext/tangent_plane_check.h"
33
#include "theory/arith/nl/ext_theory_callback.h"
34
#include "theory/arith/nl/iand_solver.h"
35
#include "theory/arith/nl/icp/icp_solver.h"
36
#include "theory/arith/nl/nl_model.h"
37
#include "theory/arith/nl/stats.h"
38
#include "theory/arith/nl/strategy.h"
39
#include "theory/arith/nl/transcendental/transcendental_solver.h"
40
#include "theory/ext_theory.h"
41
#include "theory/theory.h"
42
43
namespace CVC4 {
44
namespace theory {
45
namespace eq {
46
  class EqualityEngine;
47
}
48
namespace arith {
49
50
class InferenceManager;
51
class TheoryArith;
52
53
namespace nl {
54
55
class NlLemma;
56
57
/** Non-linear extension class
58
 *
59
 * This class implements model-based refinement schemes
60
 * for non-linear arithmetic, described in:
61
 *
62
 * - "Invariant Checking of NRA Transition Systems
63
 * via Incremental Reduction to LRA with EUF" by
64
 * Cimatti et al., TACAS 2017.
65
 *
66
 * - Section 5 of "Desiging Theory Solvers with
67
 * Extensions" by Reynolds et al., FroCoS 2017.
68
 *
69
 * - "Satisfiability Modulo Transcendental
70
 * Functions via Incremental Linearization" by Cimatti
71
 * et al., CADE 2017.
72
 *
73
 * It's main functionality is a check(...) method,
74
 * which is called by TheoryArithPrivate either:
75
 * (1) at full effort with no conflicts or lemmas emitted, or
76
 * (2) at last call effort.
77
 * In this method, this class calls d_im.lemma(...)
78
 * for valid arithmetic theory lemmas, based on the current set of assertions,
79
 * where d_im is the inference manager of TheoryArith.
80
 */
81
class NonlinearExtension
82
{
83
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
84
85
 public:
86
  NonlinearExtension(TheoryArith& containing,
87
                     ArithState& state,
88
                     eq::EqualityEngine* ee,
89
                     ProofNodeManager* pnm);
90
  ~NonlinearExtension();
91
  /**
92
   * Does non-context dependent setup for a node connected to a theory.
93
   */
94
  void preRegisterTerm(TNode n);
95
  /** Check at effort level e.
96
   *
97
   * This call may result in (possibly multiple) calls to d_im.lemma(...)
98
   * where d_im is the inference manager of TheoryArith.
99
   *
100
   * If e is FULL, then we add lemmas based on context-depedent
101
   * simplification (see Reynolds et al FroCoS 2017).
102
   *
103
   * If e is LAST_CALL, we add lemmas based on model-based refinement
104
   * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this
105
   * effort may be computed during a call to interceptModel as described below.
106
   */
107
  void check(Theory::Effort e);
108
  /** intercept model
109
   *
110
   * This method is called during TheoryArith::collectModelInfo, which is
111
   * invoked after the linear arithmetic solver passes a full effort check
112
   * with no lemmas.
113
   *
114
   * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
115
   * which represents the linear arithmetic theory solver's contribution to the
116
   * current candidate model. That is, its collectModelInfo method is requesting
117
   * that equalities v1 = c1, ..., vn = cn be added to the current model, where
118
   * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice
119
   * arithmetic variables may be real-valued terms belonging to other theories,
120
   * or abstractions of applications of multiplication (kind NONLINEAR_MULT).
121
   *
122
   * This method requests that the non-linear solver inspect this model and
123
   * do any number of the following:
124
   * (1) Construct lemmas based on a model-based refinement procedure inspired
125
   * by Cimatti et al., TACAS 2017.,
126
   * (2) In the case that the nonlinear solver finds that the current
127
   * constraints are satisfiable, it may "repair" the values in the argument
128
   * arithModel so that it satisfies certain nonlinear constraints. This may
129
   * involve e.g. solving for variables in nonlinear equations.
130
   */
131
  void interceptModel(std::map<Node, Node>& arithModel,
132
                      const std::set<Node>& termSet);
133
  /** Does this class need a call to check(...) at last call effort? */
134
18876
  bool needsCheckLastEffort() const { return d_needsLastCall; }
135
  /** presolve
136
   *
137
   * This function is called during TheoryArith's presolve command.
138
   * In this function, we send lemmas we accumulated during preprocessing,
139
   * for instance, definitional lemmas from expandDefinitions are sent out
140
   * on the output channel of TheoryArith in this function.
141
   */
142
  void presolve();
143
144
  /** Process side effect se */
145
  void processSideEffect(const NlLemma& se);
146
147
 private:
148
  /** Model-based refinement
149
   *
150
   * This is the main entry point of this class for generating lemmas on the
151
   * output channel of the theory of arithmetic.
152
   *
153
   * It is currently run at last call effort. It applies lemma schemas
154
   * described in Reynolds et al. FroCoS 2017 that are based on ruling out
155
   * the current candidate model.
156
   *
157
   * This function returns true if a lemma was added to the inference manager.
158
   * Otherwise, it returns false. In the latter case, the model object d_model
159
   * may have information regarding how to construct a model, in the case that
160
   * we determined the problem is satisfiable.
161
   */
162
  bool modelBasedRefinement(const std::set<Node>& termSet);
163
164
  /** get assertions
165
   *
166
   * Let M be the set of assertions known by THEORY_ARITH. This function adds a
167
   * set of literals M' to assertions such that M' and M are equivalent.
168
   *
169
   * Examples of how M' differs with M:
170
   * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where
171
   * c and c' are constants,
172
   * (2) M' may contain t = c if both t >= c and t <= c are in M.
173
   */
174
  void getAssertions(std::vector<Node>& assertions);
175
  /** check model
176
   *
177
   * Returns the subset of assertions whose concrete values we cannot show are
178
   * true in the current model. Notice that we typically cannot compute concrete
179
   * values for assertions involving transcendental functions. Any assertion
180
   * whose model value cannot be computed is included in the return value of
181
   * this function.
182
   */
183
  std::vector<Node> checkModelEval(const std::vector<Node>& assertions);
184
185
  //---------------------------check model
186
  /** Check model
187
   *
188
   * Checks the current model based on solving for equalities, and using error
189
   * bounds on the Taylor approximation.
190
   *
191
   * If this function returns true, then all assertions in the input argument
192
   * "assertions" are satisfied for all interpretations of variables within
193
   * their computed bounds (as stored in d_check_model_bounds).
194
   *
195
   * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
196
   * "Detecting Satisfiable Formulas".
197
   */
198
  bool checkModel(const std::vector<Node>& assertions);
199
  //---------------------------end check model
200
  /** compute relevant assertions */
201
  void computeRelevantAssertions(const std::vector<Node>& assertions,
202
                                 std::vector<Node>& keep);
203
204
  /** run check strategy
205
   *
206
   * Check assertions for consistency in the effort LAST_CALL with a subset of
207
   * the assertions, false_asserts, that evaluate to false in the current model.
208
   *
209
   * xts : the list of (non-reduced) extended terms in the current context.
210
   *
211
   * This method adds lemmas to d_im directly.
212
   */
213
  void runStrategy(Theory::Effort effort,
214
                   const std::vector<Node>& assertions,
215
                   const std::vector<Node>& false_asserts,
216
                   const std::vector<Node>& xts);
217
218
  /** commonly used terms */
219
  Node d_zero;
220
  Node d_one;
221
  Node d_neg_one;
222
  Node d_true;
223
  // The theory of arithmetic containing this extension.
224
  TheoryArith& d_containing;
225
  InferenceManager& d_im;
226
  /** The statistics class */
227
  NlStats d_stats;
228
  // needs last call effort
229
  bool d_needsLastCall;
230
  /**
231
   * The number of times we have the called main check method
232
   * (modelBasedRefinement). This counter is used for interleaving strategies.
233
   */
234
  unsigned d_checkCounter;
235
  /** The callback for the extended theory below */
236
  NlExtTheoryCallback d_extTheoryCb;
237
  /** Extended theory, responsible for context-dependent simplification. */
238
  ExtTheory d_extTheory;
239
  /** The non-linear model object
240
   *
241
   * This class is responsible for computing model values for arithmetic terms
242
   * and for establishing when we are able to answer "SAT".
243
   */
244
  NlModel d_model;
245
246
  /** The transcendental extension object
247
   *
248
   * This is the subsolver responsible for running the procedure for
249
   * transcendental functions.
250
   */
251
  transcendental::TranscendentalSolver d_trSlv;
252
  /** The proof checker for proofs of the nlext. */
253
  ExtProofRuleChecker d_proofChecker;
254
  /**
255
   * Holds common lookup data for the checks implemented in the "nl-ext"
256
   * solvers (from Cimatti et al., TACAS 2017).
257
   */
258
  ExtState d_extState;
259
  /** Solver for factoring lemmas. */
260
  FactoringCheck d_factoringSlv;
261
  /** Solver for lemmas about monomial bounds. */
262
  MonomialBoundsCheck d_monomialBoundsSlv;
263
  /** Solver for lemmas about monomials. */
264
  MonomialCheck d_monomialSlv;
265
  /** Solver for lemmas that split multiplication at zero. */
266
  SplitZeroCheck d_splitZeroSlv;
267
  /** Solver for tangent plane lemmas. */
268
  TangentPlaneCheck d_tangentPlaneSlv;
269
  /** The CAD-based solver */
270
  CadSolver d_cadSlv;
271
  /** The ICP-based solver */
272
  icp::ICPSolver d_icpSlv;
273
  /** The integer and solver
274
   *
275
   * This is the subsolver responsible for running the procedure for
276
   * constraints involving integer and.
277
   */
278
  IAndSolver d_iandSlv;
279
280
  /** The strategy for the nonlinear extension. */
281
  Strategy d_strategy;
282
283
  /**
284
   * The approximations computed during collectModelInfo. For details, see
285
   * NlModel::getModelValueRepair.
286
   */
287
  std::map<Node, std::pair<Node, Node>> d_approximations;
288
  /**
289
   * The witnesses computed during collectModelInfo. For details, see
290
   * NlModel::getModelValueRepair.
291
   */
292
  std::map<Node, Node> d_witnesses;
293
  /** have we successfully built the model in this SAT context? */
294
  context::CDO<bool> d_builtModel;
295
}; /* class NonlinearExtension */
296
297
}  // namespace nl
298
}  // namespace arith
299
}  // namespace theory
300
}  // namespace CVC4
301
302
#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */