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(TypeNode locType,
      41                 :            :                   TypeNode dataType,
      42                 :            :                   Node n,
      43                 :            :                   bool pol,
      44                 :            :                   std::map<bool, std::map<Node, Node>>& visited)
      45                 :            : {
      46                 :          3 :   std::map<Node, Node>::iterator it = visited[pol].find(n);
      47         [ +  - ]:          3 :   if (it == visited[pol].end())
      48                 :            :   {
      49                 :          3 :     NodeManager* nm = NodeManager::currentNM();
      50                 :          3 :     SkolemManager* sm = nm->getSkolemManager();
      51         [ +  - ]:          6 :     Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
      52                 :          3 :                             << std::endl;
      53                 :          6 :     Node ret = n;
      54         [ +  + ]:          3 :     if (n.getKind() == Kind::SEP_EMP)
      55                 :            :     {
      56         [ +  - ]:          1 :       if (!pol)
      57                 :            :       {
      58                 :            :         Node x =
      59                 :          3 :             sm->mkDummySkolem("ex", locType, "skolem location for negated emp");
      60                 :            :         Node y =
      61                 :          2 :             sm->mkDummySkolem("ey", dataType, "skolem data for negated emp");
      62                 :            :         return nm
      63                 :          3 :             ->mkNode(Kind::SEP_STAR,
      64                 :          2 :                      nm->mkNode(Kind::SEP_PTO, x, y),
      65                 :          2 :                      nm->mkConst(true))
      66                 :          1 :             .negate();
      67                 :            :       }
      68                 :            :     }
      69 [ +  - ][ +  + ]:          2 :     else if (n.getKind() != Kind::FORALL && n.getNumChildren() > 0)
                 [ +  + ]
      70                 :            :     {
      71                 :          1 :       std::vector<Node> children;
      72                 :          1 :       bool childChanged = false;
      73         [ -  + ]:          1 :       if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
      74                 :            :       {
      75                 :          0 :         children.push_back(n.getOperator());
      76                 :            :       }
      77         [ +  + ]:          2 :       for (unsigned i = 0; i < n.getNumChildren(); i++)
      78                 :            :       {
      79                 :            :         bool newPol, newHasPol;
      80                 :          1 :         QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol);
      81                 :          2 :         Node nc = n[i];
      82         [ +  - ]:          1 :         if (newHasPol)
      83                 :            :         {
      84                 :          1 :           nc = preSkolemEmp(locType, dataType, n[i], newPol, visited);
      85 [ +  - ][ +  - ]:          1 :           childChanged = childChanged || nc != n[i];
         [ +  - ][ -  - ]
      86                 :            :         }
      87                 :          1 :         children.push_back(nc);
      88                 :            :       }
      89         [ +  - ]:          1 :       if (childChanged)
      90                 :            :       {
      91                 :          1 :         return nm->mkNode(n.getKind(), children);
      92                 :            :       }
      93                 :            :     }
      94                 :          1 :     visited[pol][n] = ret;
      95                 :          1 :     return n;
      96                 :            :   }
      97                 :            :   else
      98                 :            :   {
      99                 :          0 :     return it->second;
     100                 :            :   }
     101                 :            : }
     102                 :            : 
     103                 :            : }  // namespace
     104                 :            : 
     105                 :      48195 : SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
     106                 :      48195 :     : PreprocessingPass(preprocContext, "sep-skolem-emp"){};
     107                 :            : 
     108                 :          2 : PreprocessingPassResult SepSkolemEmp::applyInternal(
     109                 :            :     AssertionPipeline* assertionsToPreprocess)
     110                 :            : {
     111         [ +  + ]:          2 :   if (!d_env.hasSepHeap())
     112                 :            :   {
     113                 :          1 :     warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
     114                 :          1 :                  "heap types during preprocessing"
     115                 :          1 :               << std::endl;
     116                 :          1 :     return PreprocessingPassResult::NO_CONFLICT;
     117                 :            :   }
     118                 :          2 :   TypeNode locType = d_env.getSepLocType();
     119                 :          2 :   TypeNode dataType = d_env.getSepDataType();
     120                 :          1 :   std::map<bool, std::map<Node, Node>> visited;
     121         [ +  + ]:          3 :   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
     122                 :            :   {
     123                 :          4 :     Node prev = (*assertionsToPreprocess)[i];
     124                 :          2 :     bool pol = true;
     125                 :          6 :     Node next = preSkolemEmp(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