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