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                 :            :  * Implement intersection of intervals for propagation.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arith/nl/icp/intersection.h"
      14                 :            : 
      15                 :            : #ifdef CVC5_POLY_IMP
      16                 :            : 
      17                 :            : #include <poly/polyxx.h>
      18                 :            : 
      19                 :            : #include <iostream>
      20                 :            : 
      21                 :            : #include "base/check.h"
      22                 :            : #include "base/output.h"
      23                 :            : #include "theory/arith/nl/poly_conversion.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace theory {
      27                 :            : namespace arith {
      28                 :            : namespace nl {
      29                 :            : namespace icp {
      30                 :            : 
      31                 :          4 : PropagationResult intersect_interval_with(poly::Interval& cur,
      32                 :            :                                           const poly::Interval& res,
      33                 :            :                                           std::size_t size_threshold)
      34                 :            : {
      35         [ +  - ]:          8 :   Trace("nl-icp-debug") << cur << " := " << cur << " intersected with " << res
      36                 :          4 :                         << std::endl;
      37                 :            : 
      38                 :          4 :   if (bitsize(get_lower(res)) > size_threshold
      39 [ +  - ][ -  + ]:          4 :       || bitsize(get_upper(res)) > size_threshold)
                 [ -  + ]
      40                 :            :   {
      41         [ -  - ]:          0 :     Trace("nl-icp-debug") << "Reached bitsize threshold" << std::endl;
      42                 :          0 :     return PropagationResult::NOT_CHANGED;
      43                 :            :   }
      44                 :            : 
      45                 :            :   // Basic idea to organize this function:
      46                 :            :   // The bounds for res have 5 positions:
      47                 :            :   // 1 < 2 (lower(cur)) < 3 < 4 (upper(cur)) < 5
      48                 :            : 
      49         [ -  + ]:          4 :   if (get_upper(res) < get_lower(cur))
      50                 :            :   {
      51                 :            :     // upper(res) at 1
      52         [ -  - ]:          0 :     Trace("nl-icp-debug") << "res < cur -> conflict" << std::endl;
      53                 :          0 :     return PropagationResult::CONFLICT;
      54                 :            :   }
      55         [ +  + ]:          4 :   if (get_upper(res) == get_lower(cur))
      56                 :            :   {
      57                 :            :     // upper(res) at 2
      58 [ -  + ][ -  - ]:          2 :     if (get_upper_open(res) || get_lower_open(cur))
                 [ +  - ]
      59                 :            :     {
      60         [ +  - ]:          4 :       Trace("nl-icp-debug")
      61                 :          2 :           << "meet at lower, but one is open -> conflict" << std::endl;
      62                 :          2 :       return PropagationResult::CONFLICT;
      63                 :            :     }
      64         [ -  - ]:          0 :     if (!is_point(cur))
      65                 :            :     {
      66         [ -  - ]:          0 :       Trace("nl-icp-debug")
      67                 :          0 :           << "contracts to point interval at lower" << std::endl;
      68                 :          0 :       cur = poly::Interval(get_upper(res));
      69                 :          0 :       return PropagationResult::CONTRACTED;
      70                 :            :     }
      71                 :          0 :     return PropagationResult::NOT_CHANGED;
      72                 :            :   }
      73 [ -  + ][ -  + ]:          2 :   Assert(get_upper(res) > get_lower(cur))
                 [ -  - ]
      74                 :          0 :       << "Comparison operator does weird stuff.";
      75         [ -  + ]:          2 :   if (get_upper(res) < get_upper(cur))
      76                 :            :   {
      77                 :            :     // upper(res) at 3
      78         [ -  - ]:          0 :     if (get_lower(res) < get_lower(cur))
      79                 :            :     {
      80                 :            :       // lower(res) at 1
      81         [ -  - ]:          0 :       Trace("nl-icp-debug") << "lower(cur) .. upper(res)" << std::endl;
      82                 :          0 :       cur.set_upper(get_upper(res), get_upper_open(res));
      83                 :          0 :       return PropagationResult::CONTRACTED;
      84                 :            :     }
      85         [ -  - ]:          0 :     if (get_lower(res) == get_lower(cur))
      86                 :            :     {
      87                 :            :       // lower(res) at 2
      88         [ -  - ]:          0 :       Trace("nl-icp-debug")
      89                 :          0 :           << "meet at lower, lower(cur) .. upper(res)" << std::endl;
      90                 :          0 :       cur = poly::Interval(get_lower(cur),
      91 [ -  - ][ -  - ]:          0 :                            get_lower_open(cur) || get_lower_open(res),
      92                 :            :                            get_upper(res),
      93                 :          0 :                            get_upper_open(res));
      94 [ -  - ][ -  - ]:          0 :       if (get_lower_open(cur) && !get_lower_open(res))
                 [ -  - ]
      95                 :            :       {
      96                 :          0 :         return PropagationResult::CONTRACTED;
      97                 :            :       }
      98                 :          0 :       return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
      99                 :            :     }
     100                 :          0 :     Assert(get_lower(res) > get_lower(cur))
     101                 :          0 :         << "Comparison operator does weird stuff.";
     102                 :            :     // lower(res) at 3
     103         [ -  - ]:          0 :     Trace("nl-icp-debug") << "cur covers res" << std::endl;
     104                 :          0 :     cur = res;
     105                 :          0 :     return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
     106                 :            :   }
     107         [ -  + ]:          2 :   if (get_upper(res) == get_upper(cur))
     108                 :            :   {
     109                 :            :     // upper(res) at 4
     110         [ -  - ]:          0 :     if (get_lower(res) < get_lower(cur))
     111                 :            :     {
     112                 :            :       // lower(res) at 1
     113         [ -  - ]:          0 :       Trace("nl-icp-debug") << "res covers cur but meet at upper" << std::endl;
     114 [ -  - ][ -  - ]:          0 :       if (get_upper_open(res) && !get_upper_open(cur))
                 [ -  - ]
     115                 :            :       {
     116                 :          0 :         cur.set_upper(get_upper(cur), true);
     117                 :          0 :         return PropagationResult::CONTRACTED;
     118                 :            :       }
     119                 :          0 :       return PropagationResult::NOT_CHANGED;
     120                 :            :     }
     121         [ -  - ]:          0 :     if (get_lower(res) == get_lower(cur))
     122                 :            :     {
     123                 :            :       // lower(res) at 2
     124         [ -  - ]:          0 :       Trace("nl-icp-debug") << "same bounds but check openness" << std::endl;
     125                 :          0 :       bool changed = false;
     126 [ -  - ][ -  - ]:          0 :       if (get_lower_open(res) && !get_lower_open(cur))
                 [ -  - ]
     127                 :            :       {
     128                 :          0 :         changed = true;
     129                 :          0 :         cur.set_lower(get_lower(cur), true);
     130                 :            :       }
     131 [ -  - ][ -  - ]:          0 :       if (get_upper_open(res) && !get_upper_open(cur))
                 [ -  - ]
     132                 :            :       {
     133                 :          0 :         changed = true;
     134                 :          0 :         cur.set_upper(get_upper(cur), true);
     135                 :            :       }
     136         [ -  - ]:          0 :       if (changed)
     137                 :            :       {
     138         [ -  - ]:          0 :         if ((get_lower_open(res) || !get_upper_open(cur))
     139 [ -  - ][ -  - ]:          0 :             && (get_upper_open(res) || !get_upper_open(cur)))
         [ -  - ][ -  - ]
     140                 :            :         {
     141                 :          0 :           return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
     142                 :            :         }
     143                 :          0 :         return PropagationResult::CONTRACTED;
     144                 :            :       }
     145                 :          0 :       return PropagationResult::NOT_CHANGED;
     146                 :            :     }
     147                 :          0 :     Assert(get_lower(res) > get_lower(cur))
     148                 :          0 :         << "Comparison operator does weird stuff.";
     149                 :            :     // lower(res) at 3
     150         [ -  - ]:          0 :     Trace("nl-icp-debug") << "cur covers res but meet at upper" << std::endl;
     151                 :          0 :     cur = poly::Interval(get_lower(res),
     152                 :          0 :                          get_lower_open(res),
     153                 :            :                          get_upper(res),
     154 [ -  - ][ -  - ]:          0 :                          get_upper_open(cur) || get_upper_open(res));
     155 [ -  - ][ -  - ]:          0 :     if (get_upper_open(cur) && !get_upper_open(res))
                 [ -  - ]
     156                 :            :     {
     157                 :          0 :       return PropagationResult::CONTRACTED;
     158                 :            :     }
     159                 :          0 :     return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
     160                 :            :   }
     161                 :            : 
     162 [ -  + ][ -  + ]:          2 :   Assert(get_upper(res) > get_upper(cur))
                 [ -  - ]
     163                 :          0 :       << "Comparison operator does weird stuff.";
     164                 :            :   // upper(res) at 5
     165                 :            : 
     166         [ -  + ]:          2 :   if (get_lower(res) < get_lower(cur))
     167                 :            :   {
     168                 :            :     // lower(res) at 1
     169         [ -  - ]:          0 :     Trace("nl-icp-debug") << "res covers cur" << std::endl;
     170                 :          0 :     return PropagationResult::NOT_CHANGED;
     171                 :            :   }
     172         [ +  - ]:          2 :   if (get_lower(res) == get_lower(cur))
     173                 :            :   {
     174                 :            :     // lower(res) at 2
     175         [ +  - ]:          2 :     Trace("nl-icp-debug") << "res covers cur but meet at lower" << std::endl;
     176 [ +  - ][ -  + ]:          2 :     if (get_lower_open(res) && is_point(cur))
                 [ -  + ]
     177                 :            :     {
     178                 :          0 :       return PropagationResult::CONFLICT;
     179                 :            :     }
     180 [ +  - ][ -  + ]:          2 :     else if (get_lower_open(res) && !get_lower_open(cur))
                 [ -  + ]
     181                 :            :     {
     182                 :          0 :       cur.set_lower(get_lower(cur), true);
     183                 :          0 :       return PropagationResult::CONTRACTED;
     184                 :            :     }
     185                 :          2 :     return PropagationResult::NOT_CHANGED;
     186                 :            :   }
     187                 :          0 :   Assert(get_lower(res) > get_lower(cur))
     188                 :          0 :       << "Comparison operator does weird stuff.";
     189         [ -  - ]:          0 :   if (get_lower(res) < get_upper(cur))
     190                 :            :   {
     191                 :            :     // lower(res) at 3
     192         [ -  - ]:          0 :     Trace("nl-icp-debug") << "lower(res) .. upper(cur)" << std::endl;
     193                 :          0 :     cur.set_lower(get_lower(res), get_lower_open(res));
     194                 :          0 :     return PropagationResult::CONTRACTED;
     195                 :            :   }
     196         [ -  - ]:          0 :   if (get_lower(res) == get_upper(cur))
     197                 :            :   {
     198                 :            :     // lower(res) at 4
     199 [ -  - ][ -  - ]:          0 :     if (get_lower_open(res) || get_upper_open(cur))
                 [ -  - ]
     200                 :            :     {
     201         [ -  - ]:          0 :       Trace("nl-icp-debug")
     202                 :          0 :           << "meet at upper, but one is open -> conflict" << std::endl;
     203                 :          0 :       return PropagationResult::CONFLICT;
     204                 :            :     }
     205         [ -  - ]:          0 :     if (!is_point(cur))
     206                 :            :     {
     207         [ -  - ]:          0 :       Trace("nl-icp-debug")
     208                 :          0 :           << "contracts to point interval at upper" << std::endl;
     209                 :          0 :       cur = poly::Interval(get_lower(res));
     210                 :          0 :       return PropagationResult::CONTRACTED;
     211                 :            :     }
     212                 :          0 :     return PropagationResult::NOT_CHANGED;
     213                 :            :   }
     214                 :            : 
     215                 :          0 :   Assert(get_lower(res) > get_upper(cur));
     216                 :            :   // lower(res) at 5
     217         [ -  - ]:          0 :   Trace("nl-icp-debug") << "res > cur -> conflict" << std::endl;
     218                 :          0 :   return PropagationResult::CONFLICT;
     219                 :            : }
     220                 :            : 
     221                 :            : }  // namespace icp
     222                 :            : }  // namespace nl
     223                 :            : }  // namespace arith
     224                 :            : }  // namespace theory
     225                 :            : }  // namespace cvc5::internal
     226                 :            : 
     227                 :            : #endif