1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Model object for the non-linear extension class
15 #ifndef CVC4__THEORY__ARITH__NL_MODEL_H
16 #define CVC4__THEORY__ARITH__NL_MODEL_H
19 #include <unordered_map>
22 #include "context/cdo.h"
23 #include "context/context.h"
24 #include "expr/kind.h"
25 #include "expr/node.h"
26 #include "theory/theory_model.h"
32 class NonlinearExtension
;
34 /** Non-linear model finder
36 * This class is responsible for all queries related to the (candidate) model
37 * that is being processed by the non-linear arithmetic solver. It further
38 * implements techniques for finding modifications to the current candidate
39 * model in the case it can determine that a model exists. These include
40 * techniques based on solving (quadratic) equations and bound analysis.
44 friend class NonlinearExtension
;
47 NlModel(context::Context
* c
);
51 * This method is called once at the beginning of a last call effort check,
52 * where m is the model of the theory of arithmetic. This method resets the
53 * cache of computed model values.
55 void reset(TheoryModel
* m
, std::map
<Node
, Node
>& arithModel
);
58 * This method is called when the non-linear arithmetic solver restarts
59 * its computation of lemmas and models during a last call effort check.
62 /** compute model value
64 * This computes model values for terms based on two semantics, a "concrete"
65 * semantics and an "abstract" semantics.
67 * if isConcrete is true, this means compute the value of n based on its
68 * children recursively. (we call this its "concrete" value)
69 * if isConcrete is false, this means lookup the value of n in the model.
70 * (we call this its "abstract" value)
71 * In other words, !isConcrete treats multiplication terms and transcendental
72 * function applications as variables, whereas isConcrete computes their
73 * actual values based on the semantics of multiplication. This is a key
74 * distinction used in the model-based refinement scheme in Cimatti et al.
77 * For example, if M( a ) = 2, M( b ) = 3, M( a*b ) = 5, i.e. the variable
78 * for a*b has been assigned a value 5 by the linear solver, then :
80 * computeModelValue( a*b, true ) =
81 * computeModelValue( a, true )*computeModelValue( b, true ) = 2*3 = 6
83 * computeModelValue( a*b, false ) = 5
85 Node
computeConcreteModelValue(Node n
);
86 Node
computeAbstractModelValue(Node n
);
87 Node
computeModelValue(Node n
, bool isConcrete
);
89 /** Compare arithmetic terms i and j based an ordering.
92 * -1 if i < j, 1 if i > j, or 0 if i == j
94 * If isConcrete is true, we consider the concrete model values of i and j,
95 * otherwise, we consider their abstract model values. For definitions of
96 * concrete vs abstract model values, see NlModel::computeModelValue.
98 * If isAbsolute is true, we compare the absolute value of thee above
101 int compare(Node i
, Node j
, bool isConcrete
, bool isAbsolute
);
102 /** Compare arithmetic terms i and j based an ordering.
105 * -1 if i < j, 1 if i > j, or 0 if i == j
107 * If isAbsolute is true, we compare the absolute value of i and j
109 int compareValue(Node i
, Node j
, bool isAbsolute
) const;
111 //------------------------------ recording model substitutions and bounds
112 /** add check model substitution
114 * Adds the model substitution v -> s. This applies the substitution
115 * { v -> s } to each term in d_check_model_subs and adds v,s to
116 * d_check_model_vars and d_check_model_subs respectively.
117 * If this method returns false, then the substitution v -> s is inconsistent
118 * with the current substitution and bounds.
120 bool addCheckModelSubstitution(TNode v
, TNode s
);
121 /** add check model bound
123 * Adds the bound x -> < l, u > to the map above, and records the
124 * approximation ( x, l <= x <= u ) in the model. This method returns false
125 * if the bound is inconsistent with the current model substitution or
128 bool addCheckModelBound(TNode v
, TNode l
, TNode u
);
129 /** has check model assignment
131 * Have we assigned v in the current checkModel(...) call?
133 * This method returns true if variable v is in the domain of
134 * d_check_model_bounds or if it occurs in d_check_model_vars.
136 bool hasCheckModelAssignment(Node v
) const;
139 * Checks the current model based on solving for equalities, and using error
140 * bounds on the Taylor approximation.
142 * If this function returns true, then all assertions in the input argument
143 * "assertions" are satisfied for all interpretations of variables within
144 * their computed bounds (as stored in d_check_model_bounds).
146 * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
147 * "Detecting Satisfiable Formulas".
149 * d is a degree indicating how precise our computations are.
151 bool checkModel(const std::vector
<Node
>& assertions
,
152 const std::vector
<Node
>& false_asserts
,
154 std::vector
<Node
>& lemmas
,
155 std::vector
<Node
>& gs
);
157 * Set that we have used an approximation during this check. This flag is
158 * reset on a call to resetCheck. It is set when we use reasoning that
159 * is limited by a degree of precision we are using. In other words, if we
160 * used an approximation, then we maybe could still establish a lemma or
161 * determine the input is SAT if we increased our precision.
163 void setUsedApproximate();
164 /** Did we use an approximation during this check? */
165 bool usedApproximate() const;
168 * This states that formula n is a tautology (satisfied in all models).
169 * We call this on internally generated lemmas. This method computes a
170 * set of literals that are implied by n, that are hence tautological
172 * l_pi <= real.pi <= u_pi (pi approximations)
173 * sin(x) = -1*sin(-x)
174 * where these literals are internally generated for the purposes
175 * of guiding the models of the linear solver.
177 * TODO (cvc4-projects #113: would be helpful if we could do this even
178 * more aggressively by ignoring all internally generated literals.
180 * Tautological literals do not need be checked during checkModel.
182 void addTautology(Node n
);
183 //------------------------------ end recording model substitutions and bounds
185 /** print model value, for debugging.
187 * This prints both the abstract and concrete model values for arithmetic
188 * term n on Trace c with precision prec.
190 void printModelValue(const char* c
, Node n
, unsigned prec
= 5) const;
191 /** get model value repair
193 * This gets mappings that indicate how to repair the model generated by the
194 * linear arithmetic solver. This method should be called after a successful
195 * call to checkModel above.
197 * The mapping arithModel is updated by this method to map arithmetic terms v
198 * to their (exact) value that was computed during checkModel; the mapping
199 * approximations is updated to store approximate values in the form of a
200 * pair (P, w), where P is a predicate that describes the possible values of
201 * v and w is a witness point that satisfies this predicate.
203 void getModelValueRepair(
204 std::map
<Node
, Node
>& arithModel
,
205 std::map
<Node
, std::pair
<Node
, Node
>>& approximations
);
208 /** The current model */
209 TheoryModel
* d_model
;
210 /** Get the model value of n from the model object above */
211 Node
getValueInternal(Node n
) const;
212 /** Does the equality engine of the model have term n? */
213 bool hasTerm(Node n
) const;
214 /** Get the representative of n in the model */
215 Node
getRepresentative(Node n
) const;
217 //---------------------------check model
218 /** solve equality simple
220 * This method is used during checkModel(...). It takes as input an
221 * equality eq. If it returns true, then eq is correct-by-construction based
222 * on the information stored in our model representation (see
223 * d_check_model_vars, d_check_model_subs, d_check_model_bounds), and eq
224 * is added to d_check_model_solved. The equality eq may involve any
225 * number of variables, and monomials of arbitrary degree. If this method
226 * returns false, then we did not show that the equality was true in the
227 * model. This method uses incomplete techniques based on interval
228 * analysis and quadratic equation solving.
230 * If it can be shown that the equality must be false in the current
231 * model, then we may add a lemma to lemmas explaining why this is the case.
232 * For instance, if eq reduces to a univariate quadratic equation with no
233 * root, we send a conflict clause of the form a*x^2 + b*x + c != 0.
235 bool solveEqualitySimple(Node eq
, unsigned d
, std::vector
<Node
>& lemmas
);
237 /** simple check model for transcendental functions for literal
239 * This method returns true if literal is true for all interpretations of
240 * transcendental functions within their error bounds (as stored
241 * in d_check_model_bounds). This is determined by a simple under/over
242 * approximation of the value of sum of (linear) monomials. For example,
243 * if we determine that .8 < sin( 1 ) < .9, this function will return
244 * true for literals like:
246 * -1.0*sin( 1 ) < -0.79
247 * -1.0*sin( 1 ) > -0.91
248 * sin( 1 )*sin( 1 ) + sin( 1 ) > 0.0
249 * It will return false for literals like:
251 * It will also return false for literals like:
252 * -0.3*sin( 1 )*sin( 2 ) + sin( 2 ) > .7
253 * sin( sin( 1 ) ) > .5
254 * since the bounds on these terms cannot quickly be determined.
256 bool simpleCheckModelLit(Node lit
);
257 bool simpleCheckModelMsum(const std::map
<Node
, Node
>& msum
, bool pol
);
258 //---------------------------end check model
260 /** is refinable transcendental function
262 * A transcendental function application is not refineable if its current
263 * model value is zero, or if it is an application of SINE applied
266 bool isRefineableTfFun(Node tf
);
268 /** get approximate sqrt
270 * This approximates the square root of positive constant c. If this method
271 * returns true, then l and u are updated to constants such that
272 * l <= sqrt( c ) <= u
273 * The argument iter is the number of iterations in the binary search to
274 * perform. By default, this is set to 15, which is usually enough to be
275 * precise in the majority of simple cases, whereas not prohibitively
276 * expensive to compute.
278 bool getApproximateSqrt(Node c
, Node
& l
, Node
& u
, unsigned iter
= 15) const;
280 /** commonly used terms */
288 * The values that the arithmetic theory solver assigned in the model. This
289 * corresponds to exactly the set of equalities that TheoryArith is currently
290 * sending to TheoryModel during collectModelInfo.
292 std::map
<Node
, Node
> d_arithVal
;
293 /** cache of model values
295 * Stores the the concrete/abstract model values. This is a cache of the
296 * computeModelValue method.
298 std::map
<Node
, Node
> d_mv
[2];
300 * A substitution from variables that appear in assertions to a solved form
301 * term. These vectors are ordered in the form:
302 * x_1 -> t_1 ... x_n -> t_n
303 * where x_i is not in the free variables of t_j for j>=i.
305 std::vector
<Node
> d_check_model_vars
;
306 std::vector
<Node
> d_check_model_subs
;
307 /** lower and upper bounds for check model
309 * For each term t in the domain of this map, if this stores the pair
310 * (c_l, c_u) then the model M is such that c_l <= M( t ) <= c_u.
312 * We add terms whose value is approximated in the model to this map, which
314 * (1) applications of transcendental functions, whose value is approximated
315 * by the Taylor series,
316 * (2) variables we have solved quadratic equations for, whose value
317 * involves approximations of square roots.
319 std::map
<Node
, std::pair
<Node
, Node
> > d_check_model_bounds
;
321 * The map from literals that our model construction solved, to the variable
322 * that was solved for. Examples of such literals are:
323 * (1) Equalities x = t, which we turned into a model substitution x -> t,
324 * where x not in FV( t ), and
325 * (2) Equalities a*x*x + b*x + c = 0, which we turned into a model bound
326 * -b+s*sqrt(b*b-4*a*c)/2a - E <= x <= -b+s*sqrt(b*b-4*a*c)/2a + E.
328 * These literals are exempt from check-model, since they are satisfied by
329 * definition of our model construction.
331 std::unordered_map
<Node
, Node
, NodeHashFunction
> d_check_model_solved
;
332 /** did we use an approximation on this call to last-call effort? */
334 /** the set of all tautological literals */
335 std::unordered_set
<Node
, NodeHashFunction
> d_tautology
;
336 }; /* class NlModel */
339 } // namespace theory
342 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */