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 new non-linear solver.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arith/nl/equality_substitution.h"
      14                 :            : 
      15                 :            : #include "smt/env.h"
      16                 :            : #include "theory/arith/arith_utilities.h"
      17                 :            : 
      18                 :            : namespace cvc5::internal {
      19                 :            : namespace theory {
      20                 :            : namespace arith {
      21                 :            : namespace nl {
      22                 :            : 
      23                 :            : namespace {
      24                 :            : struct ShouldTraverse : public SubstitutionMap::ShouldTraverseCallback
      25                 :            : {
      26                 :      56445 :   bool operator()(TNode n) const override
      27                 :            :   {
      28    [ +  + ][ + ]:      56445 :     switch (theory::kindToTheoryId(n.getKind()))
      29                 :            :     {
      30                 :      24698 :       case TheoryId::THEORY_BOOL:
      31                 :      24698 :       case TheoryId::THEORY_BUILTIN: return true;
      32                 :      29003 :       case TheoryId::THEORY_ARITH: return !isTranscendentalKind(n.getKind());
      33                 :       2744 :       default: return false;
      34                 :            :     }
      35                 :            :   }
      36                 :            : };
      37                 :            : }  // namespace
      38                 :            : 
      39                 :      15002 : EqualitySubstitution::EqualitySubstitution(Env& env)
      40                 :      15002 :     : EnvObj(env), d_substitutions(std::make_unique<SubstitutionMap>())
      41                 :            : {
      42                 :      15002 : }
      43                 :        188 : void EqualitySubstitution::reset()
      44                 :            : {
      45                 :        188 :   d_substitutions = std::make_unique<SubstitutionMap>();
      46                 :        188 :   d_conflict.clear();
      47                 :        188 :   d_conflictMap.clear();
      48                 :        188 :   d_trackOrigin.clear();
      49                 :        188 : }
      50                 :            : 
      51                 :        188 : std::vector<Node> EqualitySubstitution::eliminateEqualities(
      52                 :            :     const std::vector<Node>& assertions)
      53                 :            : {
      54         [ -  + ]:        188 :   if (TraceIsOn("nl-eqs"))
      55                 :            :   {
      56         [ -  - ]:          0 :     Trace("nl-eqs") << "Input:" << std::endl;
      57         [ -  - ]:          0 :     for (const auto& a : assertions)
      58                 :            :     {
      59         [ -  - ]:          0 :       Trace("nl-eqs") << "\t" << a << std::endl;
      60                 :            :     }
      61                 :            :   }
      62                 :        188 :   std::set<TNode> tracker;
      63                 :        188 :   std::vector<Node> asserts = assertions;
      64                 :        188 :   std::vector<Node> next;
      65                 :        188 :   const ShouldTraverse stc;
      66                 :            : 
      67                 :        188 :   size_t last_size = 0;
      68         [ +  + ]:        446 :   while (asserts.size() != last_size)
      69                 :            :   {
      70                 :        278 :     last_size = asserts.size();
      71                 :            :     // collect all eliminations from original into d_substitutions
      72         [ +  + ]:       9906 :     for (const auto& orig : asserts)
      73                 :            :     {
      74         [ +  + ]:       9757 :       if (orig.getKind() != Kind::EQUAL) continue;
      75                 :       1411 :       tracker.clear();
      76                 :       1411 :       d_substitutions->invalidateCache();
      77                 :            :       Node o =
      78                 :       1411 :           d_substitutions->apply(orig, d_env.getRewriter(), &tracker, &stc);
      79         [ +  + ]:       1411 :       if (o.getKind() != Kind::EQUAL) continue;
      80 [ -  + ][ -  + ]:       1282 :       Assert(o.getNumChildren() == 2);
                 [ -  - ]
      81         [ +  + ]:       2672 :       for (size_t i = 0; i < 2; ++i)
      82                 :            :       {
      83 [ -  + ][ -  + ]:       1989 :         const auto& l = (o[i].getKind() == Kind::TO_REAL ? o[i][0] : o[i]);
                 [ -  - ]
      84                 :            :         const auto& r =
      85 [ -  + ][ -  + ]:       1989 :             (o[1 - i].getKind() == Kind::TO_REAL ? o[1 - i][0] : o[1 - i]);
                 [ -  - ]
      86                 :            :         // lhs can't be constant
      87         [ +  + ]:       1989 :         if (l.isConst()) continue;
      88                 :            :         // types must match (otherwise we might have int/real issues)
      89         [ -  + ]:       4935 :         if (!CVC5_EQUAL(r.getType(), l.getType())) continue;
      90                 :            :         // can't substitute stuff from other theories
      91         [ +  + ]:       1645 :         if (!Theory::isLeafOf(l, TheoryId::THEORY_ARITH)) continue;
      92                 :            :         // can't substitute the same thing twice
      93         [ -  + ]:        736 :         if (d_substitutions->hasSubstitution(l)) continue;
      94                 :            :         // lhs can't be a subexpression of rhs, would leaf to recursion
      95         [ +  + ]:        736 :         if (expr::hasSubterm(r, l)) continue;
      96                 :            :         // the same, but after substitution
      97                 :        599 :         d_substitutions->invalidateCache();
      98         [ -  + ]:        599 :         if (expr::hasSubterm(d_substitutions->apply(r, nullptr, nullptr, &stc),
      99                 :            :                              l))
     100                 :          0 :           continue;
     101         [ +  - ]:       1198 :         Trace("nl-eqs") << "Found substitution " << l << " -> " << r
     102                 :          0 :                         << std::endl
     103                 :        599 :                         << " from " << o << " / " << orig << std::endl;
     104                 :        599 :         d_substitutions->addSubstitution(l, r);
     105                 :        599 :         d_trackOrigin.emplace(l, o);
     106         [ +  + ]:        599 :         if (o != orig)
     107                 :            :         {
     108                 :        153 :           addToConflictMap(o, orig, tracker);
     109                 :            :         }
     110                 :        599 :         break;
     111 [ +  + ][ +  + ]:       3978 :       }
     112         [ +  + ]:       1411 :     }
     113                 :            : 
     114                 :            :     // simplify with subs from original into next
     115                 :        278 :     next.clear();
     116         [ +  + ]:       9346 :     for (const auto& a : asserts)
     117                 :            :     {
     118                 :       9088 :       tracker.clear();
     119                 :       9088 :       d_substitutions->invalidateCache();
     120                 :            :       Node simp =
     121                 :       9088 :           d_substitutions->apply(a, d_env.getRewriter(), &tracker, &stc);
     122         [ +  + ]:       9088 :       if (simp.isConst())
     123                 :            :       {
     124         [ +  + ]:        894 :         if (simp.getConst<bool>())
     125                 :            :         {
     126                 :        874 :           continue;
     127                 :            :         }
     128         [ +  - ]:         20 :         Trace("nl-eqs") << "Simplified " << a << " to " << simp << std::endl;
     129         [ +  + ]:         62 :         for (TNode t : tracker)
     130                 :            :         {
     131         [ +  - ]:         42 :           Trace("nl-eqs") << "Tracker has " << t << std::endl;
     132                 :         42 :           auto toit = d_trackOrigin.find(t);
     133 [ -  + ][ -  + ]:         42 :           Assert(toit != d_trackOrigin.end());
                 [ -  - ]
     134                 :         42 :           d_conflict.emplace_back(toit->second);
     135                 :         42 :         }
     136                 :         20 :         d_conflict.emplace_back(a);
     137                 :         20 :         postprocessConflict(d_conflict);
     138         [ +  - ]:         20 :         Trace("nl-eqs") << "Direct conflict: " << d_conflict << std::endl;
     139         [ +  - ]:         40 :         Trace("nl-eqs") << std::endl
     140                 :          0 :                         << d_conflict.size() << " vs "
     141                 :         20 :                         << std::distance(d_substitutions->begin(),
     142                 :          0 :                                          d_substitutions->end())
     143                 :          0 :                         << std::endl
     144                 :         20 :                         << std::endl;
     145                 :         20 :         return {};
     146                 :            :       }
     147         [ +  + ]:       8194 :       if (simp != a)
     148                 :            :       {
     149         [ +  - ]:       2174 :         Trace("nl-eqs") << "Simplified " << a << " to " << simp << std::endl;
     150                 :       2174 :         addToConflictMap(simp, a, tracker);
     151                 :            :       }
     152                 :       8194 :       next.emplace_back(simp);
     153    [ +  + ][ + ]:       9088 :     }
     154                 :        258 :     asserts = std::move(next);
     155                 :            :   }
     156                 :        168 :   d_conflict.clear();
     157         [ -  + ]:        168 :   if (TraceIsOn("nl-eqs"))
     158                 :            :   {
     159         [ -  - ]:          0 :     Trace("nl-eqs") << "Output:" << std::endl;
     160         [ -  - ]:          0 :     for (const auto& a : asserts)
     161                 :            :     {
     162         [ -  - ]:          0 :       Trace("nl-eqs") << "\t" << a << std::endl;
     163                 :            :     }
     164         [ -  - ]:          0 :     Trace("nl-eqs") << "Substitutions:" << std::endl;
     165         [ -  - ]:          0 :     for (const auto& subs : d_substitutions->getSubstitutions())
     166                 :            :     {
     167         [ -  - ]:          0 :       Trace("nl-eqs") << "\t" << subs.first << " -> " << subs.second
     168                 :          0 :                       << std::endl;
     169                 :          0 :     }
     170                 :            :   }
     171                 :        168 :   return asserts;
     172                 :        188 : }
     173                 :        193 : void EqualitySubstitution::postprocessConflict(
     174                 :            :     std::vector<Node>& conflict) const
     175                 :            : {
     176         [ +  - ]:        193 :   Trace("nl-eqs") << "Postprocessing " << conflict << std::endl;
     177                 :        193 :   std::set<Node> result;
     178         [ +  + ]:        867 :   for (const auto& c : conflict)
     179                 :            :   {
     180                 :        674 :     auto it = d_conflictMap.find(c);
     181         [ +  + ]:        674 :     if (it == d_conflictMap.end())
     182                 :            :     {
     183                 :        522 :       result.insert(c);
     184                 :            :     }
     185                 :            :     else
     186                 :            :     {
     187         [ +  - ]:        152 :       Trace("nl-eqs") << "Origin of " << c << ": " << it->second << std::endl;
     188                 :        152 :       result.insert(it->second.begin(), it->second.end());
     189                 :            :     }
     190                 :            :   }
     191                 :        193 :   conflict.clear();
     192                 :        193 :   conflict.insert(conflict.end(), result.begin(), result.end());
     193         [ +  - ]:        193 :   Trace("nl-eqs") << "-> " << conflict << std::endl;
     194                 :        193 : }
     195                 :       6606 : void EqualitySubstitution::insertOrigins(std::set<Node>& dest,
     196                 :            :                                          const Node& n) const
     197                 :            : {
     198                 :       6606 :   auto it = d_conflictMap.find(n);
     199         [ +  + ]:       6606 :   if (it == d_conflictMap.end())
     200                 :            :   {
     201                 :       5520 :     dest.insert(n);
     202                 :            :   }
     203                 :            :   else
     204                 :            :   {
     205                 :       1086 :     dest.insert(it->second.begin(), it->second.end());
     206                 :            :   }
     207                 :       6606 : }
     208                 :       2327 : void EqualitySubstitution::addToConflictMap(const Node& n,
     209                 :            :                                             const Node& orig,
     210                 :            :                                             const std::set<TNode>& tracker)
     211                 :            : {
     212                 :       2327 :   std::set<Node> origins;
     213                 :       2327 :   insertOrigins(origins, orig);
     214         [ +  + ]:       6606 :   for (const auto& t : tracker)
     215                 :            :   {
     216                 :       4279 :     auto tit = d_trackOrigin.find(t);
     217 [ -  + ][ -  + ]:       4279 :     Assert(tit != d_trackOrigin.end());
                 [ -  - ]
     218                 :       4279 :     insertOrigins(origins, tit->second);
     219                 :            :   }
     220                 :       2327 :   d_conflictMap.emplace(n, std::vector<Node>(origins.begin(), origins.end()));
     221                 :       2327 : }
     222                 :            : 
     223                 :            : }  // namespace nl
     224                 :            : }  // namespace arith
     225                 :            : }  // namespace theory
     226                 :            : }  // namespace cvc5::internal