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 distinct_elim preprocessing pass.
      11                 :            :  *
      12                 :            :  * Eagerly eliminates (blasts) distinct terms into pairwise disequalities,
      13                 :            :  * based on a configurable threshold on the number of children.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "preprocessing/passes/distinct_elim.h"
      17                 :            : 
      18                 :            : #include "options/smt_options.h"
      19                 :            : #include "preprocessing/assertion_pipeline.h"
      20                 :            : #include "theory/uf/theory_uf_rewriter.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace preprocessing {
      24                 :            : namespace passes {
      25                 :            : 
      26                 :      28895 : DistinctElim::DistinctElim(PreprocessingPassContext* preprocContext)
      27                 :            :     : PreprocessingPass(preprocContext, "distinct-elim"),
      28                 :      28895 :       d_threshold(options().smt.distinctElimThreshold)
      29                 :            : {
      30         [ +  + ]:      28895 :   if (options().smt.produceProofs)
      31                 :            :   {
      32                 :      30750 :     d_tpg.reset(new TConvProofGenerator(d_env,
      33                 :      15375 :                                         userContext(),
      34                 :            :                                         TConvPolicy::FIXPOINT,
      35                 :            :                                         TConvCachePolicy::NEVER,
      36                 :      15375 :                                         "DistinctElim::tpg"));
      37                 :            :   }
      38                 :      28895 : }
      39                 :            : 
      40                 :         12 : PreprocessingPassResult DistinctElim::applyInternal(
      41                 :            :     AssertionPipeline* assertionsToPreprocess)
      42                 :            : {
      43         [ +  + ]:         48 :   for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
      44                 :            :        ++i)
      45                 :            :   {
      46                 :         36 :     TrustNode trn = eliminate((*assertionsToPreprocess)[i]);
      47         [ +  + ]:         36 :     if (trn.isNull())
      48                 :            :     {
      49                 :         22 :       continue;
      50                 :            :     }
      51                 :         14 :     assertionsToPreprocess->replaceTrusted(i, trn);
      52         [ -  + ]:         14 :     if (assertionsToPreprocess->isInConflict())
      53                 :            :     {
      54                 :          0 :       return PreprocessingPassResult::CONFLICT;
      55                 :            :     }
      56    [ +  + ][ - ]:         36 :   }
      57                 :         12 :   return PreprocessingPassResult::NO_CONFLICT;
      58                 :            : }
      59                 :            : 
      60                 :         36 : TrustNode DistinctElim::eliminate(TNode n)
      61                 :            : {
      62                 :         36 :   NodeManager* nm = nodeManager();
      63                 :         36 :   std::unordered_map<TNode, Node> visited;
      64                 :         36 :   std::unordered_map<TNode, Node>::iterator it;
      65                 :            :   // to ensure all intermediate nodes are ref counted
      66                 :         36 :   std::unordered_set<Node> keep;
      67                 :         36 :   std::vector<TNode> visit;
      68                 :         36 :   visit.push_back(n);
      69                 :            :   do
      70                 :            :   {
      71                 :        560 :     TNode cur = visit.back();
      72                 :        560 :     it = visited.find(cur);
      73         [ +  + ]:        560 :     if (it == visited.end())
      74                 :            :     {
      75                 :        280 :       visited[cur] = Node::null();
      76                 :        280 :       visit.insert(visit.end(), cur.begin(), cur.end());
      77                 :            :     }
      78         [ +  - ]:        280 :     else if (it->second.isNull())
      79                 :            :     {
      80                 :            :       // reconstruct with processed children
      81                 :        280 :       Node ret = cur;
      82                 :        280 :       bool childChanged = false;
      83                 :        280 :       std::vector<Node> children;
      84         [ -  + ]:        280 :       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      85                 :            :       {
      86                 :          0 :         children.push_back(cur.getOperator());
      87                 :            :       }
      88         [ +  + ]:        524 :       for (const Node& cn : cur)
      89                 :            :       {
      90 [ -  + ][ -  + ]:        244 :         Assert(visited.find(cn) != visited.end());
                 [ -  - ]
      91 [ -  + ][ -  + ]:        244 :         Assert(!visited[cn].isNull());
                 [ -  - ]
      92 [ +  - ][ -  + ]:        244 :         childChanged = childChanged || cn != visited[cn];
         [ +  - ][ -  - ]
      93                 :        244 :         children.push_back(visited[cn]);
      94                 :        244 :       }
      95         [ -  + ]:        280 :       if (childChanged)
      96                 :            :       {
      97                 :          0 :         ret = nm->mkNode(cur.getKind(), children);
      98                 :          0 :         keep.insert(ret);
      99                 :            :       }
     100                 :            :       // blast distinct if it is within the threshold (0 means no limit)
     101                 :        280 :       if (ret.getKind() == Kind::DISTINCT
     102 [ +  + ][ +  + ]:        280 :           && (d_threshold == 0 || ret.getNumChildren() <= d_threshold))
         [ +  + ][ +  + ]
     103                 :            :       {
     104                 :         14 :         Node blasted = theory::uf::TheoryUfRewriter::blastDistinct(nm, ret);
     105                 :         14 :         keep.insert(blasted);
     106         [ +  + ]:         14 :         if (d_tpg != nullptr)
     107                 :            :         {
     108                 :            :           // justify (= ret blasted) via the DISTINCT_ELIM proof rewrite rule
     109                 :          8 :           d_tpg->addTheoryRewriteStep(
     110                 :            :               ret, blasted, ProofRewriteRule::DISTINCT_ELIM);
     111                 :            :         }
     112                 :         14 :         ret = blasted;
     113                 :         14 :       }
     114                 :        280 :       visited[cur] = ret;
     115                 :        280 :       visit.pop_back();
     116                 :        280 :     }
     117                 :            :     else
     118                 :            :     {
     119                 :          0 :       visit.pop_back();
     120                 :            :     }
     121         [ +  + ]:        560 :   } while (!visit.empty());
     122 [ -  + ][ -  + ]:         36 :   Assert(visited.find(n) != visited.end());
                 [ -  - ]
     123 [ -  + ][ -  + ]:         36 :   Assert(!visited.find(n)->second.isNull());
                 [ -  - ]
     124                 :         36 :   Node ret = visited[n];
     125         [ +  + ]:         36 :   if (ret == n)
     126                 :            :   {
     127                 :         22 :     return TrustNode::null();
     128                 :            :   }
     129                 :            :   // use the term conversion proof generator if it exists
     130         [ +  + ]:         14 :   return TrustNode::mkTrustRewrite(n, ret, d_tpg.get());
     131                 :         36 : }
     132                 :            : 
     133                 :            : }  // namespace passes
     134                 :            : }  // namespace preprocessing
     135                 :            : }  // namespace cvc5::internal