Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz
       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                 :            :  * Synthesis finder
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/sygus/synth_finder.h"
      17                 :            : 
      18                 :            : #include "expr/sygus_term_enumerator.h"
      19                 :            : #include "options/base_options.h"
      20                 :            : #include "options/quantifiers_options.h"
      21                 :            : #include "printer/printer.h"
      22                 :            : #include "smt/env.h"
      23                 :            : #include "theory/datatypes/sygus_datatype_utils.h"
      24                 :            : #include "theory/quantifiers/candidate_rewrite_database.h"
      25                 :            : #include "theory/quantifiers/query_generator_sample_sat.h"
      26                 :            : #include "theory/quantifiers/query_generator_unsat.h"
      27                 :            : #include "theory/quantifiers/rewrite_verifier.h"
      28                 :            : #include "theory/quantifiers/sygus/print_sygus_to_builtin.h"
      29                 :            : #include "theory/quantifiers/sygus/sygus_enumerator.h"
      30                 :            : #include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
      31                 :            : #include "theory/quantifiers/sygus_sampler.h"
      32                 :            : 
      33                 :            : namespace cvc5::internal {
      34                 :            : namespace theory {
      35                 :            : namespace quantifiers {
      36                 :            : 
      37                 :         93 : SynthFinder::SynthFinder(Env& env) : EnvObj(env), d_current(nullptr) {}
      38                 :            : 
      39                 :         93 : void SynthFinder::initialize(modes::FindSynthTarget fst, const TypeNode& gtn)
      40                 :            : {
      41                 :            :   // should be a sygus datatype
      42 [ +  - ][ +  - ]:        186 :   Assert(!gtn.isNull() && gtn.isDatatype() && gtn.getDType().isSygus());
         [ +  - ][ -  + ]
                 [ -  - ]
      43                 :         93 :   d_fst = fst;
      44                 :         93 :   d_fstu = fst;
      45                 :            :   // rewrites from input use the same algorithm
      46         [ +  + ]:         93 :   if (d_fstu == modes::FindSynthTarget::REWRITE_INPUT)
      47                 :            :   {
      48                 :         27 :     d_fstu = modes::FindSynthTarget::REWRITE;
      49                 :            :   }
      50                 :            : 
      51                 :            :   // clear the buffer
      52                 :         93 :   d_bufferIndex = 0;
      53                 :         93 :   d_buffer.clear();
      54                 :            : 
      55                 :            :   // initialize the enumerator with the given callback, which also will ensure
      56                 :            :   // that expanded definition forms are set on gtn.
      57                 :         93 :   d_enum.reset(new SygusTermEnumerator(d_env, gtn, d_ecb.get()));
      58                 :            : 
      59                 :            :   // initialize the expression miner
      60                 :         93 :   initializeInternal(d_fstu, gtn);
      61                 :         93 : }
      62                 :            : 
      63                 :       1677 : bool SynthFinder::increment()
      64                 :            : {
      65 [ -  + ][ -  + ]:       1677 :   Assert(d_enum != nullptr);
                 [ -  - ]
      66                 :       1677 :   return d_enum->increment();
      67                 :            : }
      68                 :            : 
      69                 :       1677 : Node SynthFinder::getCurrent()
      70                 :            : {
      71 [ -  + ][ -  + ]:       1677 :   Assert(d_enum != nullptr);
                 [ -  - ]
      72                 :       3354 :   Node curr = d_enum->getCurrent();
      73         [ -  + ]:       1677 :   if (curr.isNull())
      74                 :            :   {
      75                 :            :     // enumerator does not yet have a term
      76                 :          0 :     return curr;
      77                 :            :   }
      78                 :       1677 :   return runNext(curr, d_fstu);
      79                 :            : }
      80                 :            : 
      81                 :            : /**
      82                 :            :  * A callback that does not do symmetry breaking based on rewriting.
      83                 :            :  */
      84                 :            : class SygusEnumeratorCallbackNoSym : public SygusEnumeratorCallback
      85                 :            : {
      86                 :            :  public:
      87                 :         12 :   SygusEnumeratorCallbackNoSym(Env& env) : SygusEnumeratorCallback(env) {}
      88                 :            : 
      89                 :            :  protected:
      90                 :            :   /**
      91                 :            :    * Get the cache value for the given candidate, which returns bn itself,
      92                 :            :    * without invoking the rewriter.
      93                 :            :    */
      94                 :          0 :   Node getCacheValue(const Node& n, const Node& bn) override { return bn; }
      95                 :            : };
      96                 :            : 
      97                 :         93 : void SynthFinder::initializeInternal(modes::FindSynthTarget fst,
      98                 :            :                                      const TypeNode& gtn)
      99                 :            : {
     100                 :         93 :   options::SygusQueryGenMode qmode = options().quantifiers.sygusQueryGen;
     101                 :            : 
     102                 :            :   // get the sygus variables from the type of the enumerator
     103 [ -  + ][ -  + ]:         93 :   Assert(gtn.isDatatype());
                 [ -  - ]
     104                 :         93 :   const DType& dt = gtn.getDType();
     105 [ -  + ][ -  + ]:         93 :   Assert(dt.isSygus());
                 [ -  - ]
     106                 :        186 :   Node vlist = dt.getSygusVarList();
     107                 :        186 :   std::vector<Node> vars;
     108         [ +  + ]:         93 :   if (!vlist.isNull())
     109                 :            :   {
     110         [ +  + ]:        360 :     for (const Node& sv : vlist)
     111                 :            :     {
     112                 :        303 :       vars.push_back(sv);
     113                 :            :     }
     114                 :            :   }
     115                 :            : 
     116                 :            :   // initialize the sampler if necessary
     117                 :         93 :   bool needsSampler = false;
     118                 :         93 :   size_t nsamples = options().quantifiers.sygusSamples;
     119         [ +  + ]:         93 :   if (fst == modes::FindSynthTarget::REWRITE
     120         [ +  + ]:         54 :       || fst == modes::FindSynthTarget::REWRITE_UNSOUND)
     121                 :            :   {
     122                 :         51 :     needsSampler = true;
     123                 :            :   }
     124         [ +  + ]:         42 :   else if (fst == modes::FindSynthTarget::QUERY)
     125                 :            :   {
     126                 :          6 :     needsSampler = (qmode == options::SygusQueryGenMode::SAMPLE_SAT);
     127                 :            :   }
     128                 :         93 :   d_sampler = nullptr;
     129         [ +  + ]:         93 :   if (needsSampler)
     130                 :            :   {
     131                 :         53 :     d_sampler.reset(new SygusSampler(d_env));
     132                 :         53 :     d_sampler->initializeSygus(gtn, nsamples);
     133                 :            :   }
     134                 :            : 
     135                 :            :   // initialize the sygus enumerator callback if necessary
     136                 :         93 :   d_ecb = nullptr;
     137         [ +  + ]:         93 :   if (fst == modes::FindSynthTarget::REWRITE_UNSOUND)
     138                 :            :   {
     139                 :         12 :     d_ecb.reset(new SygusEnumeratorCallbackNoSym(d_env));
     140                 :            :   }
     141                 :            : 
     142                 :            :   // now, setup the handlers
     143         [ +  + ]:         93 :   if (fst == modes::FindSynthTarget::ENUM)
     144                 :            :   {
     145                 :         36 :     d_eid.reset(new ExprMinerId(d_env));
     146                 :         36 :     d_current = d_eid.get();
     147                 :            :   }
     148         [ +  + ]:         57 :   else if (fst == modes::FindSynthTarget::REWRITE)
     149                 :            :   {
     150                 :         39 :     d_crd.reset(
     151                 :            :         new CandidateRewriteDatabase(d_env,
     152                 :         39 :                                      options().quantifiers.sygusRewSynthCheck,
     153                 :            :                                      false,
     154                 :            :                                      true,
     155                 :         39 :                                      options().quantifiers.sygusRewSynthRec));
     156                 :         39 :     d_current = d_crd.get();
     157                 :            :   }
     158         [ +  + ]:         18 :   else if (fst == modes::FindSynthTarget::REWRITE_UNSOUND)
     159                 :            :   {
     160                 :         12 :     d_rrv.reset(new RewriteVerifier(d_env));
     161                 :         12 :     d_current = d_rrv.get();
     162                 :            :   }
     163         [ +  - ]:          6 :   else if (fst == modes::FindSynthTarget::QUERY)
     164                 :            :   {
     165         [ +  + ]:          6 :     if (qmode == options::SygusQueryGenMode::SAMPLE_SAT)
     166                 :            :     {
     167                 :          2 :       size_t deqThresh = options().quantifiers.sygusQueryGenThresh;
     168                 :          2 :       d_qg = std::make_unique<QueryGeneratorSampleSat>(d_env, deqThresh);
     169                 :            :     }
     170         [ +  + ]:          4 :     else if (qmode == options::SygusQueryGenMode::UNSAT)
     171                 :            :     {
     172                 :          2 :       d_qg = std::make_unique<QueryGeneratorUnsat>(d_env);
     173                 :            :     }
     174         [ +  - ]:          2 :     else if (qmode == options::SygusQueryGenMode::BASIC)
     175                 :            :     {
     176                 :          2 :       d_qg = std::make_unique<QueryGeneratorBasic>(d_env);
     177                 :            :     }
     178                 :            :     else
     179                 :            :     {
     180                 :          0 :       Unhandled() << "Unknown query generation mode " << qmode;
     181                 :            :     }
     182                 :          6 :     d_current = d_qg.get();
     183                 :            :   }
     184                 :            :   else
     185                 :            :   {
     186                 :          0 :     Unhandled() << "Unknown find synthesis target " << fst;
     187                 :            :   }
     188                 :            :   // initialize
     189         [ +  - ]:         93 :   if (d_current != nullptr)
     190                 :            :   {
     191                 :         93 :     d_current->initialize(vars, d_sampler.get());
     192                 :            :   }
     193                 :         93 : }
     194                 :            : 
     195                 :       1677 : Node SynthFinder::runNext(const Node& n, modes::FindSynthTarget fst)
     196                 :            : {
     197                 :            :   // if we already have a solution from a previous call that was buffered
     198         [ +  + ]:       1677 :   if (d_bufferIndex < d_buffer.size())
     199                 :            :   {
     200                 :       1500 :     Node ret = d_buffer[d_bufferIndex];
     201                 :        750 :     d_bufferIndex++;
     202                 :        750 :     return ret;
     203                 :            :   }
     204                 :        927 :   d_bufferIndex = 0;
     205                 :        927 :   d_buffer.clear();
     206                 :       1854 :   Node bn = datatypes::utils::sygusToBuiltin(n, true);
     207         [ +  - ]:        927 :   Trace("synth-finder") << "runNext " << d_fstu << " " << bn << std::endl;
     208                 :            :   // run the expression miner
     209 [ -  + ][ -  + ]:        927 :   Assert(d_current != nullptr);
                 [ -  - ]
     210                 :        927 :   d_current->addTerm(bn, d_buffer);
     211                 :            :   // return null if empty
     212         [ +  + ]:        927 :   if (d_buffer.empty())
     213                 :            :   {
     214                 :        368 :     return Node::null();
     215                 :            :   }
     216                 :            :   // ENUM is the only find synth target that makes sense to print grammar terms
     217                 :            :   // with; the others return terms that do not coincide with the enumerated
     218                 :            :   // term.
     219         [ +  + ]:        559 :   if (fst == modes::FindSynthTarget::ENUM)
     220                 :            :   {
     221         [ -  + ]:         52 :     if (isOutputOn(OutputTag::SYGUS_SOL_GTERM))
     222                 :            :     {
     223                 :          0 :       Node psol = getPrintableSygusToBuiltin(n);
     224                 :          0 :       d_env.output(OutputTag::SYGUS_SOL_GTERM)
     225                 :          0 :           << "(sygus-sol-gterm " << psol << " :" << fst << ")" << std::endl;
     226                 :            :     }
     227                 :            :   }
     228                 :        559 :   d_bufferIndex = 1;
     229                 :        559 :   return d_buffer[0];
     230                 :            : }
     231                 :            : 
     232                 :            : }  // namespace quantifiers
     233                 :            : }  // namespace theory
     234                 :            : }  // namespace cvc5::internal