src/theory/quantifiers/expr_miner.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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 expr_miner.
  14  */
  15
  16 #include "theory/quantifiers/expr_miner.h"
  17
  18 #include "expr/skolem_manager.h"
  19 #include "options/quantifiers_options.h"
  20 #include "theory/quantifiers/term_util.h"
  21 #include "theory/rewriter.h"
  22
  23 using namespace std;
  24 using namespace cvc5::kind;
  25
  26 namespace cvc5 {
  27 namespace theory {
  28 namespace quantifiers {
  29
  30 void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
  31 {
  32   d_sampler = ss;
  33   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
  34 }
  35
  36 Node ExprMiner::convertToSkolem(Node n)
  37 {
  38   if (d_skolems.empty())
  39   {
  40     NodeManager* nm = NodeManager::currentNM();
  41     SkolemManager* sm = nm->getSkolemManager();
  42     for (const Node& v : d_vars)
  43     {
  44       Node sk = sm->mkDummySkolem("rrck", v.getType());
  45       d_skolems.push_back(sk);
  46       d_fv_to_skolem[v] = sk;
  47     }
  48   }
  49   return n.substitute(
  50       d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
  51 }
  52
  53 void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
  54                                   Node query)
  55 {
  56   initializeChecker(checker, query, options(), logicInfo());
  57 }
  58
  59 void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
  60                                   Node query,
  61                                   const Options& opts,
  62                                   const LogicInfo& logicInfo)
  63 {
  64   Assert (!query.isNull());
  65   if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
  66   {
  67     initializeSubsolver(
  68         checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout());
  69   }
  70   else
  71   {
  72     initializeSubsolver(checker, opts, logicInfo);
  73   }
  74   // also set the options
  75   checker->setOption("sygus-rr-synth-input", "false");
  76   checker->setOption("input-language", "smt2");
  77   // Convert bound variables to skolems. This ensures the satisfiability
  78   // check is ground.
  79   Node squery = convertToSkolem(query);
  80   checker->assertFormula(squery);
  81 }
  82
  83 Result ExprMiner::doCheck(Node query)
  84 {
  85   Node queryr = Rewriter::rewrite(query);
  86   if (queryr.isConst())
  87   {
  88     if (!queryr.getConst<bool>())
  89     {
  90       return Result(Result::UNSAT);
  91     }
  92     else
  93     {
  94       return Result(Result::SAT);
  95     }
  96   }
  97   std::unique_ptr<SolverEngine> smte;
  98   initializeChecker(smte, query);
  99   return smte->checkSat();
 100 }
 101
 102 }  // namespace quantifiers
 103 }  // namespace theory
 104 }  // namespace cvc5