Branch data     Line data    Source code

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