src/theory/arith/nl/nonlinear_extension.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Tim King
   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  * Extensions to the theory of arithmetic incomplete handling of nonlinear
  14  * multiplication via axiom instantiations.
  15  */
  16
  17 #ifndef CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
  18 #define CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "theory/arith/nl/cad_solver.h"
  25 #include "theory/arith/nl/ext/ext_state.h"
  26 #include "theory/arith/nl/ext/factoring_check.h"
  27 #include "theory/arith/nl/ext/monomial_bounds_check.h"
  28 #include "theory/arith/nl/ext/monomial_check.h"
  29 #include "theory/arith/nl/ext/proof_checker.h"
  30 #include "theory/arith/nl/ext/split_zero_check.h"
  31 #include "theory/arith/nl/ext/tangent_plane_check.h"
  32 #include "theory/arith/nl/ext_theory_callback.h"
  33 #include "theory/arith/nl/iand_solver.h"
  34 #include "theory/arith/nl/icp/icp_solver.h"
  35 #include "theory/arith/nl/nl_model.h"
  36 #include "theory/arith/nl/stats.h"
  37 #include "theory/arith/nl/strategy.h"
  38 #include "theory/arith/nl/transcendental/transcendental_solver.h"
  39 #include "theory/ext_theory.h"
  40 #include "theory/theory.h"
  41 #include "util/result.h"
  42
  43 namespace cvc5 {
  44 namespace theory {
  45 namespace eq {
  46   class EqualityEngine;
  47 }
  48 namespace arith {
  49
  50 class InferenceManager;
  51 class TheoryArith;
  52
  53 namespace nl {
  54
  55 class NlLemma;
  56
  57 /** Non-linear extension class
  58  *
  59  * This class implements model-based refinement schemes
  60  * for non-linear arithmetic, described in:
  61  *
  62  * - "Invariant Checking of NRA Transition Systems
  63  * via Incremental Reduction to LRA with EUF" by
  64  * Cimatti et al., TACAS 2017.
  65  *
  66  * - Section 5 of "Desiging Theory Solvers with
  67  * Extensions" by Reynolds et al., FroCoS 2017.
  68  *
  69  * - "Satisfiability Modulo Transcendental
  70  * Functions via Incremental Linearization" by Cimatti
  71  * et al., CADE 2017.
  72  *
  73  * It's main functionality is a check(...) method,
  74  * which is called by TheoryArithPrivate either:
  75  * (1) at full effort with no conflicts or lemmas emitted, or
  76  * (2) at last call effort.
  77  * In this method, this class calls d_im.lemma(...)
  78  * for valid arithmetic theory lemmas, based on the current set of assertions,
  79  * where d_im is the inference manager of TheoryArith.
  80  */
  81 class NonlinearExtension
  82 {
  83   typedef context::CDHashSet<Node> NodeSet;
  84
  85  public:
  86   NonlinearExtension(TheoryArith& containing,
  87                      ArithState& state,
  88                      eq::EqualityEngine* ee,
  89                      ProofNodeManager* pnm);
  90   ~NonlinearExtension();
  91   /**
  92    * Does non-context dependent setup for a node connected to a theory.
  93    */
  94   void preRegisterTerm(TNode n);
  95   /** Check at effort level e.
  96    *
  97    * This call may result in (possibly multiple) calls to d_im.lemma(...)
  98    * where d_im is the inference manager of TheoryArith.
  99    *
 100    * If e is FULL, then we add lemmas based on context-depedent
 101    * simplification (see Reynolds et al FroCoS 2017).
 102    *
 103    * If e is LAST_CALL, we add lemmas based on model-based refinement
 104    * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this
 105    * effort may be computed during a call to interceptModel as described below.
 106    */
 107   void check(Theory::Effort e);
 108   /** intercept model
 109    *
 110    * This method is called during TheoryArith::collectModelInfo, which is
 111    * invoked after the linear arithmetic solver passes a full effort check
 112    * with no lemmas.
 113    *
 114    * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
 115    * which represents the linear arithmetic theory solver's contribution to the
 116    * current candidate model. That is, its collectModelInfo method is requesting
 117    * that equalities v1 = c1, ..., vn = cn be added to the current model, where
 118    * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice
 119    * arithmetic variables may be real-valued terms belonging to other theories,
 120    * or abstractions of applications of multiplication (kind NONLINEAR_MULT).
 121    *
 122    * This method requests that the non-linear solver inspect this model and
 123    * do any number of the following:
 124    * (1) Construct lemmas based on a model-based refinement procedure inspired
 125    * by Cimatti et al., TACAS 2017.,
 126    * (2) In the case that the nonlinear solver finds that the current
 127    * constraints are satisfiable, it may "repair" the values in the argument
 128    * arithModel so that it satisfies certain nonlinear constraints. This may
 129    * involve e.g. solving for variables in nonlinear equations.
 130    */
 131   void interceptModel(std::map<Node, Node>& arithModel,
 132                       const std::set<Node>& termSet);
 133   /** Does this class need a call to check(...) at last call effort? */
 134   bool needsCheckLastEffort() const { return d_needsLastCall; }
 135   /** presolve
 136    *
 137    * This function is called during TheoryArith's presolve command.
 138    * In this function, we send lemmas we accumulated during preprocessing,
 139    * for instance, definitional lemmas from expandDefinitions are sent out
 140    * on the output channel of TheoryArith in this function.
 141    */
 142   void presolve();
 143
 144   /** Process side effect se */
 145   void processSideEffect(const NlLemma& se);
 146
 147  private:
 148   /** Model-based refinement
 149    *
 150    * This is the main entry point of this class for generating lemmas on the
 151    * output channel of the theory of arithmetic.
 152    *
 153    * It is currently run at last call effort. It applies lemma schemas
 154    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
 155    * the current candidate model.
 156    *
 157    * This function returns whether we found a satisfying assignment
 158    * (Result::Sat::SAT), or not (Result::Sat::UNSAT). Note that UNSAT does not
 159    * necessarily means the whole query is UNSAT, but that the linear model was
 160    * refuted by a lemma.
 161    */
 162   Result::Sat modelBasedRefinement(const std::set<Node>& termSet);
 163
 164   /** get assertions
 165    *
 166    * Let M be the set of assertions known by THEORY_ARITH. This function adds a
 167    * set of literals M' to assertions such that M' and M are equivalent.
 168    *
 169    * Examples of how M' differs with M:
 170    * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where
 171    * c and c' are constants,
 172    * (2) M' may contain t = c if both t >= c and t <= c are in M.
 173    */
 174   void getAssertions(std::vector<Node>& assertions);
 175   /** check model
 176    *
 177    * Returns the subset of assertions whose concrete values we cannot show are
 178    * true in the current model. Notice that we typically cannot compute concrete
 179    * values for assertions involving transcendental functions. Any assertion
 180    * whose model value cannot be computed is included in the return value of
 181    * this function.
 182    */
 183   std::vector<Node> checkModelEval(const std::vector<Node>& assertions);
 184
 185   //---------------------------check model
 186   /** Check model
 187    *
 188    * Checks the current model based on solving for equalities, and using error
 189    * bounds on the Taylor approximation.
 190    *
 191    * If this function returns true, then all assertions in the input argument
 192    * "assertions" are satisfied for all interpretations of variables within
 193    * their computed bounds (as stored in d_check_model_bounds).
 194    *
 195    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
 196    * "Detecting Satisfiable Formulas".
 197    */
 198   bool checkModel(const std::vector<Node>& assertions);
 199   //---------------------------end check model
 200   /** compute relevant assertions */
 201   void computeRelevantAssertions(const std::vector<Node>& assertions,
 202                                  std::vector<Node>& keep);
 203
 204   /** run check strategy
 205    *
 206    * Check assertions for consistency in the effort LAST_CALL with a subset of
 207    * the assertions, false_asserts, that evaluate to false in the current model.
 208    *
 209    * xts : the list of (non-reduced) extended terms in the current context.
 210    *
 211    * This method adds lemmas to d_im directly.
 212    */
 213   void runStrategy(Theory::Effort effort,
 214                    const std::vector<Node>& assertions,
 215                    const std::vector<Node>& false_asserts,
 216                    const std::vector<Node>& xts);
 217
 218   /** commonly used terms */
 219   Node d_zero;
 220   Node d_one;
 221   Node d_neg_one;
 222   Node d_true;
 223   // The theory of arithmetic containing this extension.
 224   TheoryArith& d_containing;
 225   InferenceManager& d_im;
 226   /** The statistics class */
 227   NlStats d_stats;
 228   // needs last call effort
 229   bool d_needsLastCall;
 230   /**
 231    * The number of times we have the called main check method
 232    * (modelBasedRefinement). This counter is used for interleaving strategies.
 233    */
 234   unsigned d_checkCounter;
 235   /** The callback for the extended theory below */
 236   NlExtTheoryCallback d_extTheoryCb;
 237   /** Extended theory, responsible for context-dependent simplification. */
 238   ExtTheory d_extTheory;
 239   /** The non-linear model object
 240    *
 241    * This class is responsible for computing model values for arithmetic terms
 242    * and for establishing when we are able to answer "SAT".
 243    */
 244   NlModel d_model;
 245
 246   /** The transcendental extension object
 247    *
 248    * This is the subsolver responsible for running the procedure for
 249    * transcendental functions.
 250    */
 251   transcendental::TranscendentalSolver d_trSlv;
 252   /** The proof checker for proofs of the nlext. */
 253   ExtProofRuleChecker d_proofChecker;
 254   /**
 255    * Holds common lookup data for the checks implemented in the "nl-ext"
 256    * solvers (from Cimatti et al., TACAS 2017).
 257    */
 258   ExtState d_extState;
 259   /** Solver for factoring lemmas. */
 260   FactoringCheck d_factoringSlv;
 261   /** Solver for lemmas about monomial bounds. */
 262   MonomialBoundsCheck d_monomialBoundsSlv;
 263   /** Solver for lemmas about monomials. */
 264   MonomialCheck d_monomialSlv;
 265   /** Solver for lemmas that split multiplication at zero. */
 266   SplitZeroCheck d_splitZeroSlv;
 267   /** Solver for tangent plane lemmas. */
 268   TangentPlaneCheck d_tangentPlaneSlv;
 269   /** The CAD-based solver */
 270   CadSolver d_cadSlv;
 271   /** The ICP-based solver */
 272   icp::ICPSolver d_icpSlv;
 273   /** The integer and solver
 274    *
 275    * This is the subsolver responsible for running the procedure for
 276    * constraints involving integer and.
 277    */
 278   IAndSolver d_iandSlv;
 279
 280   /** The strategy for the nonlinear extension. */
 281   Strategy d_strategy;
 282
 283   /**
 284    * The approximations computed during collectModelInfo. For details, see
 285    * NlModel::getModelValueRepair.
 286    */
 287   std::map<Node, std::pair<Node, Node>> d_approximations;
 288   /**
 289    * The witnesses computed during collectModelInfo. For details, see
 290    * NlModel::getModelValueRepair.
 291    */
 292   std::map<Node, Node> d_witnesses;
 293 }; /* class NonlinearExtension */
 294
 295 }  // namespace nl
 296 }  // namespace arith
 297 }  // namespace theory
 298 }  // namespace cvc5
 299
 300 #endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */