From e9c115e82ea1341f1bbc37fb99c005aacec3d7ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Sep 2018 23:50:50 -0500 Subject: [PATCH] Allow partial models for multiple sygus enumerators (#2499) --- src/theory/datatypes/datatypes_rewriter.h | 11 ++++ src/theory/datatypes/datatypes_sygus.cpp | 4 ++ src/theory/quantifiers/sygus/cegis_unif.cpp | 7 +++ src/theory/quantifiers/sygus/sygus_module.h | 10 ++++ src/theory/quantifiers/sygus/sygus_pbe.cpp | 29 ++++++++--- src/theory/quantifiers/sygus/sygus_pbe.h | 5 ++ .../quantifiers/sygus/synth_conjecture.cpp | 50 ++++++++++++++----- .../quantifiers/sygus/synth_conjecture.h | 12 +++-- src/theory/quantifiers/sygus/synth_engine.cpp | 3 +- 9 files changed, 106 insertions(+), 25 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index a6c95b893..05f1a9960 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -39,6 +39,17 @@ struct SygusAnyConstAttributeId }; typedef expr::Attribute SygusAnyConstAttribute; +/** + * Attribute true for enumerators whose current model values have been excluded + * by sygus symmetry breaking. This is set by the datatypes sygus solver during + * LAST_CALL effort checks for each active sygus enumerator. + */ +struct SygusSymBreakExcAttributeId +{ +}; +typedef expr::Attribute + SygusSymBreakExcAttribute; + namespace datatypes { class DatatypesRewriter { diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index db1ce1c05..a6a3ffc9d 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1317,6 +1317,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { // register the search value ( prog -> progv ), this may invoke symmetry breaking if( options::sygusSymBreakDynamic() ){ Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas); + SygusSymBreakExcAttribute ssbea; + prog.setAttribute(ssbea, rsv.isNull()); if (rsv.isNull()) { Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; @@ -1474,6 +1476,8 @@ Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s) } Assert(!d_this.isNull()); NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s + << " for " << d_this << std::endl; return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 456f44019..d4926311d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -166,6 +166,13 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, ->toStreamSygus(ss, m_eu); Trace("cegis") << ss.str() << std::endl; } + if (m_eu.isNull()) + { + // A condition enumerator was excluded by symmetry breaking, fail. + // TODO (#2498): either move conditions to getTermList or handle + // partial models in this module. + return false; + } unif_values[index][e].push_back(m_eu); } // inter-enumerator symmetry breaking for return values diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index c1b12dfd0..02cf1cdf2 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -71,6 +71,16 @@ class SygusModule */ virtual void getTermList(const std::vector& candidates, std::vector& terms) = 0; + /** allow partial model + * + * This method returns true if this module does not require that all + * terms returned by getTermList have "proper" model values when calling + * constructCandidates. A term may have a model value that is not proper + * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model + * values that are not proper are replaced by "null" when calling + * constructCandidates. + */ + virtual bool allowPartialModel() { return false; } /** construct candidate * * This function takes as input: diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9a6645560..647b16637 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -415,6 +415,8 @@ void SygusPbe::getTermList(const std::vector& candidates, } } +bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } + bool SygusPbe::constructCandidates(const std::vector& enums, const std::vector& enum_values, const std::vector& candidates, @@ -431,10 +433,18 @@ bool SygusPbe::constructCandidates(const std::vector& enums, Trace("sygus-pbe-enum") << " " << enums[i] << " -> "; TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]); Trace("sygus-pbe-enum") << std::endl; - unsigned sz = d_tds->getSygusTermSize( enum_values[i] ); - szs.push_back(sz); - if( i==0 || szgetSygusTermSize(enum_values[i]); + szs.push_back(sz); + if (i == 0 || sz < min_term_size) + { + min_term_size = sz; + } + } + else + { + szs.push_back(0); } } // Assume two enumerators of types T1 and T2. @@ -448,11 +458,14 @@ bool SygusPbe::constructCandidates(const std::vector& enums, std::vector enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { - Assert(szs[i] >= min_term_size); - int diff = szs[i] - min_term_size; - if (!options::sygusPbeMultiFair() || diff <= diffAllow) + if (!enum_values[i].isNull()) { - enum_consider.push_back( i ); + Assert(szs[i] >= min_term_size); + int diff = szs[i] - min_term_size; + if (!options::sygusPbeMultiFair() || diff <= diffAllow) + { + enum_consider.push_back(i); + } } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 66e19b6c9..b2ad5f63a 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -117,6 +117,11 @@ class SygusPbe : public SygusModule */ void getTermList(const std::vector& candidates, std::vector& terms) override; + /** + * PBE allows partial models to handle multiple enumerators if we are not + * using a strictly fair enumeration strategy. + */ + bool allowPartialModel() override; /** construct candidates * * This function attempts to use unification-based approaches for constructing diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fde69d196..a29fdcc9f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -338,7 +339,14 @@ void SynthConjecture::doCheck(std::vector& lems) // get the model value of the relevant terms from the master module std::vector enum_values; - getModelValues(terms, enum_values); + bool fullModel = getModelValues(terms, enum_values); + + // if the master requires a full model and the model is partial, we fail + if (!d_master->allowPartialModel() && !fullModel) + { + Trace("cegqi-check") << "...partial model, fail." << std::endl; + return; + } if (!constructed_cand) { @@ -586,36 +594,54 @@ void SynthConjecture::preregisterConjecture(Node q) d_ceg_si->preregisterConjecture(q); } -void SynthConjecture::getModelValues(std::vector& n, std::vector& v) +bool SynthConjecture::getModelValues(std::vector& n, std::vector& v) { + bool ret = true; Trace("cegqi-engine") << " * Value is : "; for (unsigned i = 0; i < n.size(); i++) { Node nv = getModelValue(n[i]); v.push_back(nv); + ret = ret && !nv.isNull(); if (Trace.isOn("cegqi-engine")) { - TypeNode tn = nv.getType(); - Trace("cegqi-engine") << n[i] << " -> "; + Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv; + TypeNode tn = onv.getType(); std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + Trace("cegqi-engine") << n[i] << " -> "; + if (nv.isNull()) + { + Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; + } + else { - Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); - bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } } } - Assert(!nv.isNull()); } Trace("cegqi-engine") << std::endl; + return ret; } Node SynthConjecture::getModelValue(Node n) { Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue(n); + if (n.getAttribute(SygusSymBreakExcAttribute())) + { + // if the current model value of n was excluded by symmetry breaking, then + // it does not have a proper model value that we should consider, thus we + // return null. + return Node::null(); + } + Node mv = d_qe->getModel()->getValue(n); + return mv; } void SynthConjecture::debugPrint(const char* c) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1cbd4e949..53bc829cf 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -112,9 +112,15 @@ class SynthConjecture void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } - /** get model values for terms n, store in vector v */ - void getModelValues(std::vector& n, std::vector& v); - /** get model value for term n */ + /** + * Get model values for terms n, store in vector v. This method returns true + * if and only if all values added to v are non-null. + */ + bool getModelValues(std::vector& n, std::vector& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 56844ec1f..296c10ff6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -42,8 +42,7 @@ SynthEngine::~SynthEngine() { delete d_conj; } bool SynthEngine::needsCheck(Theory::Effort e) { - return !d_quantEngine->getTheoryEngine()->needCheck() - && e >= Theory::EFFORT_LAST_CALL; + return e >= Theory::EFFORT_LAST_CALL; } QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) -- 2.30.2