From 36bb555ad804416f74fb582042d2999b216c51e0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Apr 2022 17:14:08 -0500 Subject: [PATCH] Generalization for sygus verify utility (#8586) This is in preparation for synthesis modulo oracles (SyMO), where the verification loop may run multiple times for a given solution. In a follow up PR, the loop introduced in this PR may run multiple times when oracles are present, since oracle invocations in the subsolver may trigger further simplifications to the rewritten form of the specification. It also makes it so that candidate models are generated for "unknown" results for subsolvers, which is required for SyMO. --- src/theory/quantifiers/sygus/synth_verify.cpp | 113 +++++++++++------- src/theory/quantifiers/sygus/synth_verify.h | 6 + src/theory/smt_engine_subsolver.cpp | 2 +- 3 files changed, 74 insertions(+), 47 deletions(-) diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 82e356c48..e5bab459d 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -65,22 +65,74 @@ SynthVerify::~SynthVerify() {} Result SynthVerify::verify(Node query, const std::vector& vars, std::vector& mvs) +{ + Node queryp = preprocessQueryInternal(query); + bool finished; + Result r; + do + { + Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; + if (queryp.isConst()) + { + if (!queryp.getConst()) + { + return Result(Result::UNSAT); + } + // sat, but we need to get arbtirary model values below + } + r = checkWithSubsolver(queryp, + vars, + mvs, + d_subOptions, + d_subLogicInfo, + options().quantifiers.sygusVerifyTimeout != 0, + options().quantifiers.sygusVerifyTimeout); + finished = true; + Trace("sygus-engine") << " ...got " << r << std::endl; + // we try to learn models for "sat" and "unknown" here + if (r.getStatus() != Result::UNSAT) + { + if (TraceIsOn("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; + } + // check whether the query is satisfied by the model + if (Configuration::isAssertionBuild()) + { + Assert(vars.size() == mvs.size()); + // 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 = d_tds->rewriteNode(squery); + Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; + // if the query simplifies to false, then something + // went wrong or the answer is unknown (for debugging). + if (squery.isConst() && !squery.getConst()) + { + Assert(r.getStatus() == Result::UNKNOWN) + << "Expected model from verification step to satisfy query"; + } + } + } + } while (!finished); + return r; +} + +Node SynthVerify::preprocessQueryInternal(Node query) { NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-debug") << "pre-rewritten query : " << query << std::endl; // 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 + Trace("cegqi-debug") << "post-rewritten query : " << query << std::endl; + if (!query.isConst()) { // if non-constant, we may need to add recursive function definitions FunDefEvaluator* feval = d_tds->getFunDefEvaluator(); @@ -98,6 +150,7 @@ Result SynthVerify::verify(Node query, qconj.push_back(query); for (const Node& f : syms) { + // get the function definition Node q = feval->getDefinitionFor(f); if (!q.isNull()) { @@ -105,43 +158,11 @@ Result SynthVerify::verify(Node query, } } query = nm->mkAnd(qconj); - Trace("cegqi-debug") << "query is " << query << std::endl; - } - } - Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - query = rewrite(query); - Result r = checkWithSubsolver(query, - vars, - mvs, - d_subOptions, - d_subLogicInfo, - options().quantifiers.sygusVerifyTimeout != 0, - options().quantifiers.sygusVerifyTimeout); - Trace("sygus-engine") << " ...got " << r << std::endl; - if (r.getStatus() == Result::SAT) - { - if (TraceIsOn("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 = rewrite(squery); - Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(options().quantifiers.sygusRecFun - || (squery.isConst() && squery.getConst())); + Trace("cegqi-debug") << "after function definitions, query is " << query + << std::endl; } } - return r; + return query; } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h index 2a4e50b19..37d021032 100644 --- a/src/theory/quantifiers/sygus/synth_verify.h +++ b/src/theory/quantifiers/sygus/synth_verify.h @@ -52,6 +52,12 @@ class SynthVerify : protected EnvObj std::vector& mvs); private: + /** + * Preprocess query internal. This returns the rewritten form of query + * and includes all relevant function definitions, i.e. those that occur + * in query. These are added as top-level conjuncts to the returned formula. + */ + Node preprocessQueryInternal(Node query); /** Pointer to the term database sygus */ TermDbSygus* d_tds; /** The options for subsolver calls */ diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 2cda7d2c3..bb9f4cb2f 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -126,7 +126,7 @@ Result checkWithSubsolver(Node query, initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout); smte->assertFormula(query); r = smte->checkSat(); - if (r.getStatus() == Result::SAT) + if (r.getStatus() == Result::SAT || r.getStatus() == Result::UNKNOWN) { for (const Node& v : vars) { -- 2.30.2