Branch data     Line data    Source code

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