src/theory/arith/nl_model.h

   1 /*********************                                                        */
   2 /*! \file nl_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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
  11  **
  12  ** \brief Model object for the non-linear extension class
  13  **/
  14
  15 #ifndef CVC4__THEORY__ARITH__NL_MODEL_H
  16 #define CVC4__THEORY__ARITH__NL_MODEL_H
  17
  18 #include <map>
  19 #include <unordered_map>
  20 #include <vector>
  21
  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"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace arith {
  31
  32 class NonlinearExtension;
  33
  34 /** Non-linear model finder
  35  *
  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.
  41  */
  42 class NlModel
  43 {
  44   friend class NonlinearExtension;
  45
  46  public:
  47   NlModel(context::Context* c);
  48   ~NlModel();
  49   /** reset
  50    *
  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.
  54    */
  55   void reset(TheoryModel* m, std::map<Node, Node>& arithModel);
  56   /** reset check
  57    *
  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.
  60    */
  61   void resetCheck();
  62   /** compute model value
  63    *
  64    * This computes model values for terms based on two semantics, a "concrete"
  65    * semantics and an "abstract" semantics.
  66    *
  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.
  75    * TACAS 2017.
  76    *
  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 :
  79    *
  80    *   computeModelValue( a*b, true ) =
  81    *   computeModelValue( a, true )*computeModelValue( b, true ) = 2*3 = 6
  82    * whereas:
  83    *   computeModelValue( a*b, false ) = 5
  84    */
  85   Node computeConcreteModelValue(Node n);
  86   Node computeAbstractModelValue(Node n);
  87   Node computeModelValue(Node n, bool isConcrete);
  88
  89   /** Compare arithmetic terms i and j based an ordering.
  90    *
  91    * This returns:
  92    *  -1 if i < j, 1 if i > j, or 0 if i == j
  93    *
  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.
  97    *
  98    * If isAbsolute is true, we compare the absolute value of thee above
  99    * values.
 100    */
 101   int compare(Node i, Node j, bool isConcrete, bool isAbsolute);
 102   /** Compare arithmetic terms i and j based an ordering.
 103    *
 104    * This returns:
 105    *  -1 if i < j, 1 if i > j, or 0 if i == j
 106    *
 107    * If isAbsolute is true, we compare the absolute value of i and j
 108    */
 109   int compareValue(Node i, Node j, bool isAbsolute) const;
 110
 111   //------------------------------ recording model substitutions and bounds
 112   /** add check model substitution
 113    *
 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.
 119    */
 120   bool addCheckModelSubstitution(TNode v, TNode s);
 121   /** add check model bound
 122    *
 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
 126    * bounds.
 127    */
 128   bool addCheckModelBound(TNode v, TNode l, TNode u);
 129   /** has check model assignment
 130    *
 131    * Have we assigned v in the current checkModel(...) call?
 132    *
 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.
 135    */
 136   bool hasCheckModelAssignment(Node v) const;
 137   /** Check model
 138    *
 139    * Checks the current model based on solving for equalities, and using error
 140    * bounds on the Taylor approximation.
 141    *
 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).
 145    *
 146    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
 147    * "Detecting Satisfiable Formulas".
 148    *
 149    * d is a degree indicating how precise our computations are.
 150    */
 151   bool checkModel(const std::vector<Node>& assertions,
 152                   const std::vector<Node>& false_asserts,
 153                   unsigned d,
 154                   std::vector<Node>& lemmas,
 155                   std::vector<Node>& gs);
 156   /**
 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.
 162    */
 163   void setUsedApproximate();
 164   /** Did we use an approximation during this check? */
 165   bool usedApproximate() const;
 166   /** Set tautology
 167    *
 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
 171    * as well, such as:
 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.
 176    *
 177    * TODO (cvc4-projects #113: would be helpful if we could do this even
 178    * more aggressively by ignoring all internally generated literals.
 179    *
 180    * Tautological literals do not need be checked during checkModel.
 181    */
 182   void addTautology(Node n);
 183   //------------------------------ end recording model substitutions and bounds
 184
 185   /** print model value, for debugging.
 186    *
 187    * This prints both the abstract and concrete model values for arithmetic
 188    * term n on Trace c with precision prec.
 189    */
 190   void printModelValue(const char* c, Node n, unsigned prec = 5) const;
 191   /** get model value repair
 192    *
 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.
 196    *
 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.
 202    */
 203   void getModelValueRepair(
 204       std::map<Node, Node>& arithModel,
 205       std::map<Node, std::pair<Node, Node>>& approximations);
 206
 207  private:
 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;
 216
 217   //---------------------------check model
 218   /** solve equality simple
 219    *
 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.
 229    *
 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.
 234    */
 235   bool solveEqualitySimple(Node eq, unsigned d, std::vector<Node>& lemmas);
 236
 237   /** simple check model for transcendental functions for literal
 238    *
 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:
 245    *   2.0*sin( 1 ) > 1.5
 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:
 250    *   sin( 1 ) > 0.85
 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.
 255    */
 256   bool simpleCheckModelLit(Node lit);
 257   bool simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol);
 258   //---------------------------end check model
 259
 260   /** is refinable transcendental function
 261    *
 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
 264    * to a non-variable.
 265    */
 266   bool isRefineableTfFun(Node tf);
 267
 268   /** get approximate sqrt
 269    *
 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.
 277    */
 278   bool getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter = 15) const;
 279
 280   /** commonly used terms */
 281   Node d_zero;
 282   Node d_one;
 283   Node d_two;
 284   Node d_true;
 285   Node d_false;
 286   Node d_null;
 287   /**
 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.
 291    */
 292   std::map<Node, Node> d_arithVal;
 293   /** cache of model values
 294    *
 295    * Stores the the concrete/abstract model values. This is a cache of the
 296    * computeModelValue method.
 297    */
 298   std::map<Node, Node> d_mv[2];
 299   /**
 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.
 304    */
 305   std::vector<Node> d_check_model_vars;
 306   std::vector<Node> d_check_model_subs;
 307   /** lower and upper bounds for check model
 308    *
 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.
 311    *
 312    * We add terms whose value is approximated in the model to this map, which
 313    * includes:
 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.
 318    */
 319   std::map<Node, std::pair<Node, Node> > d_check_model_bounds;
 320   /**
 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.
 327    *
 328    * These literals are exempt from check-model, since they are satisfied by
 329    * definition of our model construction.
 330    */
 331   std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
 332   /** did we use an approximation on this call to last-call effort? */
 333   bool d_used_approx;
 334   /** the set of all tautological literals */
 335   std::unordered_set<Node, NodeHashFunction> d_tautology;
 336 }; /* class NlModel */
 337
 338 }  // namespace arith
 339 }  // namespace theory
 340 }  // namespace CVC4
 341
 342 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */