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<SmtEngine>& checker,
  54                                   Node query)
  55 {
  56   Assert (!query.isNull());
  57   if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
  58   {
  59     initializeSubsolver(
  60         checker, nullptr, true, options::sygusExprMinerCheckTimeout());
  61   }
  62   else
  63   {
  64     initializeSubsolver(checker);
  65   }
  66   // also set the options
  67   checker->setOption("sygus-rr-synth-input", "false");
  68   checker->setOption("input-language", "smt2");
  69   // Convert bound variables to skolems. This ensures the satisfiability
  70   // check is ground.
  71   Node squery = convertToSkolem(query);
  72   checker->assertFormula(squery);
  73 }
  74
  75 Result ExprMiner::doCheck(Node query)
  76 {
  77   Node queryr = Rewriter::rewrite(query);
  78   if (queryr.isConst())
  79   {
  80     if (!queryr.getConst<bool>())
  81     {
  82       return Result(Result::UNSAT);
  83     }
  84     else
  85     {
  86       return Result(Result::SAT);
  87     }
  88   }
  89   std::unique_ptr<SmtEngine> smte;
  90   initializeChecker(smte, query);
  91   return smte->checkSat();
  92 }
  93
  94 }  // namespace quantifiers
  95 }  // namespace theory
  96 }  // namespace cvc5