From: Haniel Barbosa Date: Fri, 27 Apr 2018 19:33:01 +0000 (-0500) Subject: New module for synthesizing functions in a data-driven SyGuS approach (#1819) X-Git-Tag: cvc5-1.0.0~5119 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=79296a59e00efe5b00496a251005d01dbeddcd48;p=cvc5.git New module for synthesizing functions in a data-driven SyGuS approach (#1819) --- diff --git a/src/Makefile.am b/src/Makefile.am index 289ed11d4..80bd082d6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -459,6 +459,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/skolemize.h \ theory/quantifiers/sygus/cegis.cpp \ theory/quantifiers/sygus/cegis.h \ + theory/quantifiers/sygus/cegis_unif.cpp \ + theory/quantifiers/sygus/cegis_unif.h \ theory/quantifiers/sygus/ce_guided_conjecture.cpp \ theory/quantifiers/sygus/ce_guided_conjecture.h \ theory/quantifiers/sygus/ce_guided_instantiation.cpp \ @@ -487,6 +489,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_unif.h \ theory/quantifiers/sygus/sygus_unif_io.cpp \ theory/quantifiers/sygus/sygus_unif_io.h \ + theory/quantifiers/sygus/sygus_unif_rl.cpp \ + theory/quantifiers/sygus/sygus_unif_rl.h \ theory/quantifiers/sygus/sygus_unif_strat.cpp \ theory/quantifiers/sygus/sygus_unif_strat.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b8ddd6d31..2f911bdd1 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -967,6 +967,14 @@ header = "options/quantifiers_options.h" default = "true" help = "sygus advanced pruning based on examples" +[[option]] + name = "sygusUnif" + category = "regular" + long = "sygus-unif" + type = "bool" + default = "false" + help = "Unification-based function synthesis" + [[option]] name = "sygusQePreproc" category = "regular" diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 6914fc66f..db641a82e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -42,6 +42,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_ceg_gc(new CegGrammarConstructor(qe, this)), d_ceg_pbe(new CegConjecturePbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), + d_ceg_cegisUnif(new CegisUnif(qe, this)), d_master(nullptr), d_refine_count(0), d_syntax_guided(false) @@ -50,6 +51,10 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) { d_modules.push_back(d_ceg_pbe.get()); } + if (options::sygusUnif()) + { + d_modules.push_back(d_ceg_cegisUnif.get()); + } d_modules.push_back(d_ceg_cegis.get()); } diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 5d7f082d8..97cc9df1e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -23,6 +23,7 @@ #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" +#include "theory/quantifiers/sygus/cegis_unif.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" @@ -141,6 +142,8 @@ private: std::unique_ptr d_ceg_pbe; /** CEGIS module */ std::unique_ptr d_ceg_cegis; + /** CEGIS UNIF module */ + std::unique_ptr d_ceg_cegisUnif; /** the set of active modules (subset of the above list) */ std::vector d_modules; /** master module diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp new file mode 100644 index 000000000..f7d970ddf --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -0,0 +1,240 @@ +/********************* */ +/*! \file cegis_unif.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 class for cegis with unification techniques + **/ + +#include "theory/quantifiers/sygus/cegis_unif.h" + +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/sygus_unif_rl.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) + : SygusModule(qe, p) +{ + d_tds = d_qe->getTermDatabaseSygus(); +} + +CegisUnif::~CegisUnif() {} +bool CegisUnif::initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) +{ + Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; + Assert(candidates.size() > 0); + if (candidates.size() > 1) + { + return false; + } + d_candidate = candidates[0]; + Trace("cegis-unif") << "Initialize unif utility for " << d_candidate + << "...\n"; + d_sygus_unif.initialize(d_qe, d_candidate, d_enums, lemmas); + Assert(!d_enums.empty()); + Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for " + << d_candidate << "...\n"; + /* initialize the enumerators */ + for (const Node& e : d_enums) + { + d_tds->registerEnumerator(e, d_candidate, d_parent, true); + Node g = d_tds->getActiveGuardForEnumerator(e); + d_enum_to_active_guard[e] = g; + } + return true; +} + +void CegisUnif::getTermList(const std::vector& candidates, + std::vector& terms) +{ + Assert(candidates.size() == 1); + Valuation& valuation = d_qe->getValuation(); + for (const Node& e : d_enums) + { + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + /* Get whether the active guard for this enumerator is if so, then there may + exist more values for it, and hence we add it to terms. */ + Node gstatus = valuation.getSatValue(g); + if (!gstatus.isNull() && gstatus.getConst()) + { + terms.push_back(e); + } + } +} + +bool CegisUnif::constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) +{ + Assert(enums.size() == enum_values.size()); + if (enums.empty()) + { + return false; + } + unsigned min_term_size = 0; + std::vector enum_consider; + Trace("cegis-unif-enum") << "Register new enumerated values :\n"; + for (unsigned i = 0, size = enums.size(); i < size; ++i) + { + Trace("cegis-unif-enum") << " " << enums[i] << " -> " << enum_values[i] + << std::endl; + unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + if (i == 0 || sz < min_term_size) + { + enum_consider.clear(); + min_term_size = sz; + enum_consider.push_back(i); + } + else if (sz == min_term_size) + { + enum_consider.push_back(i); + } + } + /* only consider the enumerators that are at minimum size (for fairness) */ + Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / " + << enums.size() << std::endl; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i) + { + unsigned j = enum_consider[i]; + Node e = enums[j]; + Node v = enum_values[j]; + std::vector enum_lems; + d_sygus_unif.notifyEnumeration(e, v, enum_lems); + /* the lemmas must be guarded by the active guard of the enumerator */ + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + for (unsigned j = 0, size = enum_lems.size(); j < size; ++j) + { + enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + } + lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); + } + /* build candidate solution */ + Assert(candidates.size() == 1); + Node vc = d_sygus_unif.constructSolution(); + if (vc.isNull()) + { + return false; + } + candidate_values.push_back(vc); + return true; +} + +Node CegisUnif::purifyLemma(Node n, + bool ensureConst, + std::vector& model_guards, + BoolNodePairMap& cache) +{ + Trace("cegis-unif-purify") << "PurifyLemma : " << n << "\n"; + BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n)); + if (it != cache.end()) + { + Trace("cegis-unif-purify") << "... already visited " << n << "\n"; + return it->second; + } + /* Recurse */ + unsigned size = n.getNumChildren(); + Kind k = n.getKind(); + bool fapp = k == APPLY_UF && size > 0 && n[0] == d_candidate; + bool childChanged = false; + std::vector children; + for (unsigned i = 0; i < size; ++i) + { + if (i == 0 && fapp) + { + children.push_back(n[0]); + continue; + } + Node child = purifyLemma(n[i], ensureConst || fapp, model_guards, cache); + children.push_back(child); + childChanged = childChanged || child != n[i]; + } + Node nb; + if (childChanged) + { + if (n.hasOperator()) + { + children.insert(children.begin(), n.getOperator()); + } + nb = NodeManager::currentNM()->mkNode(k, children); + Trace("cegis-unif-purify") << "PurifyLemma : transformed " << n << " into " + << nb << "\n"; + } + else + { + nb = n; + } + /* get model value of non-top level applications of d_candidate */ + if (ensureConst && fapp) + { + Node nv = d_parent->getModelValue(nb); + Trace("cegis-unif-purify") << "PurifyLemma : model value for " << nb + << " is " << nv << "\n"; + /* test if different, then update model_guards */ + if (nv != nb) + { + Trace("cegis-unif-purify") << "PurifyLemma : adding model eq\n"; + model_guards.push_back( + NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate()); + nb = nv; + } + } + nb = Rewriter::rewrite(nb); + /* every non-top level application of function-to-synthesize must be reduced + to a concrete constant */ + Assert(!ensureConst || nb.isConst()); + Trace("cegis-unif-purify") << "... caching [" << n << "] = " << nb << "\n"; + cache[BoolNodePair(ensureConst, n)] = nb; + return nb; +} + +void CegisUnif::registerRefinementLemma(const std::vector& vars, + Node lem, + std::vector& lems) +{ + Node plem; + std::vector model_guards; + BoolNodePairMap cache; + Trace("cegis-unif") << "Registering lemma at CegisUnif : " << lem << "\n"; + /* Make the purified lemma which will guide the unification utility. */ + plem = purifyLemma(lem, false, model_guards, cache); + if (!model_guards.empty()) + { + model_guards.push_back(plem); + plem = NodeManager::currentNM()->mkNode(OR, model_guards); + } + plem = Rewriter::rewrite(plem); + Trace("cegis-unif") << "Purified lemma : " << plem << "\n"; + d_refinement_lemmas.push_back(plem); + /* Notify lemma to unification utility */ + d_sygus_unif.addRefLemma(plem); + /* Make the refinement lemma and add it to lems. This lemma is guarded by the + parent's guard, which has the semantics "this conjecture has a solution", + hence this lemma states: if the parent conjecture has a solution, it + satisfies the specification for the given concrete point. */ + /* Store lemma for external modules */ + lems.push_back( + NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem)); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h new file mode 100644 index 000000000..78586cd9c --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -0,0 +1,159 @@ +/********************* */ +/*! \file cegis_unif.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 cegis with unification techinques + **/ +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H + +#include +#include + +#include "theory/quantifiers/sygus/sygus_module.h" +#include "theory/quantifiers/sygus/sygus_unif_rl.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +using BoolNodePair = std::pair; +using BoolNodePairHashFunction = + PairHashFunction; +using BoolNodePairMap = + std::unordered_map; + +/** Synthesizes functions in a data-driven SyGuS approach + * + * Data is derived from refinement lemmas generated through the regular CEGIS + * approach. SyGuS is used to generate terms for classifying the data + * (e.g. using decision tree learning) and thus generate a candidate for a + * function-to-synthesize. + * + * This approach is inspired by the divide and conquer synthesis through + * unification approach by Alur et al. TACAS 2017, by ICE-based invariant + * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016 + * + * This module mantains a function-to-synthesize and a set of term + * enumerators. When new terms are enumerated it tries to learn a new candidate + * function, which is verified outside this module. If verification fails a + * refinement lemma is generated, which this module sends to the utility that + * learns candidates. + */ +class CegisUnif : public SygusModule +{ + public: + CegisUnif(QuantifiersEngine* qe, CegConjecture* p); + ~CegisUnif(); + /** initialize this class + * + * The module takes ownership of a conjecture when it contains a single + * function-to-synthesize + */ + bool initialize(Node n, + const std::vector& candidates, + std::vector& lemmas) override; + /** adds the candidate itself to enums */ + void getTermList(const std::vector& candidates, + std::vector& enums) override; + /** Tries to build a new candidate solution with new enumerated expresion + * + * This function relies on a data-driven unification-based approach for + * constructing a solutions for the function-to-synthesize. See SygusUnifRl + * for more details. + * + * Calls to this function are such that terms is the list of active + * enumerators (returned by getTermList), and term_values are their current + * model values. This function registers { terms -> terms_values } in + * the database of values that have been enumerated, which are in turn used + * for constructing candidate solutions when possible. + * + * This function also excludes models where (terms = terms_values) by adding + * blocking clauses to lems. For example, for grammar: + * A -> A+A | x | 1 | 0 + * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds: + * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 ) + * to lems, where G is active guard of the enumerator d (see + * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause + * indicates that d should not be given the model value +( x, 1 ) anymore, + * since { d -> +( x, 1 ) } has now been added to the database of this class. + */ + bool constructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + std::vector& lems) override; + + /** Communicate refinement lemma to unification utility and external modules + * + * For the lemma to be sent to the external modules it adds a guard from the + * parent conjecture which establishes that if the conjecture has a solution + * then it must satisfy this refinement lemma + * + * For the lemma to be sent to the unification utility it purifies the + * arguments of the function-to-synthensize such that all of its applications + * are over concrete values. E.g.: + * f(f(f(0))) > 1 + * becomes + * f(0) != c1 v f(c1) != c2 v f(c2) > 1 + * in which c1 and c2 are concrete integer values + * + * Note that the lemma is in the deep embedding, which means that the above + * example would actually correspond to + * eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1 + * in which d is the deep embedding of the function-to-synthesize f + */ + void registerRefinementLemma(const std::vector& vars, + Node lem, + std::vector& lems) override; + + private: + /** sygus term database of d_qe */ + TermDbSygus* d_tds; + /** + * Sygus unif utility. This class implements the core algorithm (e.g. decision + * tree learning) that this module relies upon. + */ + SygusUnifRl d_sygus_unif; + /* Function-to-synthesize (in deep embedding) */ + Node d_candidate; + /** + * list of enumerators being used to build solutions for candidate by the + * above utility. + */ + std::vector d_enums; + /** map from enumerators to active guards */ + std::map d_enum_to_active_guard; + /* list of learned refinement lemmas */ + std::vector d_refinement_lemmas; + /** + * This is called on the refinement lemma and will replace the arguments of the + * function-to-synthesize by their model values (constants). + * + * When the traversal hits a function application of the function-to-synthesize + * it will proceed to ensure that the arguments of that function application + * are constants (the ensureConst becomes "true"). It populates a vector of + * guards with the (negated) equalities between the original arguments and + * their model values. + */ + Node purifyLemma(Node n, + bool ensureConst, + std::vector& model_guards, + BoolNodePairMap& cache); + +}; /* class CegisUnif */ + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp new file mode 100644 index 000000000..bac46997d --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -0,0 +1,51 @@ +/********************* */ +/*! \file sygus_unif_rl.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 sygus_unif_rl + **/ + +#include "theory/quantifiers/sygus/sygus_unif_rl.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusUnifRl::SygusUnifRl() {} + +SygusUnifRl::~SygusUnifRl() {} + +void SygusUnifRl::initialize(QuantifiersEngine* qe, + Node f, + std::vector& enums, + std::vector& lemmas) +{ + SygusUnif::initialize(qe, f, enums, lemmas); +} + +void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector& lemmas) +{ +} + +void SygusUnifRl::addRefLemma(Node lemma) {} + +void SygusUnifRl::initializeConstructSol() {} + +Node SygusUnifRl::constructSol(Node e, NodeRole nrole, int ind) +{ + return Node::null(); +} + + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h new file mode 100644 index 000000000..8dc1906fb --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file sygus_unif_rl.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 sygus_unif_rl + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H + +#include +#include "theory/quantifiers/sygus/sygus_unif.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Sygus unification Refinement Lemmas utility + * + * This class implement synthesis-by-unification, where the specification is a + * set of refinement lemmas. With respect to SygusUnif, it's main interface + * function is addExample, which adds a refinement lemma to the specification. + */ +class SygusUnifRl : public SygusUnif +{ + public: + SygusUnifRl(); + ~SygusUnifRl(); + + /** initialize */ + void initialize(QuantifiersEngine* qe, + Node f, + std::vector& enums, + std::vector& lemmas) override; + /** Notify enumeration */ + void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; + /** add refinement lemma + * + * This adds a lemma to the specification for f. + */ + void addRefLemma(Node lemma); + + protected: + /** set of refinmente lemmas */ + std::vector d_refLemmas; + /** initialize construct solution */ + void initializeConstructSol() override; + /** construct solution */ + Node constructSol(Node e, NodeRole nrole, int ind) override; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */