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 sep-pre-skolem-emp preprocessing pass.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "preprocessing/passes/sep_skolem_emp.h"
      14                 :            : 
      15                 :            : #include <string>
      16                 :            : #include <unordered_map>
      17                 :            : #include <vector>
      18                 :            : 
      19                 :            : #include "expr/node.h"
      20                 :            : #include "expr/skolem_manager.h"
      21                 :            : #include "preprocessing/assertion_pipeline.h"
      22                 :            : #include "preprocessing/preprocessing_pass_context.h"
      23                 :            : #include "theory/quantifiers/quant_util.h"
      24                 :            : #include "theory/rewriter.h"
      25                 :            : #include "theory/theory.h"
      26                 :            : #include "theory/theory_engine.h"
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace preprocessing {
      30                 :            : namespace passes {
      31                 :            : 
      32                 :            : using namespace std;
      33                 :            : using namespace cvc5::internal::theory;
      34                 :            : 
      35                 :            : namespace {
      36                 :            : 
      37                 :          3 : Node preSkolemEmp(NodeManager* nm,
      38                 :            :                   TypeNode locType,
      39                 :            :                   TypeNode dataType,
      40                 :            :                   Node n,
      41                 :            :                   bool pol,
      42                 :            :                   std::map<bool, std::map<Node, Node>>& visited)
      43                 :            : {
      44                 :          3 :   std::map<Node, Node>::iterator it = visited[pol].find(n);
      45         [ +  - ]:          3 :   if (it == visited[pol].end())
      46                 :            :   {
      47         [ +  - ]:          6 :     Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
      48                 :          3 :                             << std::endl;
      49                 :          3 :     Node ret = n;
      50         [ +  + ]:          3 :     if (n.getKind() == Kind::SEP_EMP)
      51                 :            :     {
      52         [ +  - ]:          1 :       if (!pol)
      53                 :            :       {
      54                 :          2 :         Node x = NodeManager::mkDummySkolem("ex", locType);
      55                 :          2 :         Node y = NodeManager::mkDummySkolem("ey", dataType);
      56                 :            :         return nm
      57                 :          3 :             ->mkNode(Kind::SEP_STAR,
      58                 :          2 :                      nm->mkNode(Kind::SEP_PTO, x, y),
      59                 :          2 :                      nm->mkConst(true))
      60                 :          1 :             .negate();
      61                 :          1 :       }
      62                 :            :     }
      63 [ +  - ][ +  + ]:          2 :     else if (n.getKind() != Kind::FORALL && n.getNumChildren() > 0)
                 [ +  + ]
      64                 :            :     {
      65                 :          1 :       std::vector<Node> children;
      66                 :          1 :       bool childChanged = false;
      67         [ -  + ]:          1 :       if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
      68                 :            :       {
      69                 :          0 :         children.push_back(n.getOperator());
      70                 :            :       }
      71         [ +  + ]:          2 :       for (unsigned i = 0; i < n.getNumChildren(); i++)
      72                 :            :       {
      73                 :            :         bool newPol, newHasPol;
      74                 :          1 :         QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol);
      75                 :          1 :         Node nc = n[i];
      76         [ +  - ]:          1 :         if (newHasPol)
      77                 :            :         {
      78                 :          1 :           nc = preSkolemEmp(nm, locType, dataType, n[i], newPol, visited);
      79 [ +  - ][ +  - ]:          1 :           childChanged = childChanged || nc != n[i];
         [ +  - ][ -  - ]
      80                 :            :         }
      81                 :          1 :         children.push_back(nc);
      82                 :          1 :       }
      83         [ +  - ]:          1 :       if (childChanged)
      84                 :            :       {
      85                 :          1 :         return nm->mkNode(n.getKind(), children);
      86                 :            :       }
      87         [ -  + ]:          1 :     }
      88                 :          1 :     visited[pol][n] = ret;
      89                 :          1 :     return n;
      90                 :          3 :   }
      91                 :            :   else
      92                 :            :   {
      93                 :          0 :     return it->second;
      94                 :            :   }
      95                 :            : }
      96                 :            : 
      97                 :            : }  // namespace
      98                 :            : 
      99                 :      50671 : SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
     100                 :      50671 :     : PreprocessingPass(preprocContext, "sep-skolem-emp"){};
     101                 :            : 
     102                 :          2 : PreprocessingPassResult SepSkolemEmp::applyInternal(
     103                 :            :     AssertionPipeline* assertionsToPreprocess)
     104                 :            : {
     105         [ +  + ]:          2 :   if (!d_env.hasSepHeap())
     106                 :            :   {
     107                 :          1 :     warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
     108                 :          1 :                  "heap types during preprocessing"
     109                 :          1 :               << std::endl;
     110                 :          1 :     return PreprocessingPassResult::NO_CONFLICT;
     111                 :            :   }
     112                 :          1 :   TypeNode locType = d_env.getSepLocType();
     113                 :          1 :   TypeNode dataType = d_env.getSepDataType();
     114                 :          1 :   std::map<bool, std::map<Node, Node>> visited;
     115         [ +  + ]:          3 :   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
     116                 :            :   {
     117                 :          2 :     Node prev = (*assertionsToPreprocess)[i];
     118                 :          2 :     bool pol = true;
     119                 :            :     Node next =
     120                 :          4 :         preSkolemEmp(nodeManager(), locType, dataType, prev, pol, visited);
     121         [ +  + ]:          2 :     if (next != prev)
     122                 :            :     {
     123                 :          1 :       assertionsToPreprocess->replace(i, rewrite(next));
     124         [ +  - ]:          1 :       Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
     125         [ +  - ]:          2 :       Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i]
     126                 :          1 :                               << endl;
     127                 :            :     }
     128                 :          2 :     visited.clear();
     129                 :          2 :   }
     130                 :          1 :   return PreprocessingPassResult::NO_CONFLICT;
     131                 :          1 : }
     132                 :            : 
     133                 :            : 
     134                 :            : }  // namespace passes
     135                 :            : }  // namespace preprocessing
     136                 :            : }  // namespace cvc5::internal