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 a class for mining interesting satisfiability
      11                 :            :  * queries from a stream of generated expressions.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "theory/quantifiers/query_generator.h"
      15                 :            : 
      16                 :            : #include <fstream>
      17                 :            : #include <sstream>
      18                 :            : 
      19                 :            : #include "options/quantifiers_options.h"
      20                 :            : #include "printer/printer.h"
      21                 :            : #include "smt/env.h"
      22                 :            : #include "smt/logic_exception.h"
      23                 :            : #include "smt/print_benchmark.h"
      24                 :            : 
      25                 :            : using namespace std;
      26                 :            : using namespace cvc5::internal::kind;
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace theory {
      30                 :            : namespace quantifiers {
      31                 :            : 
      32                 :          6 : QueryGenerator::QueryGenerator(Env& env) : ExprMiner(env), d_queryCount(0) {}
      33                 :          6 : void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
      34                 :            : {
      35                 :          6 :   d_queryCount = 0;
      36                 :          6 :   ExprMiner::initialize(vars, ss);
      37                 :          6 : }
      38                 :            : 
      39                 :        836 : void QueryGenerator::dumpQuery(Node qy,
      40                 :            :                                const Result& r,
      41                 :            :                                std::vector<Node>& queries)
      42                 :            : {
      43                 :        836 :   d_queryCount++;
      44                 :            :   bool isSolved =
      45 [ +  + ][ +  - ]:        836 :       r.getStatus() == Result::SAT || r.getStatus() == Result::UNSAT;
      46                 :            :   // add to queries if not filtered
      47 [ +  - ][ +  - ]:        836 :   if (!isSolved || !options().quantifiers.sygusQueryFilterSolved)
                 [ +  - ]
      48                 :            :   {
      49                 :        836 :     queries.push_back(qy);
      50                 :            :   }
      51                 :            :   // return if we should not dump the query based on the options
      52                 :        836 :   if (options().quantifiers.sygusQueryGenDumpFiles
      53         [ +  - ]:        836 :       == options::SygusQueryDumpFilesMode::NONE)
      54                 :            :   {
      55                 :        836 :     return;
      56                 :            :   }
      57                 :          0 :   if (options().quantifiers.sygusQueryGenDumpFiles
      58         [ -  - ]:          0 :       == options::SygusQueryDumpFilesMode::UNSOLVED)
      59                 :            :   {
      60         [ -  - ]:          0 :     if (isSolved)
      61                 :            :     {
      62                 :          0 :       return;
      63                 :            :     }
      64                 :            :   }
      65                 :            : 
      66                 :          0 :   Node kqy = convertToSkolem(qy);
      67                 :            :   // Print the query to to queryN.smt2
      68                 :          0 :   std::stringstream fname;
      69                 :          0 :   fname << "query" << d_queryCount << ".smt2";
      70                 :          0 :   std::ofstream fs(fname.str(), std::ofstream::out);
      71                 :          0 :   smt::PrintBenchmark pb(nodeManager(), Printer::getPrinter(fs));
      72                 :          0 :   pb.printBenchmark(fs, d_env.getLogicInfo().getLogicString(), {}, {kqy});
      73                 :          0 :   fs.close();
      74                 :          0 : }
      75                 :            : 
      76                 :        474 : void QueryGenerator::ensureBoolean(const Node& n) const
      77                 :            : {
      78         [ -  + ]:        474 :   if (!n.getType().isBoolean())
      79                 :            :   {
      80                 :          0 :     std::stringstream ss;
      81                 :            :     ss << "SyGuS query generation in the current mode requires the grammar to "
      82                 :          0 :           "generate Boolean terms only";
      83                 :          0 :     throw LogicException(ss.str());
      84                 :          0 :   }
      85                 :        474 : }
      86                 :            : 
      87                 :          2 : QueryGeneratorBasic::QueryGeneratorBasic(Env& env) : QueryGenerator(env) {}
      88                 :            : 
      89                 :        418 : bool QueryGeneratorBasic::addTerm(Node n, std::vector<Node>& queries)
      90                 :            : {
      91                 :        418 :   ensureBoolean(n);
      92                 :        418 :   SubsolverSetupInfo ssi(d_env);
      93                 :        418 :   Result r = doCheck(n, ssi);
      94                 :        418 :   dumpQuery(n, r, queries);
      95                 :        418 :   return true;
      96                 :        418 : }
      97                 :            : 
      98                 :            : }  // namespace quantifiers
      99                 :            : }  // namespace theory
     100                 :            : }  // namespace cvc5::internal