src/theory/arith/nl/cad_solver.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  * CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf.
  14  */
  15
  16 #ifndef CVC5__THEORY__ARITH__CAD_SOLVER_H
  17 #define CVC5__THEORY__ARITH__CAD_SOLVER_H
  18
  19 #include <vector>
  20
  21 #include "context/context.h"
  22 #include "expr/node.h"
  23 #include "theory/arith/nl/cad/cdcac.h"
  24 #include "theory/arith/nl/cad/proof_checker.h"
  25
  26 namespace cvc5 {
  27
  28 class ProofNodeManager;
  29
  30 namespace theory {
  31 namespace arith {
  32
  33 class InferenceManager;
  34
  35 namespace nl {
  36
  37 class NlModel;
  38
  39 /**
  40  * A solver for nonlinear arithmetic that implements the CAD-based method
  41  * described in https://arxiv.org/pdf/2003.05633.pdf.
  42  */
  43 class CadSolver
  44 {
  45  public:
  46   CadSolver(Env& env, InferenceManager& im, NlModel& model);
  47   ~CadSolver();
  48
  49   /**
  50    * This is called at the beginning of last call effort check, where
  51    * assertions are the set of assertions belonging to arithmetic,
  52    * false_asserts is the subset of assertions that are false in the current
  53    * model, and xts is the set of extended function terms that are active in
  54    * the current context.
  55    */
  56   void initLastCall(const std::vector<Node>& assertions);
  57
  58   /**
  59    * Perform a full check, returning either {} or a single lemma.
  60    * If the result is empty, the input is satisfiable and a model is available
  61    * for construct_model_if_available. Otherwise, the single lemma can be used
  62    * as an infeasible subset.
  63    */
  64   void checkFull();
  65
  66   /**
  67    * Perform a partial check, returning either {} or a list of lemmas.
  68    * If the result is empty, the input is satisfiable and a model is available
  69    * for construct_model_if_available. Otherwise, the lemmas exclude some part
  70    * of the search space.
  71    */
  72   void checkPartial();
  73
  74   /**
  75    * If a model is available (indicated by the last call to check_full() or
  76    * check_partial()) this method puts a satisfying assignment in d_model,
  77    * clears the list of assertions, and returns true.
  78    * Otherwise, this method returns false.
  79    */
  80   bool constructModelIfAvailable(std::vector<Node>& assertions);
  81
  82  private:
  83   /**
  84    * The variable used to encode real algebraic numbers to nodes.
  85    */
  86   Node d_ranVariable;
  87
  88 #ifdef CVC5_POLY_IMP
  89   /**
  90    * The object implementing the actual decision procedure.
  91    */
  92   cad::CDCAC d_CAC;
  93   /** The proof checker for cad proofs */
  94   cad::CADProofRuleChecker d_proofChecker;
  95 #endif
  96   /**
  97    * Indicates whether we found satisfiability in the last call to
  98    * checkFullRefine.
  99    */
 100   bool d_foundSatisfiability;
 101
 102   /** The inference manager we are pushing conflicts and lemmas to. */
 103   InferenceManager& d_im;
 104   /** Reference to the non-linear model object */
 105   NlModel& d_model;
 106 }; /* class CadSolver */
 107
 108 }  // namespace nl
 109 }  // namespace arith
 110 }  // namespace theory
 111 }  // namespace cvc5
 112
 113 #endif /* CVC5__THEORY__ARITH__CAD_SOLVER_H */