src/theory/arith/nl/transcendental/exponential_solver.h

   1 /*********************                                                        */
   2 /*! \file exponential_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King
   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
  11  **
  12  ** \brief Solving for handling exponential function.
  13  **/
  14
  15 #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
  16 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
  17
  18 #include <map>
  19 #include <unordered_map>
  20 #include <unordered_set>
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "theory/arith/inference_manager.h"
  25 #include "theory/arith/nl/nl_model.h"
  26 #include "theory/arith/nl/transcendental/transcendental_state.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace arith {
  31 namespace nl {
  32 namespace transcendental {
  33
  34 /** Transcendental solver class
  35  *
  36  * This class implements model-based refinement schemes
  37  * for transcendental functions, described in:
  38  *
  39  * - "Satisfiability Modulo Transcendental
  40  * Functions via Incremental Linearization" by Cimatti
  41  * et al., CADE 2017.
  42  *
  43  * It's main functionality are methods that implement lemma schemas below,
  44  * which return a set of lemmas that should be sent on the output channel.
  45  */
  46 class ExponentialSolver
  47 {
  48  public:
  49   ExponentialSolver(TranscendentalState* tstate);
  50   ~ExponentialSolver();
  51
  52   void initLastCall(const std::vector<Node>& assertions,
  53                     const std::vector<Node>& false_asserts,
  54                     const std::vector<Node>& xts);
  55
  56   /**
  57    * check initial refine
  58    *
  59    * Constructs a set of valid theory lemmas, based on
  60    * simple facts about the exponential function.
  61    * This mostly follows the initial axioms described in
  62    * Section 4 of "Satisfiability
  63    * Modulo Transcendental Functions via Incremental
  64    * Linearization" by Cimatti et al., CADE 2017.
  65    *
  66    * Examples:
  67    *
  68    * exp( x )>0
  69    * x<0 => exp( x )<1
  70    */
  71   void checkInitialRefine();
  72
  73   /**
  74    * check monotonicity
  75    *
  76    * Constructs a set of valid theory lemmas, based on a
  77    * lemma scheme that ensures that applications
  78    * of the exponential function respect monotonicity.
  79    *
  80    * Examples:
  81    *
  82    * x > y => exp( x ) > exp( y )
  83    */
  84   void checkMonotonic();
  85
  86   /** Sent tangent lemma around c for e */
  87   void doTangentLemma(TNode e, TNode c, TNode poly_approx);
  88
  89   /** Sent secant lemmas around c for e */
  90   void doSecantLemmas(TNode e, TNode c, TNode poly_approx, unsigned d);
  91
  92  private:
  93   /** Generate bounds for secant lemmas */
  94   std::pair<Node, Node> getSecantBounds(TNode e, TNode c, unsigned d);
  95
  96   /** Holds common state for transcendental solvers */
  97   TranscendentalState* d_data;
  98
  99   /** The transcendental functions we have done initial refinements on */
 100   std::map<Node, bool> d_tf_initial_refine;
 101
 102 }; /* class ExponentialSolver */
 103
 104 }  // namespace transcendental
 105 }  // namespace nl
 106 }  // namespace arith
 107 }  // namespace theory
 108 }  // namespace CVC4
 109
 110 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */