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-2020 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 "api/cvc4cpp.h"
  18 #include "options/quantifiers_options.h"
  19 #include "smt/smt_engine.h"
  20 #include "smt/smt_engine_scope.h"
  21 #include "theory/quantifiers/term_util.h"
  22 #include "theory/smt_engine_subsolver.h"
  23
  24 using namespace std;
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace quantifiers {
  30
  31 void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
  32 {
  33   d_sampler = ss;
  34   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
  35 }
  36
  37 Node ExprMiner::convertToSkolem(Node n)
  38 {
  39   std::vector<Node> fvs;
  40   TermUtil::computeVarContains(n, fvs);
  41   if (fvs.empty())
  42   {
  43     return n;
  44   }
  45   std::vector<Node> sfvs;
  46   std::vector<Node> sks;
  47   // map to skolems
  48   NodeManager* nm = NodeManager::currentNM();
  49   for (unsigned i = 0, size = fvs.size(); i < size; i++)
  50   {
  51     Node v = fvs[i];
  52     // only look at the sampler variables
  53     if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
  54     {
  55       sfvs.push_back(v);
  56       std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
  57       if (itf == d_fv_to_skolem.end())
  58       {
  59         Node sk = nm->mkSkolem("rrck", v.getType());
  60         d_fv_to_skolem[v] = sk;
  61         sks.push_back(sk);
  62       }
  63       else
  64       {
  65         sks.push_back(itf->second);
  66       }
  67     }
  68   }
  69   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
  70 }
  71
  72 void ExprMiner::initializeChecker(SmtEngine* checker,
  73                                   ExprManager* em,
  74                                   ExprManagerMapCollection& varMap,
  75                                   Node query,
  76                                   bool& needExport)
  77 {
  78   // Convert bound variables to skolems. This ensures the satisfiability
  79   // check is ground.
  80   Node squery = convertToSkolem(query);
  81   if (options::sygusExprMinerCheckUseExport())
  82   {
  83     initializeSubsolverWithExport(checker,
  84                                   em,
  85                                   varMap,
  86                                   squery.toExpr(),
  87                                   true,
  88                                   options::sygusExprMinerCheckTimeout());
  89     checker->setOption("sygus-rr-synth-input", false);
  90     checker->setOption("input-language", "smt2");
  91     needExport = true;
  92   }
  93   else
  94   {
  95     initializeSubsolver(checker, squery.toExpr());
  96     needExport = false;
  97   }
  98 }
  99
 100 Result ExprMiner::doCheck(Node query)
 101 {
 102   Node queryr = Rewriter::rewrite(query);
 103   if (queryr.isConst())
 104   {
 105     if (!queryr.getConst<bool>())
 106     {
 107       return Result(Result::UNSAT);
 108     }
 109     else
 110     {
 111       return Result(Result::SAT);
 112     }
 113   }
 114   // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
 115   // This is only temporarily until we have separate options for each
 116   // SmtEngine instance. We should reuse the same ExprManager with
 117   // a different SmtEngine (and different options) here, eventually.
 118   // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
 119   NodeManager* nm = NodeManager::currentNM();
 120   bool needExport = false;
 121   api::Solver slv(&nm->getOptions());
 122   ExprManager* em = slv.getExprManager();
 123   SmtEngine* smte = slv.getSmtEngine();
 124   ExprManagerMapCollection varMap;
 125   initializeChecker(smte, em, varMap, queryr, needExport);
 126   return smte->checkSat();
 127 }
 128
 129 }  // namespace quantifiers
 130 }  // namespace theory
 131 }  // namespace CVC4