diff options
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.cpp')
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 148 |
1 files changed, 49 insertions, 99 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index e5df8db8a..3b7aab0b2 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -36,40 +36,36 @@ CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr), d_tds(nullptr), d_ext_rewrite(nullptr), - d_using_sygus(false) + d_using_sygus(false), + d_silent(false) { } -void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, - TypeNode tn, - std::vector<Node>& vars, - unsigned nsamples, - bool unique_type_ids) +void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars, + SygusSampler* ss) { + Assert(ss != nullptr); d_candidate = Node::null(); - d_type = tn; d_using_sygus = false; d_qe = nullptr; d_tds = nullptr; - d_ext_rewrite = er; - d_sampler.initialize(tn, vars, nsamples, unique_type_ids); - d_crewrite_filter.initialize(&d_sampler, nullptr, false); + d_ext_rewrite = nullptr; + d_crewrite_filter.initialize(ss, nullptr, false); + ExprMiner::initialize(vars, ss); } -void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, +void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, + QuantifiersEngine* qe, Node f, - unsigned nsamples, - bool useSygusType) + SygusSampler* ss) { + Assert(ss != nullptr); d_candidate = f; - d_type = f.getType(); - Assert(d_type.isDatatype()); - Assert(static_cast<DatatypeType>(d_type.toType()).getDatatype().isSygus()); d_using_sygus = true; d_qe = qe; d_tds = d_qe->getTermDatabaseSygus(); - d_ext_rewrite = d_tds->getExtRewriter(); - d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); - d_crewrite_filter.initialize(&d_sampler, d_tds, true); + d_ext_rewrite = nullptr; + d_crewrite_filter.initialize(ss, d_tds, false); + ExprMiner::initialize(vars, ss); } bool CandidateRewriteDatabase::addTerm(Node sol, @@ -77,7 +73,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, bool& rew_print) { bool is_unique_term = true; - Node eq_sol = d_sampler.registerTerm(sol); + Node eq_sol = d_sampler->registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol if (eq_sol != sol) { @@ -116,81 +112,23 @@ bool CandidateRewriteDatabase::addTerm(Node sol, Node crr = solbr.eqNode(eq_solr).negate(); Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl; - // quantify over the free variables in crr - std::vector<Node> fvs; - TermUtil::computeVarContains(crr, fvs); - std::map<Node, unsigned> fv_index; - std::vector<Node> sks; - if (!fvs.empty()) - { - // map to skolems - for (unsigned i = 0, size = fvs.size(); i < size; i++) - { - Node v = fvs[i]; - fv_index[v] = i; - std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v); - if (itf == d_fv_to_skolem.end()) - { - Node sk = nm->mkSkolem("rrck", v.getType()); - d_fv_to_skolem[v] = sk; - sks.push_back(sk); - } - else - { - sks.push_back(itf->second); - } - } - crr = crr.substitute(fvs.begin(), fvs.end(), sks.begin(), sks.end()); - } // Notice we don't set produce-models. rrChecker takes the same // options as the SmtEngine we belong to, where we ensure that // produce-models is set. - bool needExport = true; + bool needExport = false; ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> rrChecker; - Result r; - if (options::sygusRewSynthCheckTimeout.wasSetByUser()) - { - // To support a separate timeout for the subsolver, we need to create - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. If the export fails, we throw an - // OptionException. - try - { - rrChecker.reset(new SmtEngine(&em)); - rrChecker->setTimeLimit(options::sygusRewSynthCheckTimeout(), true); - rrChecker->setLogic(smt::currentSmtEngine()->getLogicInfo()); - Expr eccr = crr.toExpr().exportTo(&em, varMap); - rrChecker->assertFormula(eccr); - r = rrChecker->checkSat(); - } - catch (const CVC4::ExportUnsupportedException& e) - { - std::stringstream msg; - msg << "Unable to export " << crr - << " but exporting expressions is required for " - "--sygus-rr-synth-check-timeout."; - throw OptionException(msg.str()); - } - } - else - { - needExport = false; - rrChecker.reset(new SmtEngine(nm->toExprManager())); - rrChecker->assertFormula(crr.toExpr()); - r = rrChecker->checkSat(); - } - + initializeChecker(rrChecker, em, varMap, crr, needExport); + Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { Trace("rr-check") << "...rewrite does not hold for: " << std::endl; is_unique_term = true; std::vector<Node> vars; - d_sampler.getVariables(vars); + d_sampler->getVariables(vars); std::vector<Node> pt; for (const Node& v : vars) { @@ -200,8 +138,8 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // looking up the model value if (v.getKind() == BOUND_VARIABLE) { - std::map<Node, unsigned>::iterator itf = fv_index.find(v); - if (itf == fv_index.end()) + std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v); + if (itf == d_fv_to_skolem.end()) { // not in conjecture, can use arbitrary value val = v.getType().mkGroundTerm(); @@ -209,7 +147,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, else { // get the model value of its skolem - refv = sks[itf->second]; + refv = itf->second; } } if (val.isNull()) @@ -229,10 +167,10 @@ bool CandidateRewriteDatabase::addTerm(Node sol, Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); } - d_sampler.addSamplePoint(pt); + d_sampler->addSamplePoint(pt); // add the solution again // by construction of the above point, we should be unique now - Node eq_sol_new = d_sampler.registerTerm(sol); + Node eq_sol_new = d_sampler->registerTerm(sol); Assert(eq_sol_new == sol); } else @@ -252,19 +190,23 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // The analog of terms sol and eq_sol are equivalent under // sample points but do not rewrite to the same term. Hence, // this indicates a candidate rewrite. - out << "(" << (verified ? "" : "candidate-") << "rewrite "; - if (d_using_sygus) - { - Printer* p = Printer::getPrinter(options::outputLanguage()); - p->toStreamSygus(out, sol); - out << " "; - p->toStreamSygus(out, eq_sol); - } - else + if (!d_silent) { - out << sol << " " << eq_sol; + out << "(" << (verified ? "" : "candidate-") << "rewrite "; + if (d_using_sygus) + { + Printer* p = Printer::getPrinter(options::outputLanguage()); + p->toStreamSygus(out, sol); + out << " "; + p->toStreamSygus(out, eq_sol); + } + else + { + out << sol << " " << eq_sol; + } + out << ")" << std::endl; } - out << ")" << std::endl; + // we count this as printed, despite not literally printing it rew_print = true; // debugging information if (Trace.isOn("sygus-rr-debug")) @@ -319,6 +261,13 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) return addTerm(sol, out, rew_print); } +void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } + +void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) +{ + d_ext_rewrite = er; +} + CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( std::vector<Node>& vars, unsigned nsamples) : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) @@ -347,7 +296,8 @@ bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) { Trace("synth-rr-dbg") << "Initialize database for " << tn << std::endl; // initialize with the extended rewriter owned by this class - d_cdbs[tn].initialize(er, tn, d_vars, d_nsamples, true); + d_cdbs[tn].initialize(d_vars, &d_sampler[tn]); + d_cdbs[tn].setExtendedRewriter(er); itc = d_cdbs.find(tn); Trace("synth-rr-dbg") << "...finish." << std::endl; } |