Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Daniel Larraz
       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                 :            :  * sygus_term_enumerator
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "expr/sygus_term_enumerator.h"
      17                 :            : 
      18                 :            : #include "expr/skolem_manager.h"
      19                 :            : #include "theory/datatypes/sygus_datatype_utils.h"
      20                 :            : #include "theory/quantifiers/sygus/sygus_enumerator.h"
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : 
      24                 :        142 : SygusTermEnumerator::SygusTermEnumerator(Env& env,
      25                 :            :                                          const TypeNode& tn,
      26                 :            :                                          SygusTermEnumeratorCallback* sec,
      27                 :            :                                          bool enumShapes,
      28                 :            :                                          bool enumAnyConstHoles,
      29                 :        142 :                                          size_t numConstants)
      30                 :            :     : d_internal(new theory::quantifiers::SygusEnumerator(env,
      31                 :            :                                                           nullptr,
      32                 :            :                                                           sec,
      33                 :            :                                                           nullptr,
      34                 :            :                                                           enumShapes,
      35                 :            :                                                           enumAnyConstHoles,
      36                 :        142 :                                                           numConstants))
      37                 :            : {
      38                 :            :   // Ensure we have computed the expanded definition form of all operators in
      39                 :            :   // grammar, which is important if the grammar involves terms that have
      40                 :            :   // user definitions in env.
      41                 :        142 :   theory::datatypes::utils::computeExpandedDefinitionForms(env, tn);
      42                 :        142 :   d_enum = NodeManager::mkDummySkolem("enum", tn);
      43                 :        142 :   d_internal->initialize(d_enum);
      44                 :            :   // ensure current is non-null
      45         [ +  + ]:        142 :   if (d_internal->getCurrent().isNull())
      46                 :            :   {
      47         [ -  + ]:          4 :     if (!increment())
      48                 :            :     {
      49         [ -  - ]:          0 :       Warning() << "Could not initialize enumeration for " << tn
      50                 :          0 :                 << ", no values found";
      51                 :            :     }
      52                 :            :   }
      53                 :        142 : }
      54                 :            : 
      55                 :       5555 : bool SygusTermEnumerator::increment()
      56                 :            : {
      57         [ +  + ]:       5555 :   while (d_internal->increment())
      58                 :            :   {
      59         [ +  + ]:       5528 :     if (!d_internal->getCurrent().isNull())
      60                 :            :     {
      61                 :       1647 :       return true;
      62                 :            :     }
      63                 :            :   }
      64                 :         27 :   return false;
      65                 :            : }
      66                 :            : 
      67                 :       6846 : bool SygusTermEnumerator::incrementPartial() { return d_internal->increment(); }
      68                 :            : 
      69                 :       8551 : Node SygusTermEnumerator::getCurrent()
      70                 :            : {
      71                 :      17102 :   const Node& c = d_internal->getCurrent();
      72         [ +  + ]:       8551 :   if (c.isNull())
      73                 :            :   {
      74                 :       4825 :     return c;
      75                 :            :   }
      76                 :       3726 :   return theory::datatypes::utils::sygusToBuiltin(c);
      77                 :            : }
      78                 :            : 
      79                 :            : }  // namespace cvc5::internal