From 52e71b709504ed06ced34962692a329f4c8282ce Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Nov 2019 10:00:08 -0600 Subject: [PATCH] Support for SyGuS PBE + recursive functions (#3433) --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 8 + src/theory/quantifiers/fun_def_evaluator.cpp | 187 ++++++++++++++++++ src/theory/quantifiers/fun_def_evaluator.h | 72 +++++++ .../quantifiers/sygus/synth_conjecture.cpp | 3 +- src/theory/quantifiers/sygus/synth_engine.cpp | 14 +- src/theory/quantifiers/sygus/synth_engine.h | 56 +++--- .../quantifiers/sygus/term_database_sygus.cpp | 27 ++- .../quantifiers/sygus/term_database_sygus.h | 10 + test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/rec-fun-sygus.sy | 21 ++ 11 files changed, 369 insertions(+), 32 deletions(-) create mode 100644 src/theory/quantifiers/fun_def_evaluator.cpp create mode 100644 src/theory/quantifiers/fun_def_evaluator.h create mode 100644 test/regress/regress1/sygus/rec-fun-sygus.sy diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 77db3b4db..4f64760e0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -506,6 +506,8 @@ libcvc4_add_sources( theory/quantifiers/fmf/model_builder.h theory/quantifiers/fmf/model_engine.cpp theory/quantifiers/fmf/model_engine.h + theory/quantifiers/fun_def_evaluator.cpp + theory/quantifiers/fun_def_evaluator.h theory/quantifiers/fun_def_process.cpp theory/quantifiers/fun_def_process.h theory/quantifiers/inst_match.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 89ccd90b2..338f5544f 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1213,6 +1213,14 @@ header = "options/quantifiers_options.h" default = "false" help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant" +[[option]] + name = "sygusRecFun" + category = "regular" + long = "sygus-rec-fun" + type = "bool" + default = "false" + help = "enable efficient support for recursive functions in sygus grammars" + # Internal uses of sygus [[option]] diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp new file mode 100644 index 000000000..83debe0d9 --- /dev/null +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -0,0 +1,187 @@ +/********************* */ +/*! \file fun_def_evaluator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief Implementation of techniques for evaluating terms with recursively + ** defined functions. + **/ + +#include "theory/quantifiers/fun_def_evaluator.h" + +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +FunDefEvaluator::FunDefEvaluator() {} + +void FunDefEvaluator::assertDefinition(Node q) +{ + Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl; + Node h = QuantAttributes::getFunDefHead(q); + if (h.isNull()) + { + // not a function definition + return; + } + // h possibly with zero arguments? + Node f = h.hasOperator() ? h.getOperator() : h; + Assert(d_funDefMap.find(f) == d_funDefMap.end()) + << "FunDefEvaluator::assertDefinition: function already defined"; + FunDefInfo& fdi = d_funDefMap[f]; + 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()); + Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with " + << fdi.d_args << " / " << fdi.d_body << std::endl; +} + +Node FunDefEvaluator::evaluate(Node n) const +{ + // should do standard rewrite before this call + Assert(Rewriter::rewrite(n) == n); + Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::map::const_iterator itf; + std::vector visit; + TNode cur; + TNode curEval; + Node f; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl; + + if (it == visited.end()) + { + if (cur.isConst()) + { + Trace("fd-eval-debug") << "constant " << cur << std::endl; + visited[cur] = cur; + } + else + { + Trace("fd-eval-debug") << "recurse " << cur << std::endl; + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else + { + curEval = it->second; + if (curEval.isNull()) + { + Trace("fd-eval-debug") << "from arguments " << cur << std::endl; + Node ret = cur; + bool childChanged = false; + std::vector children; + Kind ck = cur.getKind(); + // If a parameterized node that is not APPLY_UF (which is handled below, + // we add it to the children vector. + if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (cur.getKind() == APPLY_UF) + { + // need to evaluate it + f = cur.getOperator(); + itf = d_funDefMap.find(f); + if (itf == d_funDefMap.end()) + { + Trace("fd-eval") << "FunDefEvaluator: no definition for " << f + << ", FAIL" << std::endl; + return Node::null(); + } + // get the function definition + Node sbody = itf->second.d_body; + const std::vector& args = itf->second.d_args; + if (!args.empty()) + { + // invoke it on arguments + sbody = sbody.substitute( + args.begin(), args.end(), children.begin(), children.end()); + // rewrite it + sbody = Rewriter::rewrite(sbody); + } + // our result is the result of the body + visited[cur] = sbody; + // If its not constant, we push back self and the substituted body. + // Thus, we evaluate the body first; our result will be the result of + // evaluating the body. + if (!sbody.isConst()) + { + visit.push_back(cur); + visit.push_back(sbody); + } + } + else + { + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + ret = Rewriter::rewrite(ret); + } + if (!ret.isConst()) + { + Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret + << ", FAIL" << std::endl; + // failed, possibly due to free variable + return Node::null(); + } + visited[cur] = ret; + } + } + else if (!curEval.isConst()) + { + Trace("fd-eval-debug") << "from body " << cur << std::endl; + // we had to evaluate our body, which should have a definition now + it = visited.find(curEval); + Assert(it != visited.end()); + // our definition is the result of the body + visited[cur] = it->second; + Assert(it->second.isConst()); + } + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + Assert(visited.find(n)->second.isConst()); + Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n] + << std::endl; + return visited[n]; +} + +bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); } + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h new file mode 100644 index 000000000..ad08dfa84 --- /dev/null +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file fun_def_evaluator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief Techniques for evaluating terms with recursively defined functions. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H +#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H + +#include +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * Techniques for evaluating recursively defined functions. + */ +class FunDefEvaluator +{ + public: + FunDefEvaluator(); + ~FunDefEvaluator() {} + /** + * Assert definition of a (recursive) function definition given by quantified + * formula q. + */ + void assertDefinition(Node q); + /** + * Simplify node based on the (recursive) function definitions known by this + * class. If n cannot be simplified to a constant, then this method returns + * null. + */ + Node evaluate(Node n) const; + /** + * Has a call to assertDefinition been made? If this returns false, then + * the evaluate method is the same as calling the rewriter, and returning + * false if the result is non-constant. + */ + bool hasDefinitions() const; + + private: + /** information cached per function definition */ + class FunDefInfo + { + public: + /** the body */ + Node d_body; + /** the formal argument list */ + std::vector d_args; + }; + /** maps functions to the above information */ + std::map d_funDefMap; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 5edd18464..6e69715ef 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -539,7 +539,8 @@ bool SynthConjecture::doCheck(std::vector& lems) return false; } - lem = Rewriter::rewrite(lem); + // simplify the lemma based on the term database sygus utility + lem = d_tds->rewriteNode(lem); // eagerly unfold applications of evaluation function Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; // record the instantiation diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 88d00ce3a..9f6954416 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -33,7 +33,7 @@ namespace theory { namespace quantifiers { SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) - : QuantifiersModule(qe) + : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus()) { d_conjs.push_back(std::unique_ptr( new SynthConjecture(d_quantEngine, this))); @@ -274,6 +274,8 @@ void SynthEngine::assignConjecture(Node q) void SynthEngine::registerQuantifier(Node q) { + Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q + << std::endl; if (d_quantEngine->getOwner(q) == this) { Trace("cegqi") << "Register conjecture : " << q << std::endl; @@ -287,9 +289,15 @@ void SynthEngine::registerQuantifier(Node q) assignConjecture(q); } } - else + if (options::sygusRecFun()) { - Trace("cegqi-debug") << "Register quantifier : " << q << std::endl; + if (d_quantEngine->getQuantAttributes()->isFunDef(q)) + { + // If it is a recursive function definition, add it to the function + // definition evaluator class. + FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); + fde->assertDefinition(q); + } } } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 20e4deec6..1eca56959 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -30,33 +30,6 @@ class SynthEngine : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; - private: - /** the conjecture formula(s) we are waiting to assign */ - std::vector d_waiting_conj; - /** The synthesis conjectures that this class is managing. */ - std::vector > d_conjs; - /** - * The first conjecture in the above vector. We track this conjecture - * so that a synthesis conjecture can be preregistered during a call to - * preregisterAssertion. - */ - SynthConjecture* d_conj; - /** assign quantified formula q as a conjecture - * - * This method either assigns q to a synthesis conjecture object in d_conjs, - * or otherwise reduces q to an equivalent form. This method does the latter - * if this class determines that it would rather rewrite q to an equivalent - * form r (in which case this method returns the lemma q <=> r). An example of - * this is the quantifier elimination step option::sygusQePreproc(). - */ - void assignConjecture(Node q); - /** check conjecture - * - * This method returns true if the conjecture is finished processing solutions - * for this call to SynthEngine::check(). - */ - bool checkConjecture(SynthConjecture* conj); - public: SynthEngine(QuantifiersEngine* qe, context::Context* c); ~SynthEngine(); @@ -113,6 +86,35 @@ class SynthEngine : public QuantifiersModule ~Statistics(); }; /* class SynthEngine::Statistics */ Statistics d_statistics; + + private: + /** term database sygus of d_qe */ + TermDbSygus* d_tds; + /** the conjecture formula(s) we are waiting to assign */ + std::vector d_waiting_conj; + /** The synthesis conjectures that this class is managing. */ + std::vector > d_conjs; + /** + * The first conjecture in the above vector. We track this conjecture + * so that a synthesis conjecture can be preregistered during a call to + * preregisterAssertion. + */ + SynthConjecture* d_conj; + /** assign quantified formula q as a conjecture + * + * This method either assigns q to a synthesis conjecture object in d_conjs, + * or otherwise reduces q to an equivalent form. This method does the latter + * if this class determines that it would rather rewrite q to an equivalent + * form r (in which case this method returns the lemma q <=> r). An example of + * this is the quantifier elimination step option::sygusQePreproc(). + */ + void assignConjecture(Node q); + /** check conjecture + * + * This method returns true if the conjecture is finished processing solutions + * for this call to SynthEngine::check(). + */ + bool checkConjecture(SynthConjecture* conj); }; /* class SynthEngine */ } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index d17c343f4..84a9c2405 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -50,6 +50,7 @@ TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe) d_syexp(new SygusExplain(this)), d_ext_rw(new ExtendedRewriter(true)), d_eval(new Evaluator), + d_funDefEval(new FunDefEvaluator), d_eval_unfold(new SygusEvalUnfold(this)) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -725,6 +726,28 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) return d_tinfo[tn]; } +Node TermDbSygus::rewriteNode(Node n) const +{ + Node res = Rewriter::rewrite(n); + if (options::sygusRecFun()) + { + if (d_funDefEval->hasDefinitions()) + { + // If recursive functions are enabled, then we use the recursive function + // evaluation utility. + Node fres = d_funDefEval->evaluate(res); + if (!fres.isNull()) + { + return fres; + } + // It may have failed, in which case there are undefined symbols in res. + // In this case, we revert to the result of rewriting in the return + // statement below. + } + } + return res; +} + unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel) { std::map >::iterator itsw = @@ -1061,7 +1084,9 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return res; } res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end()); - return Rewriter::rewrite(res); + // Call the rewrite node function, which may involve recursive function + // evaluation. + return rewriteNode(res); } Node TermDbSygus::evaluateWithUnfolding( diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index c591400e1..0ec883537 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -21,6 +21,7 @@ #include "theory/evaluator.h" #include "theory/quantifiers/extended_rewrite.h" +#include "theory/quantifiers/fun_def_evaluator.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/type_info.h" @@ -77,6 +78,8 @@ class TermDbSygus { ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } /** get the evaluator */ Evaluator* getEvaluator() { return d_eval.get(); } + /** (recursive) function evaluator utility */ + FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); } /** evaluation unfolding utility */ SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); } //------------------------------end utilities @@ -302,6 +305,11 @@ class TermDbSygus { * (a subfield type of) a type that has been registered to this class. */ SygusTypeInfo& getTypeInfo(TypeNode tn); + /** + * Rewrite the given node using the utilities in this class. This may + * involve (recursive function) evaluation. + */ + Node rewriteNode(Node n) const; /** print to sygus stream n on trace c */ static void toStreamSygus(const char* c, Node n); @@ -317,6 +325,8 @@ class TermDbSygus { std::unique_ptr d_ext_rw; /** evaluator */ std::unique_ptr d_eval; + /** (recursive) function evaluator utility */ + std::unique_ptr d_funDefEval; /** evaluation function unfolding utility */ std::unique_ptr d_eval_unfold; //------------------------------end utilities diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7765591f8..c98dd1be2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1736,6 +1736,7 @@ set(regress_1_tests regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 regress1/sygus/real-grammar.sy + regress1/sygus/rec-fun-sygus.sy regress1/sygus/re-concat.sy regress1/sygus/repair-const-rl.sy regress1/sygus/simple-regexp.sy diff --git a/test/regress/regress1/sygus/rec-fun-sygus.sy b/test/regress/regress1/sygus/rec-fun-sygus.sy new file mode 100644 index 000000000..13d4782d4 --- /dev/null +++ b/test/regress/regress1/sygus/rec-fun-sygus.sy @@ -0,0 +1,21 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 + +(set-logic ALL) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(define-fun-rec sum ((x List)) Int (ite ((_ is nil) x) 0 (+ (head x) (sum (tail x))))) +(define-fun-rec size ((x List)) Int (ite ((_ is nil) x) 0 (+ 1 (size (tail x))))) + +(synth-fun f ((x List)) Int + ((I Int) (L List)) + ((I Int ((+ I I) (sum L) (size L) 0 1)) + (L List (x)))) + +(constraint (= (f (cons 3 (cons 4 (cons 5 nil)))) 15)) +(constraint (= (f (cons 3 (cons (- 4) (cons 5 nil)))) 7)) +(constraint (= (f (cons 5 (cons 5 nil))) 12)) +(constraint (= (f (cons 0 (cons 0 (cons 0 (cons 0 (cons 0 (cons 0 nil))))))) 6)) +(constraint (= (f (cons (- 2) (cons 0 nil))) 0)) +(check-synth) -- 2.30.2