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
initialize(const std::vector<Node> & vars,SygusSampler * ss)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
convertToSkolem(Node n)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
initializeChecker(std::unique_ptr<SmtEngine> & checker,ExprManager & em,ExprManagerMapCollection & varMap,Node query,bool & needExport)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
doCheck(Node query)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
144