src/theory/arith/nl/cad/cdcac.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__CDCAC_H
  20 #define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
  21
  22 #ifdef CVC5_POLY_IMP
  23
  24 #include <poly/polyxx.h>
  25
  26 #include <vector>
  27
  28 #include "smt/env.h"
  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(Env& env, const std::vector<poly::Variable>& ordering = {});
  52
  53   /** Reset this instance. */
  54   void reset();
  55
  56   /** Collect variables from the constraints and compute a variable ordering. */
  57   void computeVariableOrdering();
  58
  59   /**
  60    * Extract an initial assignment from the given model.
  61    * This initial assignment is used to guide sampling if possible.
  62    * The ran_variable should be the variable used to encode real algebraic
  63    * numbers in the model and is simply passed on to node_to_value.
  64    */
  65   void retrieveInitialAssignment(NlModel& model, const Node& ran_variable);
  66
  67   /**
  68    * Returns the constraints as a non-const reference. Can be used to add new
  69    * constraints.
  70    */
  71   Constraints& getConstraints();
  72   /** Returns the constraints as a const reference. */
  73   const Constraints& getConstraints() const;
  74
  75   /**
  76    * Returns the current assignment. This is a satisfying model if
  77    * get_unsat_cover() returned an empty vector.
  78    */
  79   const poly::Assignment& getModel() const;
  80
  81   /** Returns the current variable ordering. */
  82   const std::vector<poly::Variable>& getVariableOrdering() const;
  83
  84   /**
  85    * Collect all unsatisfiable intervals for the given variable.
  86    * Combines unsatisfiable regions from d_constraints evaluated over
  87    * d_assignment. Implements Algorithm 2.
  88    */
  89   std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable);
  90
  91   /**
  92    * Sample outside of the set of intervals.
  93    * Uses a given initial value from mInitialAssignment if possible.
  94    * Returns whether a sample was found (true) or the infeasible intervals cover
  95    * the whole real line (false).
  96    */
  97   bool sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
  98                                 poly::Value& sample,
  99                                 std::size_t cur_variable);
 100
 101   /**
 102    * Collects the coefficients required for projection from the given
 103    * polynomial. Implements Algorithm 6, depending on the command line
 104    * arguments. Either directly implements Algorithm 6, or improved variants
 105    * based on Lazard's projection.
 106    */
 107   PolyVector requiredCoefficients(const poly::Polynomial& p);
 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   /** A reference to the environment */
 188   Env& d_env;
 189
 190   /**
 191    * The current assignment. When the method terminates with SAT, it contains a
 192    * model for the input constraints.
 193    */
 194   poly::Assignment d_assignment;
 195
 196   /** The set of input constraints to be checked for consistency. */
 197   Constraints d_constraints;
 198
 199   /** The computed variable ordering used for this method. */
 200   std::vector<poly::Variable> d_variableOrdering;
 201
 202   /** The object computing the variable ordering. */
 203   VariableOrdering d_varOrder;
 204
 205   /** The linear assignment used as an initial guess. */
 206   std::vector<poly::Value> d_initialAssignment;
 207
 208   /** The proof generator */
 209   std::unique_ptr<CADProofGenerator> d_proof;
 210 };
 211
 212 }  // namespace cad
 213 }  // namespace nl
 214 }  // namespace arith
 215 }  // namespace theory
 216 }  // namespace cvc5
 217
 218 #endif
 219
 220 #endif