diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 159 |
1 files changed, 159 insertions, 0 deletions
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 <map> +#include <vector> + +#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<bool, Node>; +using BoolNodePairHashFunction = + PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>; +using BoolNodePairMap = + std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>; + +/** 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<Node>& candidates, + std::vector<Node>& lemmas) override; + /** adds the candidate itself to enums */ + void getTermList(const std::vector<Node>& candidates, + std::vector<Node>& 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<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + std::vector<Node>& 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<Node>& vars, + Node lem, + std::vector<Node>& 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<Node> d_enums; + /** map from enumerators to active guards */ + std::map<Node, Node> d_enum_to_active_guard; + /* list of learned refinement lemmas */ + std::vector<Node> 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<Node>& model_guards, + BoolNodePairMap& cache); + +}; /* class CegisUnif */ + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif |