Branch data     Line data    Source code

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