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 \
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 \
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"
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)
{
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());
}
#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"
std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
/** CEGIS module */
std::unique_ptr<Cegis> d_ceg_cegis;
+ /** CEGIS UNIF module */
+ std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
/** the set of active modules (subset of the above list) */
std::vector<SygusModule*> d_modules;
/** master module
--- /dev/null
+/********************* */
+/*! \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<Node>& candidates,
+ std::vector<Node>& 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<Node>& candidates,
+ std::vector<Node>& 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<bool>())
+ {
+ terms.push_back(e);
+ }
+ }
+}
+
+bool CegisUnif::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)
+{
+ Assert(enums.size() == enum_values.size());
+ if (enums.empty())
+ {
+ return false;
+ }
+ unsigned min_term_size = 0;
+ std::vector<unsigned> 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<Node> 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<Node>& 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<Node> 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<Node>& vars,
+ Node lem,
+ std::vector<Node>& lems)
+{
+ Node plem;
+ std::vector<Node> 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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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<Node>& enums,
+ std::vector<Node>& lemmas)
+{
+ SygusUnif::initialize(qe, f, enums, lemmas);
+}
+
+void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& 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 */
--- /dev/null
+/********************* */
+/*! \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 <map>
+#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<Node>& enums,
+ std::vector<Node>& lemmas) override;
+ /** Notify enumeration */
+ void notifyEnumeration(Node e, Node v, std::vector<Node>& 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<Node> 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 */
projects / cvc5.git / commitdiff