Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of non-linear solver.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arith/nl/strategy.h"
      14                 :            : 
      15                 :            : #include <iostream>
      16                 :            : 
      17                 :            : #include "base/check.h"
      18                 :            : #include "options/arith_options.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : namespace arith {
      23                 :            : namespace nl {
      24                 :            : 
      25                 :         31 : std::ostream& operator<<(std::ostream& os, InferStep step)
      26                 :            : {
      27 [ +  + ][ +  + ]:         31 :   switch (step)
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  - ]
                    [ - ]
      28                 :            :   {
      29                 :          1 :     case InferStep::NONE: return os << "NONE";
      30                 :          1 :     case InferStep::BREAK: return os << "BREAK";
      31                 :          1 :     case InferStep::FLUSH_WAITING_LEMMAS: return os << "FLUSH_WAITING_LEMMAS";
      32                 :          1 :     case InferStep::COVERINGS_INIT: return os << "COVERINGS_INIT";
      33                 :          1 :     case InferStep::COVERINGS_FULL: return os << "COVERINGS_FULL";
      34                 :          1 :     case InferStep::NL_FACTORING: return os << "NL_FACTORING";
      35                 :          1 :     case InferStep::NL_FLATTEN_MON: return os << "NL_FLATTEN_MON";
      36                 :          1 :     case InferStep::IAND_INIT: return os << "IAND_INIT";
      37                 :          1 :     case InferStep::IAND_FULL: return os << "IAND_FULL";
      38                 :          1 :     case InferStep::IAND_INITIAL: return os << "IAND_INITIAL";
      39                 :          1 :     case InferStep::PIAND_INIT: return os << "PIAND_INIT";
      40                 :          1 :     case InferStep::PIAND_FULL: return os << "PIAND_FULL";
      41                 :          1 :     case InferStep::PIAND_INITIAL: return os << "PIAND_INITIAL";
      42                 :          1 :     case InferStep::POW2_INIT: return os << "POW2_INIT";
      43                 :          1 :     case InferStep::POW2_FULL: return os << "POW2_FULL";
      44                 :          1 :     case InferStep::POW2_INITIAL: return os << "POW2_INITIAL";
      45                 :          1 :     case InferStep::ICP: return os << "ICP";
      46                 :          1 :     case InferStep::NL_INIT: return os << "NL_INIT";
      47                 :          1 :     case InferStep::NL_MONOMIAL_INFER_BOUNDS:
      48                 :          1 :       return os << "NL_MONOMIAL_INFER_BOUNDS";
      49                 :          1 :     case InferStep::NL_MONOMIAL_MAGNITUDE0:
      50                 :          1 :       return os << "NL_MONOMIAL_MAGNITUDE0";
      51                 :          1 :     case InferStep::NL_MONOMIAL_MAGNITUDE1:
      52                 :          1 :       return os << "NL_MONOMIAL_MAGNITUDE1";
      53                 :          1 :     case InferStep::NL_MONOMIAL_MAGNITUDE2:
      54                 :          1 :       return os << "NL_MONOMIAL_MAGNITUDE2";
      55                 :          1 :     case InferStep::NL_MONOMIAL_SIGN: return os << "NL_MONOMIAL_SIGN";
      56                 :          1 :     case InferStep::NL_RESOLUTION_BOUNDS: return os << "NL_RESOLUTION_BOUNDS";
      57                 :          1 :     case InferStep::NL_SPLIT_ZERO: return os << "NL_SPLIT_ZERO";
      58                 :          1 :     case InferStep::NL_TANGENT_PLANES: return os << "NL_TANGENT_PLANES";
      59                 :          1 :     case InferStep::NL_TANGENT_PLANES_WAITING:
      60                 :          1 :       return os << "NL_TANGENT_PLANES_WAITING";
      61                 :          1 :     case InferStep::TRANS_INIT: return os << "TRANS_INIT";
      62                 :          1 :     case InferStep::TRANS_INITIAL: return os << "TRANS_INITIAL";
      63                 :          1 :     case InferStep::TRANS_MONOTONIC: return os << "TRANS_MONOTONIC";
      64                 :          1 :     case InferStep::TRANS_TANGENT_PLANES: return os << "TRANS_TANGENT_PLANES";
      65                 :          0 :     case InferStep::UNKNOWN: return os << "?";
      66                 :          0 :     default: Unreachable(); return os << "UNKNOWN_STEP";
      67                 :            :   }
      68                 :            : }
      69                 :            : 
      70                 :            : namespace {
      71                 :            : /** Puts a new InferStep into a StepSequence */
      72                 :      68061 : inline StepSequence& operator<<(StepSequence& steps, InferStep s)
      73                 :            : {
      74                 :      68061 :   steps.emplace_back(s);
      75                 :      68061 :   return steps;
      76                 :            : }
      77                 :            : }  // namespace
      78                 :            : 
      79                 :       1687 : void Interleaving::add(const StepSequence& ss, std::size_t constant)
      80                 :            : {
      81                 :       1687 :   d_branches.emplace_back(Branch{ss, constant});
      82                 :       1687 :   d_size += constant;
      83                 :       1687 : }
      84                 :          0 : void Interleaving::resetCounter() { d_counter = 0; }
      85                 :            : 
      86                 :      12364 : const StepSequence& Interleaving::get()
      87                 :            : {
      88 [ -  + ][ -  + ]:      12364 :   Assert(!d_branches.empty())
                 [ -  - ]
      89                 :          0 :       << "Can not get next sequence from an empty interleaving.";
      90                 :      12364 :   std::size_t cnt = d_counter;
      91                 :            :   // Increase the counter
      92                 :      12364 :   d_counter = (d_counter + 1) % d_size;
      93         [ +  - ]:      12364 :   for (const auto& branch : d_branches)
      94                 :            :   {
      95         [ +  - ]:      12364 :     if (cnt < branch.d_interleavingConstant)
      96                 :            :     {
      97                 :            :       // This is the current branch
      98                 :      12364 :       return branch.d_steps;
      99                 :            :     }
     100                 :          0 :     cnt -= branch.d_interleavingConstant;
     101                 :            :   }
     102                 :          0 :   DebugUnhandled() << "Something went wrong.";
     103                 :            :   return d_branches[0].d_steps;
     104                 :            : }
     105                 :      12364 : bool Interleaving::empty() const { return d_branches.empty(); }
     106                 :            : 
     107                 :     273876 : bool StepGenerator::hasNext() const { return d_next < d_steps.size(); }
     108                 :     272925 : InferStep StepGenerator::next() { return d_steps[d_next++]; }
     109                 :            : 
     110                 :      12364 : bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); }
     111                 :       1687 : void Strategy::initializeStrategy(const Options& options)
     112                 :            : {
     113                 :       1687 :   StepSequence one;
     114         [ +  + ]:       1687 :   if (options.arith.nlICP)
     115                 :            :   {
     116                 :          4 :     one << InferStep::ICP << InferStep::BREAK;
     117                 :            :   }
     118         [ +  + ]:       1687 :   if (options.arith.nlExt == options::NlExtMode::FULL
     119         [ +  + ]:        163 :       || options.arith.nlExt == options::NlExtMode::LIGHT)
     120                 :            :   {
     121                 :       1675 :     one << InferStep::NL_INIT << InferStep::BREAK;
     122                 :            :   }
     123         [ +  + ]:       1687 :   if (options.arith.nlExt == options::NlExtMode::FULL)
     124                 :            :   {
     125                 :       1524 :     one << InferStep::TRANS_INIT << InferStep::BREAK;
     126         [ +  + ]:       1524 :     if (options.arith.nlExtSplitZero)
     127                 :            :     {
     128                 :          2 :       one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK;
     129                 :            :     }
     130                 :       1524 :     one << InferStep::TRANS_INITIAL << InferStep::BREAK;
     131                 :            :   }
     132                 :       1687 :   one << InferStep::IAND_INIT;
     133                 :       1687 :   one << InferStep::IAND_INITIAL << InferStep::BREAK;
     134                 :       1687 :   one << InferStep::PIAND_INIT;
     135                 :       1687 :   one << InferStep::PIAND_INITIAL << InferStep::BREAK;
     136                 :       1687 :   one << InferStep::POW2_INIT;
     137                 :       1687 :   one << InferStep::POW2_INITIAL << InferStep::BREAK;
     138         [ +  + ]:       1687 :   if (options.arith.nlExt == options::NlExtMode::FULL
     139         [ +  + ]:        163 :       || options.arith.nlExt == options::NlExtMode::LIGHT)
     140                 :            :   {
     141                 :       1675 :     one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK;
     142                 :       1675 :     one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK;
     143                 :            :   }
     144         [ +  - ]:       1687 :   if (options.arith.nlExtFlattenMon)
     145                 :            :   {
     146                 :       1687 :     one << InferStep::NL_FLATTEN_MON << InferStep::BREAK;
     147                 :            :   }
     148         [ +  + ]:       1687 :   if (options.arith.nlExt == options::NlExtMode::FULL)
     149                 :            :   {
     150                 :       1524 :     one << InferStep::TRANS_MONOTONIC << InferStep::BREAK;
     151                 :       1524 :     one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK;
     152                 :       1524 :     one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK;
     153                 :       1524 :     one << InferStep::NL_MONOMIAL_INFER_BOUNDS;
     154         [ +  - ]:       1524 :     if (options.arith.nlExtTangentPlanes
     155         [ -  + ]:       1524 :         && options.arith.nlExtTangentPlanesInterleave)
     156                 :            :     {
     157                 :          0 :       one << InferStep::NL_TANGENT_PLANES;
     158                 :            :     }
     159                 :       1524 :     one << InferStep::BREAK;
     160                 :            :   }
     161                 :       1687 :   one << InferStep::IAND_FULL << InferStep::BREAK;
     162                 :       1687 :   one << InferStep::PIAND_FULL << InferStep::BREAK;
     163                 :       1687 :   one << InferStep::POW2_FULL << InferStep::BREAK;
     164         [ +  + ]:       1687 :   if (options.arith.nlCov)
     165                 :            :   {
     166                 :        259 :     one << InferStep::COVERINGS_INIT << InferStep::BREAK;
     167                 :        259 :     one << InferStep::COVERINGS_FULL << InferStep::BREAK;
     168                 :            :   }
     169         [ +  + ]:       1687 :   if (options.arith.nlExt == options::NlExtMode::FULL
     170 [ +  + ][ -  + ]:       1524 :       && (!options.arith.nlCov || options.arith.nlCovForce))
     171                 :            :   {
     172                 :            :     // if nl-cov is not enabled or we forced it to be enabled, then we use
     173                 :            :     // heuristic non-terminating techniques as a last resort
     174                 :       1428 :     one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK;
     175         [ +  - ]:       1428 :     if (options.arith.nlExtFactor)
     176                 :            :     {
     177                 :       1428 :       one << InferStep::NL_FACTORING << InferStep::BREAK;
     178                 :            :     }
     179         [ -  + ]:       1428 :     if (options.arith.nlExtResBound)
     180                 :            :     {
     181                 :          0 :       one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK;
     182                 :            :     }
     183         [ +  - ]:       1428 :     if (options.arith.nlExtTangentPlanes
     184         [ +  - ]:       1428 :         && !options.arith.nlExtTangentPlanesInterleave)
     185                 :            :     {
     186                 :       1428 :       one << InferStep::NL_TANGENT_PLANES_WAITING;
     187                 :            :     }
     188         [ +  - ]:       1428 :     if (options.arith.nlExtTfTangentPlanes)
     189                 :            :     {
     190                 :       1428 :       one << InferStep::TRANS_TANGENT_PLANES;
     191                 :            :     }
     192                 :       1428 :     one << InferStep::BREAK;
     193                 :            :   }
     194                 :            : 
     195                 :       1687 :   d_interleaving.add(one);
     196                 :       1687 : }
     197                 :      12364 : StepGenerator Strategy::getStrategy()
     198                 :            : {
     199                 :      12364 :   return StepGenerator(d_interleaving.get());
     200                 :            : }
     201                 :            : 
     202                 :            : }  // namespace nl
     203                 :            : }  // namespace arith
     204                 :            : }  // namespace theory
     205                 :            : }  // namespace cvc5::internal