diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-07 11:39:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-07 11:39:27 -0600 |
commit | 53dc40ec71344d6cc8df9f009cbbba4dbefccb64 (patch) | |
tree | c005676b3c59786652b3f816fe02b42f892316b9 /src/theory/quantifiers | |
parent | e3e6f0dc62f0bb9d3fb8d752c5eb4600872fd806 (diff) |
Update any-constant and normalization policies for sygus grammars (#3583)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 6 |
6 files changed, 9 insertions, 27 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 78ea5b22f..2d27878fd 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -79,7 +79,6 @@ bool Cegis::processInitialize(Node conj, Trace("cegis") << "...register enumerator " << candidates[i]; // We use symbolic constants if we are doing repair constants or if the // grammar construction was not simple. - bool useSymCons = false; if (options::sygusRepairConst() || options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE) @@ -89,15 +88,13 @@ bool Cegis::processInitialize(Node conj, SygusTypeInfo& cti = d_tds->getTypeInfo(ctn); if (cti.hasSubtermSymbolicCons()) { - useSymCons = true; // remember that we are using symbolic constructors d_usingSymCons = true; Trace("cegis") << " (using symbolic constructors)"; } } Trace("cegis") << std::endl; - d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, erole, useSymCons); + d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, erole); } return true; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 8812032ba..a76159b90 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -639,9 +639,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; - bool useSymCons = - options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE; - d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, useSymCons); + d_tds->registerEnumerator(e, si.d_pt, d_parent, erole); } void CegisUnifEnumDecisionStrategy::registerEvalPts( diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 78fbc48f3..389cf34de 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -141,6 +141,9 @@ Node CegGrammarConstructor::process(Node q, { sfvl = preGrammarType.getDType().getSygusVarList(); tn = preGrammarType; + // normalize type, if user-provided + SygusGrammarNorm sygus_norm(d_qe); + tn = sygus_norm.normalizeSygusType(tn, sfvl); }else{ sfvl = getSygusVarList(sf); // check which arguments are irrelevant @@ -167,10 +170,6 @@ Node CegGrammarConstructor::process(Node q, Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl; - // normalize type - SygusGrammarNorm sygus_norm(d_qe); - tn = sygus_norm.normalizeSygusType(tn, sfvl); - std::map<Node, Node>::const_iterator itt = templates.find(sf); if( itt!=templates.end() ){ Node templ = itt->second; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 474fdb5d8..5c0985f7e 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -235,7 +235,7 @@ bool SygusPbe::initialize(Node conj, for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); - d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false); + d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 1fda55172..b096b2430 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -373,8 +373,7 @@ bool TermDbSygus::registerSygusType(TypeNode tn) void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, - EnumeratorRole erole, - bool useSymbolicCons) + EnumeratorRole erole) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -391,7 +390,6 @@ void TermDbSygus::registerEnumerator(Node e, Trace("sygus-db") << " registering symmetry breaking clauses..." << std::endl; - d_enum_to_using_sym_cons[e] = useSymbolicCons; // depending on if we are using symbolic constructors, introduce symmetry // breaking lemma templates for each relevant subtype of the grammar SygusTypeInfo& eti = getTypeInfo(et); @@ -409,13 +407,7 @@ void TermDbSygus::registerEnumerator(Node e, for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { bool isAnyC = static_cast<int>(i) == anyC; - if (isAnyC && !useSymbolicCons) - { - // if we are not using the any constant constructor - // do not use the symbolic constructor - rm_indices.push_back(i); - } - else if (anyC != -1 && !isAnyC && useSymbolicCons) + if (anyC != -1 && !isAnyC) { // if we are using the any constant constructor, do not use any // concrete constant diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 6d328ddca..b9f8bf987 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -103,17 +103,13 @@ class TermDbSygus { * and not x2-x1 will be generated, assuming x1 and x2 are in the same * "subclass", see getSubclassForVar). * - * useSymbolicCons : whether we want model values for e to include symbolic - * constructors like the "any constant" variable. - * * An "active guard" may be allocated by this method for e based on erole * and the policies for active generation. */ void registerEnumerator(Node e, Node f, SynthConjecture* conj, - EnumeratorRole erole, - bool useSymbolicCons = false); + EnumeratorRole erole); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ |