1 /********************* */
2 /*! \file nonlinear_extension.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Tianyi Liang
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Extensions for incomplete handling of nonlinear multiplication.
14 ** Extensions to the theory of arithmetic incomplete handling of nonlinear
15 ** multiplication via axiom instantiations.
18 #ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
19 #define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
26 #include "context/cdlist.h"
27 #include "expr/kind.h"
28 #include "expr/node.h"
29 #include "theory/arith/nl/cad_solver.h"
30 #include "theory/arith/nl/iand_solver.h"
31 #include "theory/arith/nl/nl_lemma_utils.h"
32 #include "theory/arith/nl/nl_model.h"
33 #include "theory/arith/nl/nl_solver.h"
34 #include "theory/arith/nl/stats.h"
35 #include "theory/arith/nl/transcendental_solver.h"
36 #include "theory/arith/theory_arith.h"
37 #include "theory/ext_theory.h"
38 #include "theory/uf/equality_engine.h"
45 /** Non-linear extension class
47 * This class implements model-based refinement schemes
48 * for non-linear arithmetic, described in:
50 * - "Invariant Checking of NRA Transition Systems
51 * via Incremental Reduction to LRA with EUF" by
52 * Cimatti et al., TACAS 2017.
54 * - Section 5 of "Desiging Theory Solvers with
55 * Extensions" by Reynolds et al., FroCoS 2017.
57 * - "Satisfiability Modulo Transcendental
58 * Functions via Incremental Linearization" by Cimatti
61 * It's main functionality is a check(...) method,
62 * which is called by TheoryArithPrivate either:
63 * (1) at full effort with no conflicts or lemmas emitted, or
64 * (2) at last call effort.
65 * In this method, this class calls d_out->lemma(...)
66 * for valid arithmetic theory lemmas, based on the current set of assertions,
67 * where d_out is the output channel of TheoryArith.
69 class NonlinearExtension
71 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
74 NonlinearExtension(TheoryArith
& containing
, eq::EqualityEngine
* ee
);
75 ~NonlinearExtension();
77 * Does non-context dependent setup for a node connected to a theory.
79 void preRegisterTerm(TNode n
);
80 /** Get current substitution
82 * This function and the one below are
83 * used for context-dependent
84 * simplification, see Section 3.1 of
85 * "Designing Theory Solvers with Extensions"
86 * by Reynolds et al. FroCoS 2017.
88 * effort : an identifier indicating the stage where
89 * we are performing context-dependent simplification,
90 * vars : a set of arithmetic variables.
92 * This function populates subs and exp, such that for 0 <= i < vars.size():
93 * ( exp[vars[i]] ) => vars[i] = subs[i]
94 * where exp[vars[i]] is a set of assertions
95 * that hold in the current context. We call { vars -> subs } a "derivable
96 * substituion" (see Reynolds et al. FroCoS 2017).
98 bool getCurrentSubstitution(int effort
,
99 const std::vector
<Node
>& vars
,
100 std::vector
<Node
>& subs
,
101 std::map
<Node
, std::vector
<Node
>>& exp
);
102 /** Is the term n in reduced form?
104 * Used for context-dependent simplification.
106 * effort : an identifier indicating the stage where
107 * we are performing context-dependent simplification,
108 * on : the original term that we reduced to n,
109 * exp : an explanation such that ( exp => on = n ).
111 * We return a pair ( b, exp' ) such that
112 * if b is true, then:
113 * n is in reduced form
114 * if exp' is non-null, then ( exp' => on = n )
115 * The second part of the pair is used for constructing
116 * minimal explanations for context-dependent simplifications.
118 std::pair
<bool, Node
> isExtfReduced(int effort
,
121 const std::vector
<Node
>& exp
) const;
122 /** Check at effort level e.
124 * This call may result in (possibly multiple) calls to d_out->lemma(...)
125 * where d_out is the output channel of TheoryArith.
127 * If e is FULL, then we add lemmas based on context-depedent
128 * simplification (see Reynolds et al FroCoS 2017).
130 * If e is LAST_CALL, we add lemmas based on model-based refinement
131 * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this
132 * effort may be computed during a call to interceptModel as described below.
134 void check(Theory::Effort e
);
137 * This method is called during TheoryArith::collectModelInfo, which is
138 * invoked after the linear arithmetic solver passes a full effort check
141 * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
142 * which represents the linear arithmetic theory solver's contribution to the
143 * current candidate model. That is, its collectModelInfo method is requesting
144 * that equalities v1 = c1, ..., vn = cn be added to the current model, where
145 * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice
146 * arithmetic variables may be real-valued terms belonging to other theories,
147 * or abstractions of applications of multiplication (kind NONLINEAR_MULT).
149 * This method requests that the non-linear solver inspect this model and
150 * do any number of the following:
151 * (1) Construct lemmas based on a model-based refinement procedure inspired
152 * by Cimatti et al., TACAS 2017.,
153 * (2) In the case that the nonlinear solver finds that the current
154 * constraints are satisfiable, it may "repair" the values in the argument
155 * arithModel so that it satisfies certain nonlinear constraints. This may
156 * involve e.g. solving for variables in nonlinear equations.
158 * Notice that in the former case, the lemmas it constructs are not sent out
159 * immediately. Instead, they are put in temporary vector d_cmiLemmas, which
160 * are then sent out (if necessary) when a last call
161 * effort check is issued to this class.
163 void interceptModel(std::map
<Node
, Node
>& arithModel
);
164 /** Does this class need a call to check(...) at last call effort? */
165 bool needsCheckLastEffort() const { return d_needsLastCall
; }
168 * This function is called during TheoryArith's presolve command.
169 * In this function, we send lemmas we accumulated during preprocessing,
170 * for instance, definitional lemmas from expandDefinitions are sent out
171 * on the output channel of TheoryArith in this function.
176 /** Model-based refinement
178 * This is the main entry point of this class for generating lemmas on the
179 * output channel of the theory of arithmetic.
181 * It is currently run at last call effort. It applies lemma schemas
182 * described in Reynolds et al. FroCoS 2017 that are based on ruling out
183 * the current candidate model.
185 * This function returns true if a lemma was added to the vector lems.
186 * Otherwise, it returns false. In the latter case, the model object d_model
187 * may have information regarding how to construct a model, in the case that
188 * we determined the problem is satisfiable.
190 bool modelBasedRefinement(std::vector
<NlLemma
>& mlems
);
194 * Check assertions for consistency in the effort LAST_CALL with a subset of
195 * the assertions, false_asserts, that evaluate to false in the current model.
197 * xts : the list of (non-reduced) extended terms in the current context.
199 * This method adds lemmas to arguments lems and wlems, each of
200 * which are intended to be sent out on the output channel of TheoryArith
201 * under certain conditions.
203 * If the set lems is non-empty, then no further processing is
204 * necessary. The last call effort check should terminate and these
205 * lemmas should be sent.
207 * The "waiting" lemmas wlems contain lemmas that should be sent on the
208 * output channel as a last resort. In other words, only if we are not
209 * able to establish SAT via a call to checkModel(...) should wlems be
210 * considered. This set typically contains tangent plane lemmas.
212 int checkLastCall(const std::vector
<Node
>& assertions
,
213 const std::vector
<Node
>& false_asserts
,
214 const std::vector
<Node
>& xts
,
215 std::vector
<NlLemma
>& lems
,
216 std::vector
<NlLemma
>& wlems
);
220 * Let M be the set of assertions known by THEORY_ARITH. This function adds a
221 * set of literals M' to assertions such that M' and M are equivalent.
223 * Examples of how M' differs with M:
224 * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where
225 * c and c' are constants,
226 * (2) M' may contain t = c if both t >= c and t <= c are in M.
228 void getAssertions(std::vector
<Node
>& assertions
);
231 * Returns the subset of assertions whose concrete values we cannot show are
232 * true in the current model. Notice that we typically cannot compute concrete
233 * values for assertions involving transcendental functions. Any assertion
234 * whose model value cannot be computed is included in the return value of
237 std::vector
<Node
> checkModelEval(const std::vector
<Node
>& assertions
);
239 //---------------------------check model
242 * Checks the current model based on solving for equalities, and using error
243 * bounds on the Taylor approximation.
245 * If this function returns true, then all assertions in the input argument
246 * "assertions" are satisfied for all interpretations of variables within
247 * their computed bounds (as stored in d_check_model_bounds).
249 * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
250 * "Detecting Satisfiable Formulas".
252 * The arguments lemmas and gs store the lemmas and guard literals to be sent
253 * out on the output channel of TheoryArith as lemmas and calls to
254 * ensureLiteral respectively.
256 bool checkModel(const std::vector
<Node
>& assertions
,
257 const std::vector
<Node
>& false_asserts
,
258 std::vector
<NlLemma
>& lemmas
,
259 std::vector
<Node
>& gs
);
260 //---------------------------end check model
263 * Potentially adds lemmas to the set out and clears lemmas. Returns
264 * the number of lemmas added to out. We do not add lemmas that have already
265 * been sent on the output channel of TheoryArith.
267 unsigned filterLemmas(std::vector
<NlLemma
>& lemmas
,
268 std::vector
<NlLemma
>& out
);
269 /** singleton version of above */
270 unsigned filterLemma(NlLemma lem
, std::vector
<NlLemma
>& out
);
273 * Send lemmas in out on the output channel of theory of arithmetic.
275 void sendLemmas(const std::vector
<NlLemma
>& out
);
276 /** Process side effect se */
277 void processSideEffect(const NlLemma
& se
);
279 /** cache of all lemmas sent on the output channel (user-context-dependent) */
281 /** Same as above, for preprocessed lemmas */
283 /** commonly used terms */
288 // The theory of arithmetic containing this extension.
289 TheoryArith
& d_containing
;
290 // pointer to used equality engine
291 eq::EqualityEngine
* d_ee
;
292 /** The statistics class */
294 // needs last call effort
295 bool d_needsLastCall
;
296 /** Extended theory, responsible for context-dependent simplification. */
297 ExtTheory d_extTheory
;
298 /** The non-linear model object
300 * This class is responsible for computing model values for arithmetic terms
301 * and for establishing when we are able to answer "SAT".
304 /** The transcendental extension object
306 * This is the subsolver responsible for running the procedure for
307 * transcendental functions.
309 TranscendentalSolver d_trSlv
;
310 /** The nonlinear extension object
312 * This is the subsolver responsible for running the procedure for
313 * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017.
316 /** The CAD-based solver */
318 /** The integer and solver
320 * This is the subsolver responsible for running the procedure for
321 * constraints involving integer and.
323 IAndSolver d_iandSlv
;
325 * The lemmas we computed during collectModelInfo, to be sent out on the
326 * output channel of TheoryArith.
328 std::vector
<NlLemma
> d_cmiLemmas
;
330 * The approximations computed during collectModelInfo. For details, see
331 * NlModel::getModelValueRepair.
333 std::map
<Node
, std::pair
<Node
, Node
>> d_approximations
;
335 * The witnesses computed during collectModelInfo. For details, see
336 * NlModel::getModelValueRepair.
338 std::map
<Node
, Node
> d_witnesses
;
339 /** have we successfully built the model in this SAT context? */
340 context::CDO
<bool> d_builtModel
;
341 }; /* class NonlinearExtension */
345 } // namespace theory
348 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */