src/theory/quantifiers/expr_miner.cpp

   1 /*********************                                                        */
   2 /*! \file expr_miner.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Implementation of expr_miner
  13  **/
  14
  15 #include "theory/quantifiers/expr_miner.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "smt/smt_engine.h"
  19 #include "smt/smt_engine_scope.h"
  20 #include "theory/quantifiers/term_util.h"
  21
  22 using namespace std;
  23 using namespace CVC4::kind;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
  30 {
  31   d_sampler = ss;
  32   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
  33 }
  34
  35 Node ExprMiner::convertToSkolem(Node n)
  36 {
  37   std::vector<Node> fvs;
  38   TermUtil::computeVarContains(n, fvs);
  39   if (fvs.empty())
  40   {
  41     return n;
  42   }
  43   std::vector<Node> sfvs;
  44   std::vector<Node> sks;
  45   // map to skolems
  46   NodeManager* nm = NodeManager::currentNM();
  47   for (unsigned i = 0, size = fvs.size(); i < size; i++)
  48   {
  49     Node v = fvs[i];
  50     // only look at the sampler variables
  51     if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
  52     {
  53       sfvs.push_back(v);
  54       std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
  55       if (itf == d_fv_to_skolem.end())
  56       {
  57         Node sk = nm->mkSkolem("rrck", v.getType());
  58         d_fv_to_skolem[v] = sk;
  59         sks.push_back(sk);
  60       }
  61       else
  62       {
  63         sks.push_back(itf->second);
  64       }
  65     }
  66   }
  67   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
  68 }
  69
  70 void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
  71                                   ExprManager& em,
  72                                   ExprManagerMapCollection& varMap,
  73                                   Node query,
  74                                   bool& needExport)
  75 {
  76   // Convert bound variables to skolems. This ensures the satisfiability
  77   // check is ground.
  78   Node squery = convertToSkolem(query);
  79   NodeManager* nm = NodeManager::currentNM();
  80   if (options::sygusExprMinerCheckUseExport())
  81   {
  82     // To support a separate timeout for the subsolver, we need to create
  83     // a separate ExprManager with its own options. This requires that
  84     // the expressions sent to the subsolver can be exported from on
  85     // ExprManager to another. If the export fails, we throw an
  86     // OptionException.
  87     try
  88     {
  89       checker.reset(new SmtEngine(&em));
  90       checker->setIsInternalSubsolver();
  91       checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
  92       checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
  93       checker->setOption("sygus-rr-synth-input", false);
  94       checker->setOption("input-language", "smt2");
  95       Expr equery = squery.toExpr().exportTo(&em, varMap);
  96       checker->assertFormula(equery);
  97     }
  98     catch (const CVC4::ExportUnsupportedException& e)
  99     {
 100       std::stringstream msg;
 101       msg << "Unable to export " << squery
 102           << " but exporting expressions is "
 103              "required for an expression "
 104              "miner check.";
 105       throw OptionException(msg.str());
 106     }
 107     needExport = true;
 108   }
 109   else
 110   {
 111     needExport = false;
 112     checker.reset(new SmtEngine(nm->toExprManager()));
 113     checker->assertFormula(squery.toExpr());
 114   }
 115 }
 116
 117 Result ExprMiner::doCheck(Node query)
 118 {
 119   Node queryr = Rewriter::rewrite(query);
 120   if (queryr.isConst())
 121   {
 122     if (!queryr.getConst<bool>())
 123     {
 124       return Result(Result::UNSAT);
 125     }
 126     else
 127     {
 128       return Result(Result::SAT);
 129     }
 130   }
 131   NodeManager* nm = NodeManager::currentNM();
 132   bool needExport = false;
 133   ExprManager em(nm->getOptions());
 134   std::unique_ptr<SmtEngine> smte;
 135   ExprManagerMapCollection varMap;
 136   initializeChecker(smte, em, varMap, queryr, needExport);
 137   return smte->checkSat();
 138 }
 139
 140 }  // namespace quantifiers
 141 }  // namespace theory
 142 }  // namespace CVC4