src/theory/arith/nl/cad/lazard_evaluation.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Implements the CDCAC approach as described in
  14  * https://arxiv.org/pdf/2003.05633.pdf.
  15  */
  16
  17 #include "cvc5_private.h"
  18
  19 #ifndef CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H
  20 #define CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H
  21
  22 #ifdef CVC5_POLY_IMP
  23
  24 #include <poly/polyxx.h>
  25
  26 #include <memory>
  27
  28 namespace cvc5::theory::arith::nl::cad {
  29
  30 struct LazardEvaluationState;
  31 /**
  32  * This class does the heavy lifting for the modified lifting procedure that is
  33  * required for Lazard's projection.
  34  *
  35  * Let p \in Q[x_0, ..., x_n] a multivariate polynomial whose roots we want to
  36  * isolate over the partial sample point A = [x_0 = a_0, ... x_{n-1} = a_{n-1}]
  37  * where a_0, ... a_{n-1} are real algebraic numbers and x_n is the last free
  38  * variable.
  39  *
  40  * The modified lifting procedure conceptually works as follows:
  41  *
  42  * for (x = a) in A:
  43  *    while p[x // a] = 0:
  44  *       p = p / (x - a)
  45  *    p = p[x // a]
  46  * return roots(p)
  47  *
  48  * As the assignment contains real algebraic numbers, though, we can not do any
  49  * of the computations directly, as our polynomials only support coefficients
  50  * from Z or Q, but not extensions (in the algebraic sense) thereof.
  51  *
  52  * Our approach is as follows:
  53  * Let pk be the minimal polynomial for a_k.
  54  * Instead of substituting p[x_k // a_k] we (canonically) embed p into the
  55  * quotient ring Q[x_k]/<p_k> and recursively build a tower of such quotient
  56  * rings that is isomorphic to nesting the corresponding field extensions
  57  * Q(a_1)(a_2)... When we have done that, we obtain p that is reduced with
  58  * respect to all minimal polynomials, but may still contain x_0,... x_{n-1}. To
  59  * get rid of these, we compute a Gröbner basis of p and the minimal polynomials
  60  * (using a suitable elimination order) and extract the polynomial in x_n. This
  61  * polynomial has all roots (and possibly some more) that we are looking for.
  62  * Instead of a Gröbner basis, we can also compute the iterated resultant as
  63  * follows: Res(Res(p, p_{n-1}, x_{n-1}), p_{n-2}, x_{n-2})...
  64  *
  65  * Consider
  66  * http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2020/2020-04.pdf
  67  * Section 2.5.1 for a full discussion.
  68  *
  69  * !!! WARNING !!!
  70  * If CoCoALib is not available, this class will simply fall back to
  71  * poly::infeasible_regions and issue a warning about this.
  72  */
  73 class LazardEvaluation
  74 {
  75  public:
  76   LazardEvaluation();
  77   ~LazardEvaluation();
  78
  79   /**
  80    * Add the next assigned variable x_k = a_k to this construction.
  81    */
  82   void add(const poly::Variable& var, const poly::Value& val);
  83   /**
  84    * Finish by adding the free variable x_n.
  85    */
  86   void addFreeVariable(const poly::Variable& var);
  87   /**
  88    * Reduce the polynomial q. Compared to the above description, there may
  89    * actually be multiple polynomials in the Gröbner basis and instead of
  90    * loosing this knowledge and returning their product, we return them as a
  91    * vector.
  92    */
  93   std::vector<poly::Polynomial> reducePolynomial(
  94       const poly::Polynomial& q) const;
  95
  96   /**
  97    * Compute the infeasible regions of q under the given sign condition.
  98    * Uses reducePolynomial and then performs real root isolation on the
  99    * resulting polynomials to obtain the intervals. Mimics
 100    * poly::infeasible_regions, but uses Lazard's evaluation.
 101    */
 102   std::vector<poly::Interval> infeasibleRegions(const poly::Polynomial& q,
 103                                                 poly::SignCondition sc) const;
 104
 105  private:
 106   std::unique_ptr<LazardEvaluationState> d_state;
 107 };
 108
 109 }  // namespace cvc5::theory::arith::nl::cad
 110
 111 #endif
 112 #endif