From: Andrew Reynolds Date: Wed, 14 Jul 2021 20:42:40 +0000 (-0500) Subject: Move synthesis verification check to own file (#6882) X-Git-Tag: cvc5-1.0.0~1490 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7d01e2f8f0e2ff5d2af30aa6b97e5e16758997e;p=cvc5.git Move synthesis verification check to own file (#6882) In preparation for more extensions to this aspect of the synthesis solver. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bc0a922d2..e001dd462 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -915,6 +915,8 @@ libcvc5_add_sources( theory/quantifiers/sygus/synth_conjecture.h theory/quantifiers/sygus/synth_engine.cpp theory/quantifiers/sygus/synth_engine.h + theory/quantifiers/sygus/synth_verify.cpp + theory/quantifiers/sygus/synth_verify.h theory/quantifiers/sygus/template_infer.cpp theory/quantifiers/sygus/template_infer.h theory/quantifiers/sygus/term_database_sygus.cpp diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b2b69687c..1ddc2fa22 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -59,6 +59,7 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), + d_verify(d_tds), d_hasSolution(false), d_ceg_si(new CegSingleInv(tr, s)), d_templInfer(new SygusTemplateInfer), @@ -89,18 +90,6 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_modules.push_back(d_sygus_ccore.get()); } d_modules.push_back(d_ceg_cegis.get()); - // determine the options to use for the verification subsolvers we spawn - // we start with the options of the current SmtEngine - SmtEngine* smtCurr = smt::currentSmtEngine(); - d_subOptions.copyValues(smtCurr->getOptions()); - // limit the number of instantiation rounds on subcalls - d_subOptions.quantifiers.instMaxRounds = - d_subOptions.quantifiers.sygusVerifyInstMaxRounds; - // Disable sygus on the subsolver. This is particularly important since it - // ensures that recursive function definitions have the standard ownership - // instead of being claimed by sygus in the subsolver. - d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; - d_subOptions.quantifiers.sygus = false; } SynthConjecture::~SynthConjecture() {} @@ -580,86 +569,31 @@ bool SynthConjecture::doCheck(std::vector& lems) return false; } - // simplify the lemma based on the term database sygus utility - query = d_tds->rewriteNode(query); - // eagerly unfold applications of evaluation function - Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl; // Record the solution, which may be falsified below. We require recording // here since the result of the satisfiability test may be unknown. recordSolution(candidate_values); - if (!query.isConst() || query.getConst()) + Result r = d_verify.verify(query, d_ce_sk_vars, d_ce_sk_var_mvs); + + if (r.asSatisfiabilityResult().isSat() == Result::SAT) { - // add recursive function definitions - FunDefEvaluator* feval = d_tds->getFunDefEvaluator(); - const std::vector& fdefs = feval->getDefinitions(); - if (!fdefs.empty()) - { - // Get the relevant definitions based on the symbols in the query. - // Notice in some cases, this may have the effect of making the subcall - // involve no recursive function definitions at all, in which case the - // subcall to verification may be decidable, in which case the call - // below is guaranteed to generate a new counterexample point. - std::unordered_set syms; - expr::getSymbols(query, syms); - std::vector qconj; - qconj.push_back(query); - for (const Node& f : syms) - { - Node q = feval->getDefinitionFor(f); - if (!q.isNull()) - { - qconj.push_back(q); - } - } - query = nm->mkAnd(qconj); - Trace("cegqi-debug") << "query is " << query << std::endl; - } - Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - Result r = - checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs, &d_subOptions); - Trace("sygus-engine") << " ...got " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - if (Trace.isOn("sygus-engine")) - { - Trace("sygus-engine") << " * Verification lemma failed for:\n "; - for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) - { - Trace("sygus-engine") - << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; - } - Trace("sygus-engine") << std::endl; - } - if (Configuration::isAssertionBuild()) - { - // the values for the query should be a complete model - Node squery = query.substitute(d_ce_sk_vars.begin(), - d_ce_sk_vars.end(), - d_ce_sk_var_mvs.begin(), - d_ce_sk_var_mvs.end()); - Trace("cegqi-debug") << "...squery : " << squery << std::endl; - squery = Rewriter::rewrite(squery); - Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(options::sygusRecFun() - || (squery.isConst() && squery.getConst())); - } - return false; - } - else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) - { - // In the rare case that the subcall is unknown, we simply exclude the - // solution, without adding a counterexample point. This should only - // happen if the quantifier free logic is undecidable. - excludeCurrentSolution(terms, candidate_values); - // We should set incomplete, since a "sat" answer should not be - // interpreted as "infeasible", which would make a difference in the rare - // case where e.g. we had a finite grammar and exhausted the grammar. - d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY); - return false; - } - // otherwise we are unsat, and we will process the solution below + // we have a counterexample + return false; + } + else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + // In the rare case that the subcall is unknown, we simply exclude the + // solution, without adding a counterexample point. This should only + // happen if the quantifier free logic is undecidable. + excludeCurrentSolution(terms, candidate_values); + // We should set incomplete, since a "sat" answer should not be + // interpreted as "infeasible", which would make a difference in the rare + // case where e.g. we had a finite grammar and exhausted the grammar. + d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY); + return false; } + // otherwise we are unsat, and we will process the solution below + // now mark that we have a solution d_hasSolution = true; if (options::sygusStream()) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index bf3e7b31d..e6645ddf2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -31,6 +31,7 @@ #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "theory/quantifiers/sygus/sygus_stats.h" +#include "theory/quantifiers/sygus/synth_verify.h" #include "theory/quantifiers/sygus/template_infer.h" namespace cvc5 { @@ -216,6 +217,8 @@ class SynthConjecture SygusStatistics& d_stats; /** term database sygus of d_qe */ TermDbSygus* d_tds; + /** The synthesis verify utility */ + SynthVerify d_verify; /** The feasible guard. */ Node d_feasible_guard; /** @@ -423,8 +426,6 @@ class SynthConjecture * rewrite rules. */ std::map d_exprm; - /** The options for subsolver calls */ - Options d_subOptions; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp new file mode 100644 index 000000000..43131ac24 --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -0,0 +1,130 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Class for verifying queries for synthesis solutions + */ + +#include "theory/quantifiers/sygus/synth_verify.h" + +#include "expr/node_algorithm.h" +#include "options/base_options.h" +#include "options/quantifiers_options.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" + +using namespace cvc5::kind; +using namespace std; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +SynthVerify::SynthVerify(TermDbSygus* tds) : d_tds(tds) +{ + // determine the options to use for the verification subsolvers we spawn + // we start with the options of the current SmtEngine + SmtEngine* smtCurr = smt::currentSmtEngine(); + d_subOptions.copyValues(smtCurr->getOptions()); + // limit the number of instantiation rounds on subcalls + d_subOptions.quantifiers.instMaxRounds = + d_subOptions.quantifiers.sygusVerifyInstMaxRounds; + // Disable sygus on the subsolver. This is particularly important since it + // ensures that recursive function definitions have the standard ownership + // instead of being claimed by sygus in the subsolver. + d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; + d_subOptions.quantifiers.sygus = false; +} + +SynthVerify::~SynthVerify() {} + +Result SynthVerify::verify(Node query, + const std::vector& vars, + std::vector& mvs) +{ + NodeManager* nm = NodeManager::currentNM(); + // simplify the lemma based on the term database sygus utility + query = d_tds->rewriteNode(query); + // eagerly unfold applications of evaluation function + Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl; + + if (query.isConst()) + { + if (!query.getConst()) + { + return Result(Result::UNSAT); + } + // sat, but we need to get arbtirary model values below + } + else + { + // if non-constant, we may need to add recursive function definitions + FunDefEvaluator* feval = d_tds->getFunDefEvaluator(); + const std::vector& fdefs = feval->getDefinitions(); + if (!fdefs.empty()) + { + // Get the relevant definitions based on the symbols in the query. + // Notice in some cases, this may have the effect of making the subcall + // involve no recursive function definitions at all, in which case the + // subcall to verification may be decidable, in which case the call + // below is guaranteed to generate a new counterexample point. + std::unordered_set syms; + expr::getSymbols(query, syms); + std::vector qconj; + qconj.push_back(query); + for (const Node& f : syms) + { + Node q = feval->getDefinitionFor(f); + if (!q.isNull()) + { + qconj.push_back(q); + } + } + query = nm->mkAnd(qconj); + Trace("cegqi-debug") << "query is " << query << std::endl; + } + } + Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; + Result r = checkWithSubsolver(query, vars, mvs, &d_subOptions); + Trace("sygus-engine") << " ...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + if (Trace.isOn("sygus-engine")) + { + Trace("sygus-engine") << " * Verification lemma failed for:\n "; + for (unsigned i = 0, size = vars.size(); i < size; i++) + { + Trace("sygus-engine") << vars[i] << " -> " << mvs[i] << " "; + } + Trace("sygus-engine") << std::endl; + } + if (Configuration::isAssertionBuild()) + { + // the values for the query should be a complete model + Node squery = + query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end()); + Trace("cegqi-debug") << "...squery : " << squery << std::endl; + squery = Rewriter::rewrite(squery); + Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; + Assert(options::sygusRecFun() + || (squery.isConst() && squery.getConst())); + } + } + return r; +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h new file mode 100644 index 000000000..794908ee5 --- /dev/null +++ b/src/theory/quantifiers/sygus/synth_verify.h @@ -0,0 +1,64 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Class for verifying queries for synthesis solutions + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_VERIFY_H +#define CVC5__THEORY__QUANTIFIERS__SYNTH_VERIFY_H + +#include + +#include "options/options.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "util/result.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * Class for verifying queries corresponding to synthesis conjectures + */ +class SynthVerify +{ + public: + SynthVerify(TermDbSygus* tds); + ~SynthVerify(); + /** + * Verification call, which takes into account specific aspects of the + * synthesis conjecture, e.g. recursive function definitions. + * + * @param query The query corresponding to the negated body of the synthesis + * conjecture + * @param vars The skolem variables witnessing the counterexample + * @param mvs If satisfiable, these contain the model value for vars + * @return The result of whether query is satisfiable. + */ + Result verify(Node query, + const std::vector& vars, + std::vector& mvs); + + private: + /** Pointer to the term database sygus */ + TermDbSygus* d_tds; + /** The options for subsolver calls */ + Options d_subOptions; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif