diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-06 10:00:08 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-06 10:00:08 -0600 |
commit | 52e71b709504ed06ced34962692a329f4c8282ce (patch) | |
tree | da64b2bf12fd4f176833a53d36175131799e3c1d /src/theory | |
parent | dcccaec1155c66f2e52cfe823bc9654c46e3832b (diff) |
Support for SyGuS PBE + recursive functions (#3433)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 187 | ||||
-rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.h | 72 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.h | 56 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 10 |
7 files changed, 337 insertions, 32 deletions
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<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::map<Node, FunDefInfo>::const_iterator itf; + std::vector<TNode> 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<Node> 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<Node>& 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 <map> +#include <vector> +#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<Node> d_args; + }; + /** maps functions to the above information */ + std::map<Node, FunDefInfo> 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<Node>& 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<SynthConjecture>( 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<Node, bool, NodeHashFunction> NodeBoolMap; - private: - /** the conjecture formula(s) we are waiting to assign */ - std::vector<Node> d_waiting_conj; - /** The synthesis conjectures that this class is managing. */ - std::vector<std::unique_ptr<SynthConjecture> > 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<Node> d_waiting_conj; + /** The synthesis conjectures that this class is managing. */ + std::vector<std::unique_ptr<SynthConjecture> > 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<TypeNode, std::map<Node, unsigned> >::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<ExtendedRewriter> d_ext_rw; /** evaluator */ std::unique_ptr<Evaluator> d_eval; + /** (recursive) function evaluator utility */ + std::unique_ptr<FunDefEvaluator> d_funDefEval; /** evaluation function unfolding utility */ std::unique_ptr<SygusEvalUnfold> d_eval_unfold; //------------------------------end utilities |