From: Andrew Reynolds Date: Tue, 7 Jan 2020 17:39:27 +0000 (-0600) Subject: Update any-constant and normalization policies for sygus grammars (#3583) X-Git-Tag: cvc5-1.0.0~3746 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53dc40ec71344d6cc8df9f009cbbba4dbefccb64;p=cvc5.git Update any-constant and normalization policies for sygus grammars (#3583) --- 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::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(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 */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b42d586c8..a53201e3e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1762,6 +1762,7 @@ set(regress_1_tests regress1/sygus/issue3498.smt2 regress1/sygus/issue3514.smt2 regress1/sygus/issue3507.smt2 + regress1/sygus/issue3580.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/coeff-solve-inv.sy b/test/regress/regress1/sygus/coeff-solve-inv.sy index edfcd6089..ed4689fe9 100644 --- a/test/regress/regress1/sygus/coeff-solve-inv.sy +++ b/test/regress/regress1/sygus/coeff-solve-inv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 +; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 --sygus-grammar-cons=any-const (set-logic LIA) (synth-inv inv-f ((x Int) (y Int)) ) diff --git a/test/regress/regress1/sygus/issue3580.sy b/test/regress/regress1/sygus/issue3580.sy new file mode 100644 index 000000000..9da07407a --- /dev/null +++ b/test/regress/regress1/sygus/issue3580.sy @@ -0,0 +1,24 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2 +(set-logic ALL) +(synth-fun f + () Bool + ((B Bool)) + ( + (B Bool (true)) + ) +) +(synth-fun g + ((r Int)) Bool + ((B Bool) (I Int) (IConst Int)) + ( + (B Bool ((= I I) (=> B B))) + (I Int (r 0 (mod I IConst))) + (IConst Int ((Constant Int))) + ) +) +(constraint (g 0)) +(constraint (not (g 1))) +(constraint (g 2)) +(constraint f) +(check-synth) diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy index c19b2ff42..29e8527dc 100644 --- a/test/regress/regress2/sygus/ex23.sy +++ b/test/regress/regress2/sygus/ex23.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-repair-const +; COMMAND-LINE: --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const (set-logic LIA) (synth-inv inv-f ((y Int) (z Int) (c Int)))