diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-17 14:09:46 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-17 14:09:46 -0500 |
commit | 19cf50fcb832b01bb119dc1cfc31884e4e864f06 (patch) | |
tree | 2c9c0f41307ab5d62df39102571935bd2ea5fff1 /src/theory | |
parent | 19ab3936ef46e93a98a142e0c454659ecc1d1e27 (diff) |
Cegis-specific infrastructure (#1933)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 141 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 63 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 6 |
6 files changed, 165 insertions, 113 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 0aebbe11a..031507c11 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -138,11 +138,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { addedLemma = true; }else{ //this may happen if we eagerly unfold, simplify to true - if( !options::sygusDirectEval() ){ - Trace("cegqi-warn") << " ...FAILED to add candidate!" << std::endl; - }else{ - Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; - } + Trace("cegqi-engine-debug") + << " ...FAILED to add candidate!" << std::endl; } } if( addedLemma ){ diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 47053080a..ec17294f9 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -13,7 +13,9 @@ **/ #include "theory/quantifiers/sygus/cegis.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" +#include "printer/printer.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/theory_engine.h" @@ -27,6 +29,7 @@ namespace theory { namespace quantifiers { Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {} + bool Cegis::initialize(Node n, const std::vector<Node>& candidates, std::vector<Node>& lemmas) @@ -49,7 +52,13 @@ bool Cegis::initialize(Node n, TypeNode bt = d_base_body.getType(); d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples()); } + return processInitialize(n, candidates, lemmas); +} +bool Cegis::processInitialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas) +{ // initialize an enumerator for each candidate for (unsigned i = 0; i < candidates.size(); i++) { @@ -69,9 +78,9 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, { NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; - if (options::sygusCRefEval()) + if (options::sygusRefEval()) { - Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." + Trace("cegqi-engine") << " *** Do refinement lemma evaluation..." << std::endl; // see if any refinement lemma is refuted by evaluation std::vector<Node> cre_lems; @@ -82,8 +91,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, { if (d_qe->addLemma(lem)) { - Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem - << std::endl; + Trace("cegqi-lemma") + << "Cegqi::Lemma : ref evaluation : " << lem << std::endl; addedEvalLemmas = true; } } @@ -91,61 +100,107 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, add the lemmas below as well, in parallel. */ } } - if (!options::sygusDirectEval()) - { - return addedEvalLemmas; - } - Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; - std::vector<Node> eager_terms, eager_vals, eager_exps; - for (unsigned i = 0, size = candidates.size(); i < size; ++i) + if (options::sygusEvalUnfold()) { - Trace("cegqi-debug") << " register " << candidates[i] << " -> " - << candidate_values[i] << std::endl; - d_tds->registerModelValue(candidates[i], - candidate_values[i], - eager_terms, - eager_vals, - eager_exps); - } - Trace("cegqi-debug") << "...produced " << eager_terms.size() - << " eager evaluation lemmas.\n"; - for (unsigned i = 0, size = eager_terms.size(); i < size; ++i) - { - Node lem = nm->mkNode( - OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); - if (d_qe->addLemma(lem)) + Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; + std::vector<Node> eager_terms, eager_vals, eager_exps; + for (unsigned i = 0, size = candidates.size(); i < size; ++i) { - Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem - << std::endl; - addedEvalLemmas = true; + Trace("cegqi-debug") << " register " << candidates[i] << " -> " + << candidate_values[i] << std::endl; + d_tds->registerModelValue(candidates[i], + candidate_values[i], + eager_terms, + eager_vals, + eager_exps); + } + Trace("cegqi-debug") << "...produced " << eager_terms.size() + << " evaluation unfold lemmas.\n"; + for (unsigned i = 0, size = eager_terms.size(); i < size; ++i) + { + Node lem = nm->mkNode( + OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); + if (d_qe->addLemma(lem)) + { + Trace("cegqi-lemma") + << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl; + addedEvalLemmas = true; + } } } return addedEvalLemmas; } -/** construct candidate */ bool Cegis::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) { - if (addEvalLemmas(enums, enum_values)) + if (Trace.isOn("cegis")) { - // it may be repairable - SygusRepairConst* src = d_parent->getRepairConst(); - std::vector<Node> fail_cvs = enum_values; - if (src->repairSolution(candidates, fail_cvs, candidate_values)) + Trace("cegis") << " Enumerators :\n"; + for (unsigned i = 0, size = enums.size(); i < size; ++i) { - return true; + Trace("cegis") << " " << enums[i] << " -> "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, enum_values[i]); + Trace("cegis") << ss.str() << std::endl; } + } + // evaluate on refinement lemmas + bool addedEvalLemmas = addEvalLemmas(enums, enum_values); + + // try to construct candidates + if (!processConstructCandidates(enums, + enum_values, + candidates, + candidate_values, + !addedEvalLemmas, + lems)) + { return false; } - candidate_values.insert( - candidate_values.end(), enum_values.begin(), enum_values.end()); + + if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty()) + { + // if we didn't add a lemma, trying sampling to add a refinement lemma + // that immediately refutes the candidate we just constructed + if (sampleAddRefinementLemma(enums, enum_values, lems)) + { + // restart (should be guaranteed to add evaluation lemmas on this call) + return constructCandidates( + enums, enum_values, candidates, candidate_values, lems); + } + } return true; } +bool Cegis::processConstructCandidates(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + bool satisfiedRl, + std::vector<Node>& lems) +{ + if (satisfiedRl) + { + candidate_values.insert( + candidate_values.end(), enum_values.begin(), enum_values.end()); + return true; + } + SygusRepairConst* src = d_parent->getRepairConst(); + if (src != nullptr) + { + // it may be repairable + std::vector<Node> fail_cvs = enum_values; + Assert(candidates.size() == fail_cvs.size()); + return src->repairSolution(candidates, fail_cvs, candidate_values); + } + return false; +} + void Cegis::addRefinementLemma(Node lem) { d_refinement_lemmas.push_back(lem); @@ -371,21 +426,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, break; } } - // if we didn't add a lemma, trying sampling to add one - if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty()) - { - if (sampleAddRefinementLemma(vs, ms, lems)) - { - // restart (should be guaranteed to add evaluation lemmas - getRefinementEvalLemmas(vs, ms, lems); - } - } } bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, const std::vector<Node>& vals, std::vector<Node>& lems) { + Trace("cegqi-engine") << " *** Do sample add refinement..." << std::endl; if (Trace.isOn("cegis-sample")) { Trace("cegis-sample") << "Check sampling for candidate solution" diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index cbd563e07..e5ee6bc56 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -72,6 +72,23 @@ class Cegis : public SygusModule * formula P( CegConjecture::d_candidates, y ). */ Node d_base_body; + //----------------------------------cegis-implementation-specific + /** do cegis-implementation-specific intialization for this class */ + virtual bool processInitialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas); + /** do cegis-implementation-specific construct candidate + * + * satisfiedRl is whether all refinement lemmas are satisfied under the + * substitution { enums -> enum_values }. + */ + virtual bool processConstructCandidates(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + bool satisfiedRl, + std::vector<Node>& lems); + //----------------------------------end cegis-implementation-specific //-----------------------------------refinement lemmas /** refinement lemmas */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 20f062722..9ae598f83 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -33,9 +33,9 @@ CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) } CegisUnif::~CegisUnif() {} -bool CegisUnif::initialize(Node n, - const std::vector<Node>& candidates, - std::vector<Node>& lemmas) +bool CegisUnif::processInitialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas) { Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; // list of strategy points for unification candidates @@ -99,27 +99,16 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, } } -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) +bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + bool satisfiedRl, + std::vector<Node>& lems) { - if (Trace.isOn("cegis-unif-enum")) - { - Trace("cegis-unif-enum") << " Evaluation heads :\n"; - for (unsigned i = 0, size = enums.size(); i < size; ++i) - { - Trace("cegis-unif-enum") << " " << enums[i] << " -> "; - std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, enum_values[i]); - Trace("cegis-unif-enum") << ss.str() << std::endl; - } - } - // evaluate on refinement lemmas - if (addEvalLemmas(enums, enum_values)) + if (!satisfiedRl) { + // if we didn't satisfy the specification, there is no way to repair return false; } // the unification enumerators (return values, conditions) and their model @@ -137,9 +126,8 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, { for (unsigned index = 0; index < 2; index++) { - Trace("cegis-unif-enum") - << " " << (index == 0 ? "Return values" : "Conditions") << " for " - << e << ":\n"; + Trace("cegis") << " " << (index == 0 ? "Return values" : "Conditions") + << " for " << e << ":\n"; // get the current unification enumerators d_u_enum_manager.getEnumeratorsForStrategyPt( e, unif_enums[index][e], index); @@ -147,13 +135,13 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, for (const Node& eu : unif_enums[index][e]) { Node m_eu = d_parent->getModelValue(eu); - if (Trace.isOn("cegis-unif-enum")) + if (Trace.isOn("cegis")) { - Trace("cegis-unif-enum") << " " << eu << " -> "; + Trace("cegis") << " " << eu << " -> "; std::stringstream ss; Printer::getPrinter(options::outputLanguage()) ->toStreamSygus(ss, m_eu); - Trace("cegis-unif-enum") << ss.str() << std::endl; + Trace("cegis") << ss.str() << std::endl; } unif_values[index][e].push_back(m_eu); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ecaec4129..5c2c11e4d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -183,10 +183,6 @@ class CegisUnif : public Cegis public: CegisUnif(QuantifiersEngine* qe, CegConjecture* p); ~CegisUnif(); - /** initialize this class */ - bool initialize(Node n, - const std::vector<Node>& candidates, - std::vector<Node>& lemmas) override; /** Retrieves enumerators for constructing solutions * * Non-unification candidates have themselves as enumerators, while for @@ -195,33 +191,6 @@ class CegisUnif : public Cegis */ void getTermList(const std::vector<Node>& candidates, std::vector<Node>& enums) override; - /** Tries to build new candidate solutions with new enumerated expressions - * - * This function relies on a data-driven unification-based approach for - * constructing solutions for the functions-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; /** Communicates refinement lemma to unification utility and external modules * @@ -249,6 +218,38 @@ class CegisUnif : public Cegis Node getNextDecisionRequest(unsigned& priority) override; private: + /** do cegis-implementation-specific intialization for this class */ + bool processInitialize(Node n, + const std::vector<Node>& candidates, + std::vector<Node>& lemmas) override; + /** Tries to build new candidate solutions with new enumerated expressions + * + * This function relies on a data-driven unification-based approach for + * constructing solutions for the functions-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 processConstructCandidates(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + const std::vector<Node>& candidates, + std::vector<Node>& candidate_values, + bool satisfiedRl, + std::vector<Node>& lems) override; /** * Sygus unif utility. This class implements the core algorithm (e.g. decision * tree learning) that this module relies upon. diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 0b7841170..b530edeaa 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1261,7 +1261,8 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { void TermDbSygus::registerEvalTerm( Node n ) { - if( options::sygusDirectEval() ){ + if (options::sygusEvalUnfold()) + { if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ TypeNode tn = n[0].getType(); if( tn.isDatatype() ){ @@ -1344,7 +1345,8 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms Node expn; // unfold? bool do_unfold = false; - if( options::sygusUnfoldBool() ){ + if (options::sygusEvalUnfoldBool()) + { if( bTerm.getKind()==ITE || bTerm.getType().isBoolean() ){ do_unfold = true; } |