Branch data     Line data    Source code

       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-2024 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 "smt/env_obj.h"
      25                 :            : #include "theory/arith/nl/coverings_solver.h"
      26                 :            : #include "theory/arith/nl/ext/ext_state.h"
      27                 :            : #include "theory/arith/nl/ext/factoring_check.h"
      28                 :            : #include "theory/arith/nl/ext/monomial_bounds_check.h"
      29                 :            : #include "theory/arith/nl/ext/monomial_check.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/pow2_solver.h"
      37                 :            : #include "theory/arith/nl/stats.h"
      38                 :            : #include "theory/arith/nl/strategy.h"
      39                 :            : #include "theory/arith/nl/transcendental/transcendental_solver.h"
      40                 :            : #include "theory/ext_theory.h"
      41                 :            : #include "theory/theory.h"
      42                 :            : #include "util/result.h"
      43                 :            : 
      44                 :            : namespace cvc5::internal {
      45                 :            : namespace theory {
      46                 :            : namespace eq {
      47                 :            :   class EqualityEngine;
      48                 :            : }
      49                 :            : namespace arith {
      50                 :            : 
      51                 :            : class InferenceManager;
      52                 :            : class TheoryArith;
      53                 :            : 
      54                 :            : namespace nl {
      55                 :            : 
      56                 :            : class NlLemma;
      57                 :            : 
      58                 :            : /** Non-linear extension class
      59                 :            :  *
      60                 :            :  * This class implements model-based refinement schemes
      61                 :            :  * for non-linear arithmetic, described in:
      62                 :            :  *
      63                 :            :  * - "Invariant Checking of NRA Transition Systems
      64                 :            :  * via Incremental Reduction to LRA with EUF" by
      65                 :            :  * Cimatti et al., TACAS 2017.
      66                 :            :  *
      67                 :            :  * - Section 5 of "Desiging Theory Solvers with
      68                 :            :  * Extensions" by Reynolds et al., FroCoS 2017.
      69                 :            :  *
      70                 :            :  * - "Satisfiability Modulo Transcendental
      71                 :            :  * Functions via Incremental Linearization" by Cimatti
      72                 :            :  * et al., CADE 2017.
      73                 :            :  *
      74                 :            :  * It's main functionality is a check(...) method,
      75                 :            :  * which is called by TheoryArithPrivate either:
      76                 :            :  * (1) at full effort with no conflicts or lemmas emitted, or
      77                 :            :  * (2) at last call effort.
      78                 :            :  * In this method, this class calls d_im.lemma(...)
      79                 :            :  * for valid arithmetic theory lemmas, based on the current set of assertions,
      80                 :            :  * where d_im is the inference manager of TheoryArith.
      81                 :            :  */
      82                 :            : class NonlinearExtension : EnvObj
      83                 :            : {
      84                 :            :   typedef context::CDHashSet<Node> NodeSet;
      85                 :            : 
      86                 :            :  public:
      87                 :            :   NonlinearExtension(Env& env, TheoryArith& containing);
      88                 :            :   ~NonlinearExtension();
      89                 :            :   /**
      90                 :            :    * Does non-context dependent setup for a node connected to a theory.
      91                 :            :    */
      92                 :            :   void preRegisterTerm(TNode n);
      93                 :            : 
      94                 :            :   /**
      95                 :            :    * Performs the main checks for nonlinear arithmetic, based on the current
      96                 :            :    * (linear) arithmetic model from `arithModel`. This method may already send
      97                 :            :    * lemmas, but most lemmas are buffered and sent at LAST_CALL effort by
      98                 :            :    * TheoryArith. The motivation for this strategy is to allow other
      99                 :            :    * non-terminating theories (e.g. quantifiers, strings) to run full effort
     100                 :            :    * checks, before sending the lemmas generated by non-linear.
     101                 :            :    *
     102                 :            :    * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn }
     103                 :            :    * which represents the linear arithmetic theory solver's contribution to the
     104                 :            :    * current candidate model where v1, ..., vn are arithmetic variables and
     105                 :            :    * c1, ..., cn are constants. Note, that arithmetic variables may be
     106                 :            :    * real-valued terms belonging to other theories, or abstractions of
     107                 :            :    * applications of multiplication (kind NONLINEAR_MULT).
     108                 :            :    *
     109                 :            :    * The argument termSet is the set of terms that is currently appearing in the
     110                 :            :    * assertions.
     111                 :            :    */
     112                 :            :   void checkFullEffort(std::map<Node, Node>& arithModel,
     113                 :            :                        const std::set<Node>& termSet);
     114                 :            : 
     115                 :            :   /** Does this class need a call to check(...) at last call effort? */
     116                 :     106684 :   bool hasNlTerms() const { return d_hasNlTerms; }
     117                 :            : 
     118                 :            :   /** Process side effect se */
     119                 :            :   void processSideEffect(const NlLemma& se);
     120                 :            : 
     121                 :            :  private:
     122                 :            :   /** Model-based refinement
     123                 :            :    *
     124                 :            :    * This is the main entry point of this class for generating lemmas on the
     125                 :            :    * output channel of the theory of arithmetic.
     126                 :            :    *
     127                 :            :    * It is currently run at last call effort. It applies lemma schemas
     128                 :            :    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
     129                 :            :    * the current candidate model.
     130                 :            :    *
     131                 :            :    * This function returns whether we found a satisfying assignment
     132                 :            :    * (Result::SAT), or not (Result::UNSAT). Note that UNSAT does not
     133                 :            :    * necessarily means the whole query is UNSAT, but that the linear model was
     134                 :            :    * refuted by a lemma.
     135                 :            :    */
     136                 :            :   Result::Status modelBasedRefinement(const std::set<Node>& termSet);
     137                 :            : 
     138                 :            :   /** get assertions
     139                 :            :    *
     140                 :            :    * Let M be the set of assertions known by THEORY_ARITH. This function adds a
     141                 :            :    * set of literals M' to assertions such that M' and M are equivalent.
     142                 :            :    *
     143                 :            :    * Examples of how M' differs with M:
     144                 :            :    * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where
     145                 :            :    * c and c' are constants,
     146                 :            :    * (2) M' may contain t = c if both t >= c and t <= c are in M.
     147                 :            :    */
     148                 :            :   void getAssertions(std::vector<Node>& assertions);
     149                 :            :   /** check model
     150                 :            :    *
     151                 :            :    * Returns the subset of assertions whose concrete values we cannot show are
     152                 :            :    * true in the current model. Notice that we typically cannot compute concrete
     153                 :            :    * values for assertions involving transcendental functions. Any assertion
     154                 :            :    * whose model value cannot be computed is included in the return value of
     155                 :            :    * this function.
     156                 :            :    */
     157                 :            :   std::vector<Node> getUnsatisfiedAssertions(
     158                 :            :       const std::vector<Node>& assertions);
     159                 :            : 
     160                 :            :   //---------------------------check model
     161                 :            :   /** Check model
     162                 :            :    *
     163                 :            :    * Checks the current model based on solving for equalities, and using error
     164                 :            :    * bounds on the Taylor approximation.
     165                 :            :    *
     166                 :            :    * If this function returns true, then all assertions in the input argument
     167                 :            :    * "assertions" are satisfied for all interpretations of variables within
     168                 :            :    * their computed bounds (as stored in d_check_model_bounds).
     169                 :            :    *
     170                 :            :    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
     171                 :            :    * "Detecting Satisfiable Formulas".
     172                 :            :    */
     173                 :            :   bool checkModel(const std::vector<Node>& assertions);
     174                 :            :   //---------------------------end check model
     175                 :            :   /** compute relevant assertions */
     176                 :            :   void computeRelevantAssertions(const std::vector<Node>& assertions,
     177                 :            :                                  std::vector<Node>& keep);
     178                 :            : 
     179                 :            :   /** run check strategy
     180                 :            :    *
     181                 :            :    * Check assertions for consistency in the effort LAST_CALL with a subset of
     182                 :            :    * the assertions, false_asserts, that evaluate to false in the current model.
     183                 :            :    *
     184                 :            :    * xts : the list of (non-reduced) extended terms in the current context.
     185                 :            :    *
     186                 :            :    * This method adds lemmas to d_im directly.
     187                 :            :    */
     188                 :            :   void runStrategy(Theory::Effort effort,
     189                 :            :                    const std::vector<Node>& assertions,
     190                 :            :                    const std::vector<Node>& false_asserts,
     191                 :            :                    const std::vector<Node>& xts);
     192                 :            : 
     193                 :            :   /** commonly used terms */
     194                 :            :   Node d_true;
     195                 :            :   // The theory of arithmetic containing this extension.
     196                 :            :   TheoryArith& d_containing;
     197                 :            :   /** A reference to the arithmetic state object */
     198                 :            :   TheoryState& d_astate;
     199                 :            :   InferenceManager& d_im;
     200                 :            :   /** The statistics class */
     201                 :            :   NlStats d_stats;
     202                 :            :   // needs last call effort
     203                 :            :   context::CDO<bool> d_hasNlTerms;
     204                 :            :   /**
     205                 :            :    * The number of times we have the called main check method
     206                 :            :    * (modelBasedRefinement). This counter is used for interleaving strategies.
     207                 :            :    */
     208                 :            :   unsigned d_checkCounter;
     209                 :            :   /** The callback for the extended theory below */
     210                 :            :   NlExtTheoryCallback d_extTheoryCb;
     211                 :            :   /** Extended theory, responsible for context-dependent simplification. */
     212                 :            :   ExtTheory d_extTheory;
     213                 :            :   /** The non-linear model object
     214                 :            :    *
     215                 :            :    * This class is responsible for computing model values for arithmetic terms
     216                 :            :    * and for establishing when we are able to answer "SAT".
     217                 :            :    */
     218                 :            :   NlModel d_model;
     219                 :            : 
     220                 :            :   /** The transcendental extension object
     221                 :            :    *
     222                 :            :    * This is the subsolver responsible for running the procedure for
     223                 :            :    * transcendental functions.
     224                 :            :    */
     225                 :            :   transcendental::TranscendentalSolver d_trSlv;
     226                 :            :   /**
     227                 :            :    * Holds common lookup data for the checks implemented in the "nl-ext"
     228                 :            :    * solvers (from Cimatti et al., TACAS 2017).
     229                 :            :    */
     230                 :            :   ExtState d_extState;
     231                 :            :   /** Solver for factoring lemmas. */
     232                 :            :   FactoringCheck d_factoringSlv;
     233                 :            :   /** Solver for lemmas about monomial bounds. */
     234                 :            :   MonomialBoundsCheck d_monomialBoundsSlv;
     235                 :            :   /** Solver for lemmas about monomials. */
     236                 :            :   MonomialCheck d_monomialSlv;
     237                 :            :   /** Solver for lemmas that split multiplication at zero. */
     238                 :            :   SplitZeroCheck d_splitZeroSlv;
     239                 :            :   /** Solver for tangent plane lemmas. */
     240                 :            :   TangentPlaneCheck d_tangentPlaneSlv;
     241                 :            :   /** The coverings-based solver */
     242                 :            :   CoveringsSolver d_covSlv;
     243                 :            :   /** The ICP-based solver */
     244                 :            :   icp::ICPSolver d_icpSlv;
     245                 :            :   /** The integer and solver
     246                 :            :    *
     247                 :            :    * This is the subsolver responsible for running the procedure for
     248                 :            :    * constraints involving integer and.
     249                 :            :    */
     250                 :            :   IAndSolver d_iandSlv;
     251                 :            : 
     252                 :            :   /** The pow2 solver
     253                 :            :    *
     254                 :            :    * This is the subsolver responsible for running the procedure for
     255                 :            :    * constraints involving powers of 2.
     256                 :            :    */
     257                 :            :   Pow2Solver d_pow2Slv;
     258                 :            : 
     259                 :            :   /** The strategy for the nonlinear extension. */
     260                 :            :   Strategy d_strategy;
     261                 :            : }; /* class NonlinearExtension */
     262                 :            : 
     263                 :            : }  // namespace nl
     264                 :            : }  // namespace arith
     265                 :            : }  // namespace theory
     266                 :            : }  // namespace cvc5::internal
     267                 :            : 
     268                 :            : #endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */