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")
      48                 :          3 :         << "Pre-skolem emp " << n << " with pol " << pol << 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 [ +  + ][ -  - ]:          5 :             ->mkNode(Kind::SEP_STAR,
      58                 :          3 :                      {nm->mkNode(Kind::SEP_PTO, x, y), nm->mkConst(true)})
      59                 :          1 :             .negate();
      60                 :          1 :       }
      61                 :            :     }
      62 [ +  - ][ +  + ]:          2 :     else if (n.getKind() != Kind::FORALL && n.getNumChildren() > 0)
                 [ +  + ]
      63                 :            :     {
      64                 :          1 :       std::vector<Node> children;
      65                 :          1 :       bool childChanged = false;
      66         [ -  + ]:          1 :       if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
      67                 :            :       {
      68                 :          0 :         children.push_back(n.getOperator());
      69                 :            :       }
      70         [ +  + ]:          2 :       for (unsigned i = 0; i < n.getNumChildren(); i++)
      71                 :            :       {
      72                 :            :         bool newPol, newHasPol;
      73                 :          1 :         QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol);
      74                 :          1 :         Node nc = n[i];
      75         [ +  - ]:          1 :         if (newHasPol)
      76                 :            :         {
      77                 :          1 :           nc = preSkolemEmp(nm, locType, dataType, n[i], newPol, visited);
      78 [ +  - ][ +  - ]:          1 :           childChanged = childChanged || nc != n[i];
         [ +  - ][ -  - ]
      79                 :            :         }
      80                 :          1 :         children.push_back(nc);
      81                 :          1 :       }
      82         [ +  - ]:          1 :       if (childChanged)
      83                 :            :       {
      84                 :          1 :         return nm->mkNode(n.getKind(), children);
      85                 :            :       }
      86         [ -  + ]:          1 :     }
      87                 :          1 :     visited[pol][n] = ret;
      88                 :          1 :     return n;
      89                 :          3 :   }
      90                 :            :   else
      91                 :            :   {
      92                 :          0 :     return it->second;
      93                 :            :   }
      94                 :            : }
      95                 :            : 
      96                 :            : }  // namespace
      97                 :            : 
      98                 :      28895 : SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
      99                 :      28895 :     : PreprocessingPass(preprocContext, "sep-skolem-emp") {};
     100                 :            : 
     101                 :          2 : PreprocessingPassResult SepSkolemEmp::applyInternal(
     102                 :            :     AssertionPipeline* assertionsToPreprocess)
     103                 :            : {
     104         [ +  + ]:          2 :   if (!d_env.hasSepHeap())
     105                 :            :   {
     106                 :          1 :     warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
     107                 :          1 :                  "heap types during preprocessing"
     108                 :          1 :               << std::endl;
     109                 :          1 :     return PreprocessingPassResult::NO_CONFLICT;
     110                 :            :   }
     111                 :          1 :   TypeNode locType = d_env.getSepLocType();
     112                 :          1 :   TypeNode dataType = d_env.getSepDataType();
     113                 :          1 :   std::map<bool, std::map<Node, Node>> visited;
     114         [ +  + ]:          3 :   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
     115                 :            :   {
     116                 :          2 :     Node prev = (*assertionsToPreprocess)[i];
     117                 :          2 :     bool pol = true;
     118                 :            :     Node next =
     119                 :          4 :         preSkolemEmp(nodeManager(), locType, dataType, prev, pol, visited);
     120         [ +  + ]:          2 :     if (next != prev)
     121                 :            :     {
     122                 :          1 :       assertionsToPreprocess->replace(i, rewrite(next));
     123         [ +  - ]:          1 :       Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
     124         [ +  - ]:          2 :       Trace("sep-preprocess")
     125                 :          1 :           << "   ...got " << (*assertionsToPreprocess)[i] << endl;
     126                 :            :     }
     127                 :          2 :     visited.clear();
     128                 :          2 :   }
     129                 :          1 :   return PreprocessingPassResult::NO_CONFLICT;
     130                 :          1 : }
     131                 :            : 
     132                 :            : }  // namespace passes
     133                 :            : }  // namespace preprocessing
     134                 :            : }  // namespace cvc5::internal