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                 :            :  * Implementation of non-closed node conversion
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "expr/non_closed_node_converter.h"
      14                 :            : 
      15                 :            : #include "expr/array_store_all.h"
      16                 :            : #include "expr/node_algorithm.h"
      17                 :            : #include "expr/skolem_manager.h"
      18                 :            : #include "options/arrays_options.h"
      19                 :            : #include "smt/env.h"
      20                 :            : #include "theory/strings/theory_strings_utils.h"
      21                 :            : #include "theory/uf/function_const.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :         41 : NonClosedNodeConverter::NonClosedNodeConverter(Env& env)
      26                 :         41 :     : EnvObj(env), NodeConverter(nodeManager())
      27                 :            : {
      28                 :         41 :   getNonClosedKinds(env, d_nonClosedKinds);
      29                 :         41 : }
      30                 :            : 
      31                 :         41 : NonClosedNodeConverter::~NonClosedNodeConverter() {}
      32                 :            : 
      33                 :        412 : Node NonClosedNodeConverter::postConvert(Node n)
      34                 :            : {
      35         [ +  - ]:        412 :   Trace("non-closed-debug") << "postConvert: " << n << std::endl;
      36                 :        412 :   Kind k = n.getKind();
      37                 :        412 :   bool purify = false;
      38         [ +  + ]:        412 :   if (d_nonClosedKinds.find(k) != d_nonClosedKinds.end())
      39                 :            :   {
      40                 :         29 :     purify = true;
      41                 :            :   }
      42         [ -  + ]:        383 :   else if (k == Kind::STORE_ALL)
      43                 :            :   {
      44                 :            :     // Store all hides its element. if this is not closed, then this entire
      45                 :            :     // term must be purified.
      46                 :          0 :     Node nval = n.getConst<ArrayStoreAll>().getValue();
      47                 :          0 :     Node nvalc = convert(nval);
      48         [ -  - ]:          0 :     if (nvalc != nval)
      49                 :            :     {
      50                 :          0 :       purify = true;
      51                 :            :     }
      52                 :          0 :   }
      53                 :            :   else
      54                 :            :   {
      55                 :            :     // node that can "hide" constants, we must convert these to their expanded
      56                 :            :     // form and see if they convert
      57                 :        383 :     Node nc;
      58         [ +  + ]:        383 :     if (k == Kind::CONST_SEQUENCE)
      59                 :            :     {
      60                 :         15 :       nc = theory::strings::utils::mkConcatForConstSequence(n);
      61                 :            :     }
      62         [ +  + ]:        368 :     else if (k == Kind::FUNCTION_ARRAY_CONST)
      63                 :            :     {
      64                 :          3 :       nc = theory::uf::FunctionConst::toLambda(n);
      65                 :            :     }
      66 [ +  + ][ +  + ]:        383 :     if (!nc.isNull() && nc != n)
                 [ +  + ]
      67                 :            :     {
      68                 :          9 :       Node nnc = convert(nc);
      69         [ +  + ]:          9 :       if (nnc != nc)
      70                 :            :       {
      71                 :          1 :         return nnc;
      72                 :            :       }
      73         [ +  + ]:          9 :     }
      74         [ +  + ]:        383 :   }
      75         [ +  + ]:        411 :   if (purify)
      76                 :            :   {
      77                 :         29 :     Node sk = SkolemManager::mkPurifySkolem(n);
      78                 :         29 :     d_purifySkolems.push_back(sk);
      79                 :         29 :     return sk;
      80                 :         29 :   }
      81                 :        382 :   return n;
      82                 :            : }
      83                 :            : 
      84                 :        148 : bool NonClosedNodeConverter::isClosed(Env& env, const Node& n)
      85                 :            : {
      86                 :        148 :   std::unordered_set<Kind, kind::KindHashFunction> ncks;
      87                 :        148 :   getNonClosedKinds(env, ncks);
      88                 :            :   // additional kinds that *might* be non-closed
      89                 :        148 :   ncks.insert(Kind::STORE_ALL);
      90                 :        148 :   ncks.insert(Kind::CONST_SEQUENCE);
      91                 :        148 :   ncks.insert(Kind::FUNCTION_ARRAY_CONST);
      92                 :            :   // most of the time, this will return true
      93         [ +  + ]:        148 :   if (!expr::hasSubtermKinds(ncks, n))
      94                 :            :   {
      95                 :        107 :     return true;
      96                 :            :   }
      97                 :            :   // otherwise see if it converts, if it doesn't then it is closed
      98                 :         41 :   NonClosedNodeConverter ncnc(env);
      99                 :         41 :   Node nc = ncnc.convert(n);
     100                 :         41 :   return nc == n;
     101                 :        148 : }
     102                 :            : 
     103                 :        189 : void NonClosedNodeConverter::getNonClosedKinds(
     104                 :            :     const Env& env, std::unordered_set<Kind, kind::KindHashFunction>& ncks)
     105                 :            : {
     106                 :            :   // some kinds may appear in model values that cannot be asserted
     107         [ +  - ]:        189 :   if (!env.getOptions().arrays.arraysExp)
     108                 :            :   {
     109                 :        189 :     ncks.insert(Kind::STORE_ALL);
     110                 :            :   }
     111                 :        189 :   ncks.insert(Kind::CODATATYPE_BOUND_VARIABLE);
     112                 :        189 :   ncks.insert(Kind::UNINTERPRETED_SORT_VALUE);
     113                 :            :   // may appear in certain models e.g. strings of excessive length
     114                 :        189 :   ncks.insert(Kind::WITNESS);
     115                 :        189 :   ncks.insert(Kind::REAL_ALGEBRAIC_NUMBER);
     116                 :        189 : }
     117                 :            : 
     118                 :          0 : const std::vector<Node>& NonClosedNodeConverter::getSkolems() const
     119                 :            : {
     120                 :          0 :   return d_purifySkolems;
     121                 :            : }
     122                 :            : 
     123                 :            : }  // namespace cvc5::internal