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                 :            :  * The NlExtPurify preprocessing pass.
      11                 :            :  *
      12                 :            :  * Purifies non-linear terms.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "preprocessing/passes/nl_ext_purify.h"
      16                 :            : 
      17                 :            : #include "expr/skolem_manager.h"
      18                 :            : #include "preprocessing/assertion_pipeline.h"
      19                 :            : #include "theory/rewriter.h"
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : namespace preprocessing {
      23                 :            : namespace passes {
      24                 :            : 
      25                 :            : using namespace std;
      26                 :            : using namespace cvc5::internal::theory;
      27                 :            : 
      28                 :       2944 : Node NlExtPurify::purifyNlTerms(TNode n,
      29                 :            :                                 NodeMap& cache,
      30                 :            :                                 NodeMap& bcache,
      31                 :            :                                 std::vector<Node>& var_eq,
      32                 :            :                                 bool beneathMult)
      33                 :            : {
      34                 :       2944 :   NodeManager* nm = nodeManager();
      35         [ +  + ]:       2944 :   if (beneathMult)
      36                 :            :   {
      37                 :       2294 :     NodeMap::iterator find = bcache.find(n);
      38         [ +  + ]:       2294 :     if (find != bcache.end())
      39                 :            :     {
      40                 :       2170 :       return (*find).second;
      41                 :            :     }
      42                 :            :   }
      43                 :            :   else
      44                 :            :   {
      45                 :        650 :     NodeMap::iterator find = cache.find(n);
      46         [ +  + ]:        650 :     if (find != cache.end())
      47                 :            :     {
      48                 :        462 :       return (*find).second;
      49                 :            :     }
      50                 :            :   }
      51         [ -  + ]:        312 :   if (n.isClosure())
      52                 :            :   {
      53                 :            :     // don't traverse quantified formulas
      54                 :          0 :     return n;
      55                 :            :   }
      56                 :        312 :   Node ret = n;
      57         [ +  + ]:        312 :   if (n.getNumChildren() > 0)
      58                 :            :   {
      59 [ +  + ][ +  - ]:        238 :     if (beneathMult && (n.getKind() == Kind::ADD || n.getKind() == Kind::SUB))
         [ -  + ][ -  + ]
      60                 :            :     {
      61                 :            :       // don't do it if it rewrites to a constant
      62                 :          0 :       Node nr = rewrite(n);
      63         [ -  - ]:          0 :       if (nr.isConst())
      64                 :            :       {
      65                 :            :         // return the rewritten constant
      66                 :          0 :         ret = nr;
      67                 :            :       }
      68                 :            :       else
      69                 :            :       {
      70                 :            :         // new variable
      71                 :          0 :         ret = NodeManager::mkDummySkolem("__purifyNl_var", n.getType());
      72                 :          0 :         Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
      73                 :          0 :         var_eq.push_back(np.eqNode(ret));
      74         [ -  - ]:          0 :         Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
      75                 :          0 :                                << std::endl;
      76                 :          0 :       }
      77                 :          0 :     }
      78                 :            :     else
      79                 :            :     {
      80 [ +  + ][ +  + ]:        238 :       bool beneathMultNew = beneathMult || n.getKind() == Kind::MULT;
      81                 :        238 :       bool childChanged = false;
      82                 :        238 :       std::vector<Node> children;
      83         [ +  + ]:       2832 :       for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
      84                 :            :       {
      85                 :       2594 :         Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew);
      86 [ +  - ][ -  + ]:       2594 :         childChanged = childChanged || nc != n[i];
         [ +  - ][ -  - ]
      87                 :       2594 :         children.push_back(nc);
      88                 :       2594 :       }
      89         [ -  + ]:        238 :       if (childChanged)
      90                 :            :       {
      91                 :          0 :         ret = nm->mkNode(n.getKind(), children);
      92                 :            :       }
      93                 :        238 :     }
      94                 :            :   }
      95         [ +  + ]:        312 :   if (beneathMult)
      96                 :            :   {
      97                 :        124 :     bcache[n] = ret;
      98                 :            :   }
      99                 :            :   else
     100                 :            :   {
     101                 :        188 :     cache[n] = ret;
     102                 :            :   }
     103                 :        312 :   return ret;
     104                 :        312 : }
     105                 :            : 
     106                 :      50669 : NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext)
     107                 :      50669 :     : PreprocessingPass(preprocContext, "nl-ext-purify"){};
     108                 :            : 
     109                 :         10 : PreprocessingPassResult NlExtPurify::applyInternal(
     110                 :            :     AssertionPipeline* assertionsToPreprocess)
     111                 :            : {
     112                 :         10 :   unordered_map<Node, Node> cache;
     113                 :         10 :   unordered_map<Node, Node> bcache;
     114                 :         10 :   std::vector<Node> var_eq;
     115                 :         10 :   unsigned size = assertionsToPreprocess->size();
     116         [ +  + ]:        360 :   for (unsigned i = 0; i < size; ++i)
     117                 :            :   {
     118                 :        350 :     Node a = (*assertionsToPreprocess)[i];
     119                 :        350 :     Node ap = purifyNlTerms(a, cache, bcache, var_eq);
     120         [ -  + ]:        350 :     if (a != ap)
     121                 :            :     {
     122                 :          0 :       assertionsToPreprocess->replace(
     123                 :            :           i, ap, nullptr, TrustId::PREPROCESS_NL_EXT_PURIFY);
     124         [ -  - ]:          0 :       Trace("nl-ext-purify")
     125                 :          0 :           << "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n";
     126                 :            :     }
     127                 :        350 :   }
     128         [ -  + ]:         10 :   if (!var_eq.empty())
     129                 :            :   {
     130         [ -  - ]:          0 :     for (const Node& ve : var_eq)
     131                 :            :     {
     132                 :          0 :       assertionsToPreprocess->push_back(
     133                 :            :           ve, false, nullptr, TrustId::PREPROCESS_NL_EXT_PURIFY_LEMMA);
     134                 :            :     }
     135                 :            :   }
     136                 :         10 :   return PreprocessingPassResult::NO_CONFLICT;
     137                 :         10 : }
     138                 :            : 
     139                 :            : 
     140                 :            : }  // namespace passes
     141                 :            : }  // namespace preprocessing
     142                 :            : }  // namespace cvc5::internal