From: Andrew Reynolds Date: Thu, 1 Jul 2021 22:35:13 +0000 (-0500) Subject: Add recursive function definitions to subsolver in sygus (#6824) X-Git-Tag: cvc5-1.0.0~1537 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4e98013a8e2572545ec3f637dd1caa06e3f7207;p=cvc5.git Add recursive function definitions to subsolver in sygus (#6824) This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls. This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example. --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 45341a6a6..cfb678991 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1317,6 +1317,14 @@ name = "Quantifiers" default = "1000" help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)" +[[option]] + name = "sygusVerifyInstMaxRounds" + category = "regular" + long = "sygus-verify-inst-max-rounds=N" + type = "int" + default = "3" + help = "maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 3)" + # Internal uses of sygus [[option]] diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index a46452004..027ba71ec 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -84,7 +84,7 @@ std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( std::unique_ptr optChecker; // initializeSubSolver will copy the options and theories enabled // from the current solver to optChecker and adds timeout - theory::initializeSubsolver(optChecker, needsTimeout, timeout); + theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout); // we need to be in incremental mode for multiple objectives since we need to // push pop we need to produce models to inrement on our objective optChecker->setOption("incremental", "true"); diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 14bc05335..72605e9d1 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -78,7 +78,8 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, Assert (!query.isNull()); if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { - initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); + initializeSubsolver( + checker, nullptr, true, options::sygusExprMinerCheckTimeout()); } else { diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index beb2a33cd..36f557db8 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -41,7 +41,9 @@ void FunDefEvaluator::assertDefinition(Node q) Node f = h.hasOperator() ? h.getOperator() : h; Assert(d_funDefMap.find(f) == d_funDefMap.end()) << "FunDefEvaluator::assertDefinition: function already defined"; + d_funDefs.push_back(q); FunDefInfo& fdi = d_funDefMap[f]; + fdi.d_quant = q; fdi.d_body = QuantAttributes::getFunDefBody(q); Assert(!fdi.d_body.isNull()); fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end()); @@ -251,6 +253,20 @@ Node FunDefEvaluator::evaluate(Node n) const bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); } +const std::vector& FunDefEvaluator::getDefinitions() const +{ + return d_funDefs; +} +Node FunDefEvaluator::getDefinitionFor(Node f) const +{ + std::map::const_iterator it = d_funDefMap.find(f); + if (it != d_funDefMap.end()) + { + return it->second.d_quant; + } + return Node::null(); +} + } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h index 54565b4ee..a3b79bec7 100644 --- a/src/theory/quantifiers/fun_def_evaluator.h +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -53,11 +53,18 @@ class FunDefEvaluator */ bool hasDefinitions() const; + /** Get definitions */ + const std::vector& getDefinitions() const; + /** Get definition for function symbol f, if it is cached by this class */ + Node getDefinitionFor(Node f) const; + private: /** information cached per function definition */ class FunDefInfo { public: + /** the quantified formula */ + Node d_quant; /** the body */ Node d_body; /** the formal argument list */ @@ -65,6 +72,8 @@ class FunDefEvaluator }; /** maps functions to the above information */ std::map d_funDefMap; + /** list of all definitions */ + std::vector d_funDefs; /** evaluator utility */ Evaluator d_eval; }; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 0b5d06bd2..739e9ab0d 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -233,9 +233,11 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // make the satisfiability query std::unique_ptr repcChecker; // initialize the subsolver using the standard method - initializeSubsolver(repcChecker, - Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, - options::sygusRepairConstTimeout()); + initializeSubsolver( + repcChecker, + nullptr, + Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, + options::sygusRepairConstTimeout()); // renable options disabled by sygus repcChecker->setOption("miniscope-quant", "true"); repcChecker->setOption("miniscope-quant-fv", "true"); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 62c61fe1e..4e8d7d46d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "base/configuration.h" +#include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/datatypes_options.h" @@ -87,6 +88,18 @@ 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,8 +593,34 @@ bool SynthConjecture::doCheck(std::vector& lems) if (!query.isConst() || query.getConst()) { + // 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); + 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) { diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 4329a9c60..bf3e7b31d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -423,6 +423,8 @@ 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_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 86c3f62d0..1792f9386 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -164,7 +164,7 @@ void SynthEngine::checkOwnership(Node q) // take ownership of quantified formulas with sygus attribute, and function // definitions when options::sygusRecFun is true. QuantAttributes& qa = d_qreg.getQuantAttributes(); - if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q))) + if (qa.isSygus(q) || (qa.isFunDef(q) && options::sygusRecFun())) { d_qreg.setOwner(q, this, 2); } diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 1c76f0205..5f285dc07 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -42,13 +42,18 @@ Result quickCheck(Node& query) } void initializeSubsolver(std::unique_ptr& smte, + Options* opts, bool needsTimeout, unsigned long timeout) { NodeManager* nm = NodeManager::currentNM(); SmtEngine* smtCurr = smt::currentSmtEngine(); - // must copy the options - smte.reset(new SmtEngine(nm, &smtCurr->getOptions())); + if (opts == nullptr) + { + // must copy the options + opts = &smtCurr->getOptions(); + } + smte.reset(new SmtEngine(nm, opts)); smte->setIsInternalSubsolver(); smte->setLogic(smtCurr->getLogicInfo()); // set the options @@ -60,6 +65,7 @@ void initializeSubsolver(std::unique_ptr& smte, Result checkWithSubsolver(std::unique_ptr& smte, Node query, + Options* opts, bool needsTimeout, unsigned long timeout) { @@ -69,21 +75,26 @@ Result checkWithSubsolver(std::unique_ptr& smte, { return r; } - initializeSubsolver(smte, needsTimeout, timeout); + initializeSubsolver(smte, opts, needsTimeout, timeout); smte->assertFormula(query); return smte->checkSat(); } -Result checkWithSubsolver(Node query, bool needsTimeout, unsigned long timeout) +Result checkWithSubsolver(Node query, + Options* opts, + bool needsTimeout, + unsigned long timeout) { std::vector vars; std::vector modelVals; - return checkWithSubsolver(query, vars, modelVals, needsTimeout, timeout); + return checkWithSubsolver( + query, vars, modelVals, opts, needsTimeout, timeout); } Result checkWithSubsolver(Node query, const std::vector& vars, std::vector& modelVals, + Options* opts, bool needsTimeout, unsigned long timeout) { @@ -105,7 +116,7 @@ Result checkWithSubsolver(Node query, return r; } std::unique_ptr smte; - initializeSubsolver(smte, needsTimeout, timeout); + initializeSubsolver(smte, opts, needsTimeout, timeout); smte->assertFormula(query); r = smte->checkSat(); if (r.asSatisfiabilityResult().isSat() == Result::SAT) diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index f7985d651..2d80831f2 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -41,10 +41,13 @@ namespace theory { * if the current SMT engine has declared a separation logic heap. * * @param smte The smt engine pointer to initialize + * @param opts The options for the subsolver. If nullptr, then we copy the + * options from the current SmtEngine in scope. * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ void initializeSubsolver(std::unique_ptr& smte, + Options* opts = nullptr, bool needsTimeout = false, unsigned long timeout = 0); @@ -56,6 +59,7 @@ void initializeSubsolver(std::unique_ptr& smte, */ Result checkWithSubsolver(std::unique_ptr& smte, Node query, + Options* opts = nullptr, bool needsTimeout = false, unsigned long timeout = 0); @@ -66,10 +70,12 @@ Result checkWithSubsolver(std::unique_ptr& smte, * concerned with the state of the SMT engine after the check. * * @param query The query to check + * @param opts The options for the subsolver * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ Result checkWithSubsolver(Node query, + Options* opts = nullptr, bool needsTimeout = false, unsigned long timeout = 0); @@ -81,12 +87,14 @@ Result checkWithSubsolver(Node query, * @param query The query to check * @param vars The variables we are interesting in getting a model for. * @param modelVals A vector storing the model values of variables in vars. + * @param opts The options for the subsolver * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ Result checkWithSubsolver(Node query, const std::vector& vars, std::vector& modelVals, + Options* opts = nullptr, bool needsTimeout = false, unsigned long timeout = 0); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e2e216567..260b0d9b7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2521,6 +2521,7 @@ set(regress_2_tests regress2/sygus/process-arg-invariance.sy regress2/sygus/real-grammar-neg.sy regress2/sygus/sets-fun-test.sy + regress2/sygus/sumn_recur_synth.sy regress2/sygus/strings-no-syntax-len.sy regress2/sygus/three.sy regress2/typed_v1l50016-simp.cvc diff --git a/test/regress/regress2/sygus/sumn_recur_synth.sy b/test/regress/regress2/sygus/sumn_recur_synth.sy new file mode 100644 index 000000000..103992dfe --- /dev/null +++ b/test/regress/regress2/sygus/sumn_recur_synth.sy @@ -0,0 +1,37 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic UFLIA) + +(declare-var x Int) +(declare-var x! Int) +(declare-var y Int) +(declare-var y! Int) + +(define-fun-rec sum_n ((x Int)) Int + (ite (>= x 1) + (+ x (sum_n (- x 1))) + 0)) + +(synth-fun inv_fun ((x Int) (y Int)) Bool + ((C Bool) (B Bool) (E Int)) + ((C Bool ((and (>= y 1) B))) + (B Bool ((= (sum_n E) E) (>= E E))) + (E Int (0 1 x y (+ E E)))) +) + +(define-fun pre_fun ((x Int) (y Int)) Bool + (and (= x 0) (= y 1))) + +(define-fun trans_fun ((x Int) (y Int) (x! Int) (y! Int)) Bool + (and (<= y 2) (= x! (+ x y)) (= y! (+ y 1)))) + +(define-fun post_fun ((x Int) (y Int)) Bool + (= x (sum_n (- y 1))) +) + +(constraint (=> (pre_fun x y) (inv_fun x y))) +(constraint (=> (and (inv_fun x y) (trans_fun x y x! y!)) (inv_fun x! y!))) +(constraint (=> (inv_fun x y) (post_fun x y))) + + +(check-synth)