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                 :            :  * ITE simplification preprocessing pass.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "preprocessing/passes/ite_simp.h"
      14                 :            : 
      15                 :            : #include <vector>
      16                 :            : 
      17                 :            : #include "options/base_options.h"
      18                 :            : #include "options/smt_options.h"
      19                 :            : #include "preprocessing/assertion_pipeline.h"
      20                 :            : #include "preprocessing/preprocessing_pass_context.h"
      21                 :            : #include "theory/arith/arith_ite_utils.h"
      22                 :            : #include "theory/theory_engine.h"
      23                 :            : 
      24                 :            : using namespace std;
      25                 :            : using namespace cvc5::internal;
      26                 :            : using namespace cvc5::internal::theory;
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace preprocessing {
      30                 :            : namespace passes {
      31                 :            : 
      32                 :          0 : Node mkAssocAnd(NodeManager* nm, const std::vector<Node>& children)
      33                 :            : {
      34         [ -  - ]:          0 :   if (children.size() == 0)
      35                 :            :   {
      36                 :          0 :     return nm->mkConst(true);
      37                 :            :   }
      38         [ -  - ]:          0 :   else if (children.size() == 1)
      39                 :            :   {
      40                 :          0 :     return children[0];
      41                 :            :   }
      42                 :            :   else
      43                 :            :   {
      44                 :          0 :     const uint32_t max = kind::metakind::getMaxArityForKind(Kind::AND);
      45                 :          0 :     const uint32_t min = kind::metakind::getMinArityForKind(Kind::AND);
      46                 :            : 
      47                 :          0 :     Assert(min <= children.size());
      48                 :            : 
      49                 :          0 :     unsigned int numChildren = children.size();
      50         [ -  - ]:          0 :     if (numChildren <= max)
      51                 :            :     {
      52                 :          0 :       return nm->mkNode(Kind::AND, children);
      53                 :            :     }
      54                 :            : 
      55                 :            :     typedef std::vector<Node>::const_iterator const_iterator;
      56                 :          0 :     const_iterator it = children.begin();
      57                 :          0 :     const_iterator end = children.end();
      58                 :            : 
      59                 :            :     /* The new top-level children and the children of each sub node */
      60                 :          0 :     std::vector<Node> newChildren;
      61                 :          0 :     std::vector<Node> subChildren;
      62                 :            : 
      63 [ -  - ][ -  - ]:          0 :     while (it != end && numChildren > max)
                 [ -  - ]
      64                 :            :     {
      65                 :            :       /* Grab the next max children and make a node for them. */
      66         [ -  - ]:          0 :       for (const_iterator next = it + max; it != next; ++it, --numChildren)
      67                 :            :       {
      68                 :          0 :         subChildren.push_back(*it);
      69                 :            :       }
      70                 :          0 :       Node subNode = nm->mkNode(Kind::AND, subChildren);
      71                 :          0 :       newChildren.push_back(subNode);
      72                 :          0 :       subChildren.clear();
      73                 :          0 :     }
      74                 :            : 
      75                 :            :     /* If there's children left, "top off" the Expr. */
      76         [ -  - ]:          0 :     if (numChildren > 0)
      77                 :            :     {
      78                 :            :       /* If the leftovers are too few, just copy them into newChildren;
      79                 :            :        * otherwise make a new sub-node  */
      80         [ -  - ]:          0 :       if (numChildren < min)
      81                 :            :       {
      82         [ -  - ]:          0 :         for (; it != end; ++it)
      83                 :            :         {
      84                 :          0 :           newChildren.push_back(*it);
      85                 :            :         }
      86                 :            :       }
      87                 :            :       else
      88                 :            :       {
      89         [ -  - ]:          0 :         for (; it != end; ++it)
      90                 :            :         {
      91                 :          0 :           subChildren.push_back(*it);
      92                 :            :         }
      93                 :          0 :         Node subNode = nm->mkNode(Kind::AND, subChildren);
      94                 :          0 :         newChildren.push_back(subNode);
      95                 :          0 :       }
      96                 :            :     }
      97                 :            : 
      98                 :            :     /* It's inconceivable we could have enough children for this to fail
      99                 :            :      * (more than 2^32, in most cases?). */
     100                 :          0 :     AlwaysAssert(newChildren.size() <= max)
     101                 :          0 :         << "Too many new children in mkAssociative";
     102                 :            : 
     103                 :            :     /* It would be really weird if this happened (it would require
     104                 :            :      * min > 2, for one thing), but let's make sure. */
     105                 :          0 :     AlwaysAssert(newChildren.size() >= min)
     106                 :          0 :         << "Too few new children in mkAssociative";
     107                 :            : 
     108                 :          0 :     return nm->mkNode(Kind::AND, newChildren);
     109                 :          0 :   }
     110                 :            : }
     111                 :            : 
     112                 :            : /* -------------------------------------------------------------------------- */
     113                 :            : 
     114                 :      51756 : ITESimp::Statistics::Statistics(StatisticsRegistry& reg)
     115                 :      51756 :     : d_arithSubstitutionsAdded(reg.registerInt(
     116                 :            :           "preprocessing::passes::ITESimp::ArithSubstitutionsAdded"))
     117                 :            : {
     118                 :      51756 : }
     119                 :            : 
     120                 :         12 : Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion)
     121                 :            : {
     122         [ +  + ]:         12 :   if (!ite_utils->containsTermITE(assertion))
     123                 :            :   {
     124                 :         11 :     return assertion;
     125                 :            :   }
     126                 :            :   else
     127                 :            :   {
     128                 :          1 :     Node result = ite_utils->simpITE(assertion);
     129                 :          1 :     Node res_rewritten = rewrite(result);
     130                 :            : 
     131         [ -  + ]:          1 :     if (options().smt.simplifyWithCareEnabled)
     132                 :            :     {
     133                 :          0 :       verbose(2) << "starting simplifyWithCare()" << endl;
     134                 :          0 :       Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
     135                 :          0 :       verbose(2) << "ending simplifyWithCare()"
     136                 :          0 :                  << " post simplifyWithCare()" << postSimpWithCare.getId()
     137                 :          0 :                  << endl;
     138                 :          0 :       result = rewrite(postSimpWithCare);
     139                 :          0 :     }
     140                 :            :     else
     141                 :            :     {
     142                 :          1 :       result = res_rewritten;
     143                 :            :     }
     144                 :          1 :     return result;
     145                 :          1 :   }
     146                 :            : }
     147                 :            : 
     148                 :          5 : bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
     149                 :            : {
     150                 :          5 :   bool result = true;
     151                 :          5 :   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
     152         [ +  + ]:          5 :   if (simpDidALotOfWork)
     153                 :            :   {
     154         [ +  - ]:          1 :     if (options().smt.compressItes)
     155                 :            :     {
     156                 :          1 :       result = d_iteUtilities.compress(assertionsToPreprocess);
     157                 :            :     }
     158                 :            :   }
     159                 :            : 
     160                 :            :   // Do theory specific preprocessing passes
     161                 :          5 :   if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
     162 [ +  - ][ +  - ]:          5 :       && !options().base.incrementalSolving)
                 [ +  - ]
     163                 :            :   {
     164         [ +  + ]:          5 :     if (!simpDidALotOfWork)
     165                 :            :     {
     166                 :            :       util::ContainsTermITEVisitor& contains =
     167                 :          4 :           *(d_iteUtilities.getContainsVisitor());
     168                 :            :       arith::ArithIteUtils aiteu(
     169                 :          4 :           d_env, contains, d_preprocContext->getTopLevelSubstitutions().get());
     170                 :          4 :       bool anyItes = false;
     171         [ +  + ]:         12 :       for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
     172                 :            :       {
     173                 :          8 :         Node curr = (*assertionsToPreprocess)[i];
     174         [ -  + ]:          8 :         if (contains.containsTermITE(curr))
     175                 :            :         {
     176                 :          0 :           anyItes = true;
     177                 :          0 :           Node res = aiteu.reduceVariablesInItes(curr);
     178         [ -  - ]:          0 :           Trace("arith::ite::red") << "@ " << i << " ... " << curr << endl
     179                 :          0 :                                    << "   ->" << res << endl;
     180         [ -  - ]:          0 :           if (curr != res)
     181                 :            :           {
     182                 :          0 :             Node more = aiteu.reduceConstantIteByGCD(res);
     183         [ -  - ]:          0 :             Trace("arith::ite::red") << "  gcd->" << more << endl;
     184                 :          0 :             Node morer = rewrite(more);
     185                 :          0 :             assertionsToPreprocess->replace(
     186                 :            :                 i, morer, nullptr, TrustId::PREPROCESS_ITE_SIMP);
     187                 :          0 :           }
     188                 :          0 :         }
     189                 :          8 :       }
     190         [ +  - ]:          4 :       if (!anyItes)
     191                 :            :       {
     192                 :          4 :         unsigned prevSubCount = aiteu.getSubCount();
     193                 :          4 :         aiteu.learnSubstitutions(assertionsToPreprocess->ref());
     194         [ -  + ]:          4 :         if (prevSubCount < aiteu.getSubCount())
     195                 :            :         {
     196                 :            :           d_statistics.d_arithSubstitutionsAdded +=
     197                 :          0 :               aiteu.getSubCount() - prevSubCount;
     198                 :          0 :           bool anySuccess = false;
     199         [ -  - ]:          0 :           for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
     200                 :            :           {
     201                 :          0 :             Node curr = (*assertionsToPreprocess)[i];
     202                 :          0 :             Node next = rewrite(aiteu.applySubstitutions(curr));
     203                 :          0 :             Node res = aiteu.reduceVariablesInItes(next);
     204         [ -  - ]:          0 :             Trace("arith::ite::red") << "@ " << i << " ... " << next << endl
     205                 :          0 :                                      << "   ->" << res << endl;
     206                 :          0 :             Node more = aiteu.reduceConstantIteByGCD(res);
     207         [ -  - ]:          0 :             Trace("arith::ite::red") << "  gcd->" << more << endl;
     208         [ -  - ]:          0 :             if (more != next)
     209                 :            :             {
     210                 :          0 :               anySuccess = true;
     211                 :          0 :               break;
     212                 :            :             }
     213 [ -  - ][ -  - ]:          0 :           }
         [ -  - ][ -  - ]
     214                 :          0 :           for (size_t i = 0, N = assertionsToPreprocess->size();
     215 [ -  - ][ -  - ]:          0 :                anySuccess && i < N;
     216                 :            :                ++i)
     217                 :            :           {
     218                 :          0 :             Node curr = (*assertionsToPreprocess)[i];
     219                 :          0 :             Node next = rewrite(aiteu.applySubstitutions(curr));
     220                 :          0 :             Node res = aiteu.reduceVariablesInItes(next);
     221         [ -  - ]:          0 :             Trace("arith::ite::red") << "@ " << i << " ... " << next << endl
     222                 :          0 :                                      << "   ->" << res << endl;
     223                 :          0 :             Node more = aiteu.reduceConstantIteByGCD(res);
     224         [ -  - ]:          0 :             Trace("arith::ite::red") << "  gcd->" << more << endl;
     225                 :          0 :             Node morer = rewrite(more);
     226                 :          0 :             assertionsToPreprocess->replace(
     227                 :            :                 i, morer, nullptr, TrustId::PREPROCESS_ITE_SIMP);
     228                 :          0 :           }
     229                 :            :         }
     230                 :            :       }
     231                 :          4 :     }
     232                 :            :   }
     233                 :          5 :   return result;
     234                 :            : }
     235                 :            : 
     236                 :            : /* -------------------------------------------------------------------------- */
     237                 :            : 
     238                 :      51756 : ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
     239                 :            :     : PreprocessingPass(preprocContext, "ite-simp"),
     240                 :      51756 :       d_iteUtilities(d_env),
     241                 :      51756 :       d_statistics(statisticsRegistry())
     242                 :            : {
     243                 :      51756 : }
     244                 :            : 
     245                 :          5 : PreprocessingPassResult ITESimp::applyInternal(
     246                 :            :     AssertionPipeline* assertionsToPreprocess)
     247                 :            : {
     248                 :          5 :   d_preprocContext->spendResource(Resource::PreprocessStep);
     249                 :            : 
     250                 :          5 :   size_t nasserts = assertionsToPreprocess->size();
     251         [ +  + ]:         17 :   for (size_t i = 0; i < nasserts; ++i)
     252                 :            :   {
     253                 :         12 :     d_preprocContext->spendResource(Resource::PreprocessStep);
     254                 :         12 :     Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]);
     255                 :         12 :     assertionsToPreprocess->replace(
     256                 :            :         i, simp, nullptr, TrustId::PREPROCESS_ITE_SIMP);
     257         [ -  + ]:         12 :     if (assertionsToPreprocess->isInConflict())
     258                 :            :     {
     259                 :          0 :       return PreprocessingPassResult::CONFLICT;
     260                 :            :     }
     261         [ +  - ]:         12 :   }
     262                 :          5 :   bool done = doneSimpITE(assertionsToPreprocess);
     263         [ +  - ]:          5 :   return done ? PreprocessingPassResult::NO_CONFLICT
     264                 :          5 :               : PreprocessingPassResult::CONFLICT;
     265                 :            : }
     266                 :            : 
     267                 :            : /* -------------------------------------------------------------------------- */
     268                 :            : 
     269                 :            : }  // namespace passes
     270                 :            : }  // namespace preprocessing
     271                 :            : }  // namespace cvc5::internal