src/theory/quantifiers/expr_miner.cpp

   1 /*********************                                                        */
   2 /*! \file expr_miner.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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("sygus-abduct", false);
  95       checker->setOption("input-language", "smt2");
  96       Expr equery = squery.toExpr().exportTo(&em, varMap);
  97       checker->assertFormula(equery);
  98     }
  99     catch (const CVC4::ExportUnsupportedException& e)
 100     {
 101       std::stringstream msg;
 102       msg << "Unable to export " << squery
 103           << " but exporting expressions is "
 104              "required for an expression "
 105              "miner check.";
 106       throw OptionException(msg.str());
 107     }
 108     needExport = true;
 109   }
 110   else
 111   {
 112     needExport = false;
 113     checker.reset(new SmtEngine(nm->toExprManager()));
 114     checker->assertFormula(squery.toExpr());
 115   }
 116 }
 117
 118 Result ExprMiner::doCheck(Node query)
 119 {
 120   Node queryr = Rewriter::rewrite(query);
 121   if (queryr.isConst())
 122   {
 123     if (!queryr.getConst<bool>())
 124     {
 125       return Result(Result::UNSAT);
 126     }
 127     else
 128     {
 129       return Result(Result::SAT);
 130     }
 131   }
 132   NodeManager* nm = NodeManager::currentNM();
 133   bool needExport = false;
 134   ExprManager em(nm->getOptions());
 135   std::unique_ptr<SmtEngine> smte;
 136   ExprManagerMapCollection varMap;
 137   initializeChecker(smte, em, varMap, queryr, needExport);
 138   return smte->checkSat();
 139 }
 140
 141 }  // namespace quantifiers
 142 }  // namespace theory
 143 }  // namespace CVC4