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

   1 /*********************                                                        */
   2 /*! \file cdcac.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Gereon Kremer
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** \brief Implements the CDCAC approach.
  13  **
  14  ** Implements the CDCAC approach as described in
  15  ** https://arxiv.org/pdf/2003.05633.pdf.
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
  21 #define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
  22
  23 #ifdef CVC4_POLY_IMP
  24
  25 #include <poly/polyxx.h>
  26
  27 #include <vector>
  28
  29 #include "theory/arith/nl/cad/cdcac_utils.h"
  30 #include "theory/arith/nl/cad/constraints.h"
  31 #include "theory/arith/nl/cad/proof_generator.h"
  32 #include "theory/arith/nl/cad/variable_ordering.h"
  33
  34 namespace cvc5 {
  35 namespace theory {
  36 namespace arith {
  37 namespace nl {
  38
  39 class NlModel;
  40
  41 namespace cad {
  42
  43 /**
  44  * This class implements Cylindrical Algebraic Coverings as presented in
  45  * https://arxiv.org/pdf/2003.05633.pdf
  46  */
  47 class CDCAC
  48 {
  49  public:
  50   /** Initialize this method with the given variable ordering. */
  51   CDCAC(context::Context* ctx,
  52         ProofNodeManager* pnm,
  53         const std::vector<poly::Variable>& ordering = {});
  54
  55   /** Reset this instance. */
  56   void reset();
  57
  58   /** Collect variables from the constraints and compute a variable ordering. */
  59   void computeVariableOrdering();
  60
  61   /**
  62    * Extract an initial assignment from the given model.
  63    * This initial assignment is used to guide sampling if possible.
  64    * The ran_variable should be the variable used to encode real algebraic
  65    * numbers in the model and is simply passed on to node_to_value.
  66    */
  67   void retrieveInitialAssignment(NlModel& model, const Node& ran_variable);
  68
  69   /**
  70    * Returns the constraints as a non-const reference. Can be used to add new
  71    * constraints.
  72    */
  73   Constraints& getConstraints();
  74   /** Returns the constraints as a const reference. */
  75   const Constraints& getConstraints() const;
  76
  77   /**
  78    * Returns the current assignment. This is a satisfying model if
  79    * get_unsat_cover() returned an empty vector.
  80    */
  81   const poly::Assignment& getModel() const;
  82
  83   /** Returns the current variable ordering. */
  84   const std::vector<poly::Variable>& getVariableOrdering() const;
  85
  86   /**
  87    * Collect all unsatisfiable intervals for the given variable.
  88    * Combines unsatisfiable regions from d_constraints evaluated over
  89    * d_assignment. Implements Algorithm 2.
  90    */
  91   std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable);
  92
  93   /**
  94    * Sample outside of the set of intervals.
  95    * Uses a given initial value from mInitialAssignment if possible.
  96    * Returns whether a sample was found (true) or the infeasible intervals cover
  97    * the whole real line (false).
  98    */
  99   bool sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
 100                                 poly::Value& sample,
 101                                 std::size_t cur_variable);
 102
 103   /**
 104    * Collects the coefficients required for projection from the given
 105    * polynomial. Implements Algorithm 6.
 106    */
 107   PolyVector requiredCoefficients(const poly::Polynomial& p) const;
 108
 109   /**
 110    * Constructs a characterization of the given covering.
 111    * A characterization contains polynomials whose roots bound the region around
 112    * the current assignment. Implements Algorithm 4.
 113    */
 114   PolyVector constructCharacterization(std::vector<CACInterval>& intervals);
 115
 116   /**
 117    * Constructs an infeasible interval from a characterization.
 118    * Implements Algorithm 5.
 119    */
 120   CACInterval intervalFromCharacterization(const PolyVector& characterization,
 121                                            std::size_t cur_variable,
 122                                            const poly::Value& sample);
 123
 124   /**
 125    * Main method that checks for the satisfiability of the constraints.
 126    * Recursively explores possible assignments and excludes regions based on the
 127    * coverings. Returns either a covering for the lowest dimension or an empty
 128    * vector. If the covering is empty, the result is SAT and an assignment can
 129    * be obtained from d_assignment. If the covering is not empty, the result is
 130    * UNSAT and an infeasible subset can be extracted from the returned covering.
 131    * Implements Algorithm 2.
 132    * @param curVariable The id of the variable (within d_variableOrdering) to
 133    * be considered. This argument is used to manage the recursion internally and
 134    * should always be zero if called externally.
 135    * @param returnFirstInterval If true, the function returns after the first
 136    * interval obtained from a recursive call. The result is not (necessarily) an
 137    * unsat cover, but merely a list of infeasible intervals.
 138    */
 139   std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
 140                                          bool returnFirstInterval = false);
 141
 142   void startNewProof();
 143   /**
 144    * Finish the generated proof (if proofs are enabled) with a scope over the
 145    * given assertions.
 146    */
 147   ProofGenerator* closeProof(const std::vector<Node>& assertions);
 148
 149   /** Get the proof generator */
 150   CADProofGenerator* getProof() { return d_proof.get(); }
 151
 152  private:
 153   /** Check whether proofs are enabled */
 154   bool isProofEnabled() const { return d_proof != nullptr; }
 155
 156   /**
 157    * Check whether the current sample satisfies the integrality condition of the
 158    * current variable. Returns true if the variable is not integral or the
 159    * sample is integral.
 160    */
 161   bool checkIntegrality(std::size_t cur_variable, const poly::Value& value);
 162   /**
 163    * Constructs an interval that excludes the non-integral region around the
 164    * current sample. Assumes !check_integrality(cur_variable, value).
 165    */
 166   CACInterval buildIntegralityInterval(std::size_t cur_variable,
 167                                        const poly::Value& value);
 168
 169   /**
 170    * Check whether the polynomial has a real root above the given value (when
 171    * evaluated over the current assignment).
 172    */
 173   bool hasRootAbove(const poly::Polynomial& p, const poly::Value& val) const;
 174   /**
 175    * Check whether the polynomial has a real root below the given value (when
 176    * evaluated over the current assignment).
 177    */
 178   bool hasRootBelow(const poly::Polynomial& p, const poly::Value& val) const;
 179
 180   /**
 181    * Sort intervals according to section 4.4.1. and removes fully redundant
 182    * intervals as in 4.5. 1. by calling out to cleanIntervals.
 183    * Additionally makes sure to prune proofs for removed intervals.
 184    */
 185   void pruneRedundantIntervals(std::vector<CACInterval>& intervals);
 186
 187   /**
 188    * The current assignment. When the method terminates with SAT, it contains a
 189    * model for the input constraints.
 190    */
 191   poly::Assignment d_assignment;
 192
 193   /** The set of input constraints to be checked for consistency. */
 194   Constraints d_constraints;
 195
 196   /** The computed variable ordering used for this method. */
 197   std::vector<poly::Variable> d_variableOrdering;
 198
 199   /** The object computing the variable ordering. */
 200   VariableOrdering d_varOrder;
 201
 202   /** The linear assignment used as an initial guess. */
 203   std::vector<poly::Value> d_initialAssignment;
 204
 205   /** The proof generator */
 206   std::unique_ptr<CADProofGenerator> d_proof;
 207 };
 208
 209 }  // namespace cad
 210 }  // namespace nl
 211 }  // namespace arith
 212 }  // namespace theory
 213 }  // namespace cvc5
 214
 215 #endif
 216
 217 #endif