From 19cf50fcb832b01bb119dc1cfc31884e4e864f06 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 May 2018 14:09:46 -0500 Subject: [PATCH] Cegis-specific infrastructure (#1933) --- src/options/quantifiers_options.toml | 23 +-- .../sygus/ce_guided_instantiation.cpp | 7 +- src/theory/quantifiers/sygus/cegis.cpp | 141 ++++++++++++------ src/theory/quantifiers/sygus/cegis.h | 17 +++ src/theory/quantifiers/sygus/cegis_unif.cpp | 44 ++---- src/theory/quantifiers/sygus/cegis_unif.h | 63 ++++---- .../quantifiers/sygus/term_database_sygus.cpp | 6 +- test/regress/Makefile.tests | 1 + test/regress/regress1/sygus/VC22_a.sy | 1 + .../regress1/sygus/find_sc_bvult_bvnot.sy | 74 +++++++++ 10 files changed, 248 insertions(+), 129 deletions(-) create mode 100644 test/regress/regress1/sygus/find_sc_bvult_bvnot.sy diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 715b0c286..691b2fef4 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1058,41 +1058,32 @@ header = "options/quantifiers_options.h" help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures" [[option]] - name = "sygusDirectEval" + name = "sygusEvalUnfold" category = "regular" - long = "sygus-direct-eval" + long = "sygus-eval-unfold" type = "bool" default = "true" read_only = true - help = "direct unfolding of evaluation functions" + help = "do unfolding of sygus evaluation functions" [[option]] - name = "sygusUnfoldBool" + name = "sygusEvalUnfoldBool" category = "regular" - long = "sygus-unfold-bool" + long = "sygus-eval-unfold-bool" type = "bool" default = "true" read_only = true help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas" [[option]] - name = "sygusCRefEval" + name = "sygusRefEval" category = "regular" - long = "sygus-cref-eval" + long = "sygus-ref-eval" type = "bool" default = "true" read_only = true help = "direct evaluation of refinement lemmas for conflict analysis" -[[option]] - name = "sygusCRefEvalMinExp" - category = "regular" - long = "sygus-cref-eval-min-exp" - type = "bool" - default = "true" - read_only = true - help = "use min explain for direct evaluation of refinement lemmas for conflict analysis" - [[option]] name = "sygusStream" category = "regular" 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& candidates, std::vector& 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& candidates, + std::vector& 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& 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 cre_lems; @@ -82,8 +91,8 @@ bool Cegis::addEvalLemmas(const std::vector& 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& candidates, add the lemmas below as well, in parallel. */ } } - if (!options::sygusDirectEval()) - { - return addedEvalLemmas; - } - Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; - std::vector 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 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& enums, const std::vector& enum_values, const std::vector& candidates, std::vector& candidate_values, std::vector& lems) { - if (addEvalLemmas(enums, enum_values)) + if (Trace.isOn("cegis")) { - // it may be repairable - SygusRepairConst* src = d_parent->getRepairConst(); - std::vector 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& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& 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 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& 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& candidates, const std::vector& vals, std::vector& 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& candidates, + std::vector& 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& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& 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& candidates, - std::vector& lemmas) +bool CegisUnif::processInitialize(Node n, + const std::vector& candidates, + std::vector& 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& candidates, } } -bool CegisUnif::constructCandidates(const std::vector& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - std::vector& lems) +bool CegisUnif::processConstructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& 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& 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& 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& candidates, - std::vector& 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& candidates, std::vector& 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& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - std::vector& 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& candidates, + std::vector& 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& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& 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; } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c0f1cf315..f8fdd4a18 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1480,6 +1480,7 @@ REG1_TESTS = \ regress1/sygus/dt-test-ns.sy \ regress1/sygus/dup-op.sy \ regress1/sygus/fg_polynomial3.sy \ + regress1/sygus/find_sc_bvult_bvnot.sy \ regress1/sygus/hd-01-d1-prog.sy \ regress1/sygus/hd-19-d1-prog-dup-op.sy \ regress1/sygus/hd-sdiv.sy \ diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy index 32e4723aa..ce437bc34 100644 --- a/test/regress/regress1/sygus/VC22_a.sy +++ b/test/regress/regress1/sygus/VC22_a.sy @@ -1,5 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --cegis-sample=use (set-logic LIA) (synth-fun f ((x1 Int) (x2 Int)) Int diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy new file mode 100644 index 000000000..e994c2a5b --- /dev/null +++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy @@ -0,0 +1,74 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --cegis-sample=trust +(set-logic BV) + +; we test --cegis-sample=trust since we can exhaustively sample BV4 + +(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool + ((Start Bool ( + true + false + (not Start) + (and Start Start) + (or Start Start) +; (=> Start Start) + (= StartBv StartBv) + (bvult StartBv StartBv) + (bvslt StartBv StartBv) + (bvuge StartBv StartBv) + (bvsge StartBv StartBv) + )) + (StartBv (BitVec 4) ( + s + t + #x0 + #x8 ; min_val + #x7 ; max_val + (bvneg StartBv) + (bvnot StartBv) + (bvadd StartBv StartBv) + (bvsub StartBv StartBv) + (bvand StartBv StartBv) + (bvlshr StartBv StartBv) + (bvor StartBv StartBv) + (bvshl StartBv StartBv) + )) +)) + +(declare-var s (BitVec 4)) +(declare-var t (BitVec 4)) +(define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) + (ite (= b #x0) #xF (bvudiv a b)) +) +(define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4) + (ite (= b #x0) a (bvurem a b)) +) +(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool +(bvult (bvnot x) t) +) +(constraint + (= + (or + (case #x0 s t) + (case #x1 s t) + (case #x2 s t) + (case #x3 s t) + (case #x4 s t) + (case #x5 s t) + (case #x6 s t) + (case #x7 s t) + (case #x8 s t) + (case #x9 s t) + (case #xA s t) + (case #xB s t) + (case #xC s t) + (case #xD s t) + (case #xE s t) + (case #xF s t) + ) + (SC s t) + ) +) + +(check-synth) -- 2.30.2