From: Andrew Reynolds Date: Thu, 24 Mar 2022 21:02:48 +0000 (-0500) Subject: Minor updates for quantifiers options (#8385) X-Git-Tag: cvc5-1.0.0~183 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d77704776d1fbd53e2398dd323f711e2ffcbd0b2;p=cvc5.git Minor updates for quantifiers options (#8385) --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8e29db08e..d78ea82ef 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -432,14 +432,6 @@ name = "Quantifiers" name = "last-call" help = "Run instantiation at last call effort, after theory combination and and theories report sat." -[[option]] - name = "instWhenStrictInterleave" - category = "regular" - long = "inst-when-strict-interleave" - type = "bool" - default = "true" - help = "ensure theory combination and standard quantifier effort strategies take turns" - [[option]] name = "instWhenPhase" category = "expert" @@ -1071,14 +1063,6 @@ name = "Quantifiers" default = "false" help = "statically normalize sygus grammars based on flattening (linearization)" -[[option]] - name = "sygusTemplEmbedGrammar" - category = "regular" - long = "sygus-templ-embed-grammar" - type = "bool" - default = "false" - help = "embed sygus templates into grammars" - [[option]] name = "sygusGrammarConsMode" category = "regular" @@ -1159,20 +1143,25 @@ name = "Quantifiers" help = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)" [[option]] - name = "sygusEvalUnfold" + name = "sygusEvalUnfoldMode" category = "regular" - long = "sygus-eval-unfold" - type = "bool" - default = "true" - help = "do unfolding of sygus evaluation functions" - -[[option]] - name = "sygusEvalUnfoldBool" - category = "expert" - long = "sygus-eval-unfold-bool" - type = "bool" - default = "true" - help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas" + long = "sygus-eval-unfold=MODE" + type = "SygusEvalUnfoldMode" + default = "SINGLE_BOOL" + help = "modes for sygus evaluation unfolding" + help_mode = "Modes for sygus evaluation unfolding." +[[option.mode.NONE]] + name = "none" + help = "Do not use sygus evaluation unfolding." +[[option.mode.SINGLE]] + name = "single" + help = "Do single-step unfolding for all evaluation functions." +[[option.mode.SINGLE_BOOL]] + name = "single-bool" + help = "Do single-step unfolding for Boolean functions and ITEs, and multi-step unfolding for all others." +[[option.mode.MULTI]] + name = "multi" + help = "Do multi-step unfolding for all evaluation functions." [[option]] name = "sygusStream" diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 62fe96439..df3173e00 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -44,10 +44,8 @@ void QuantifiersState::incrementInstRoundCounters(Theory::Effort e) { if (e == Theory::EFFORT_FULL) { - // increment if a last call happened, we are not strictly enforcing - // interleaving, or already were in phase + // increment if a last call happened, or already were in phase if (d_ierCounterLastLc != d_ierCounterLc - || !options().quantifiers.instWhenStrictInterleave || d_ierCounter % d_instWhenPhase != 0) { d_ierCounter = d_ierCounter + 1; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index f3d6268e0..36330f6f7 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -182,8 +182,10 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, } } // we only do evaluation unfolding for passive enumerators - bool doEvalUnfold = - (doGen && options().quantifiers.sygusEvalUnfold) || d_usingSymCons; + bool doEvalUnfold = (doGen + && options().quantifiers.sygusEvalUnfoldMode + != options::SygusEvalUnfoldMode::NONE) + || d_usingSymCons; if (doEvalUnfold) { Trace("sygus-engine") << " *** Do evaluation unfolding..." << std::endl; @@ -476,7 +478,9 @@ void Cegis::registerRefinementLemma(const std::vector& vars, Node lem) { addRefinementLemma(lem); // must be closed enumerable - if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + if (d_cexClosedEnum + && options().quantifiers.sygusEvalUnfoldMode + != options::SygusEvalUnfoldMode::NONE) { // Make the refinement lemma and add it to lems. // This lemma is guarded by the parent's guard, which has the semantics diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 2e52f67d3..d6e7dd573 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -37,7 +37,8 @@ SygusEvalUnfold::SygusEvalUnfold(Env& env, TermDbSygus* tds) void SygusEvalUnfold::registerEvalTerm(Node n) { - Assert(options().quantifiers.sygusEvalUnfold); + Assert(options().quantifiers.sygusEvalUnfoldMode + != options::SygusEvalUnfoldMode::NONE); // is this a sygus evaluation function application? if (n.getKind() != DT_SYGUS_EVAL) { @@ -146,7 +147,8 @@ void SygusEvalUnfold::registerModelValue(Node a, Node expn; // should we unfold? bool do_unfold = false; - if (options().quantifiers.sygusEvalUnfoldBool) + if (options().quantifiers.sygusEvalUnfoldMode + == options::SygusEvalUnfoldMode::SINGLE_BOOL) { Node bTermUse = bTerm; if (bTerm.getKind() == APPLY_UF) @@ -164,6 +166,12 @@ void SygusEvalUnfold::registerModelValue(Node a, do_unfold = true; } } + else if (options().quantifiers.sygusEvalUnfoldMode + == options::SygusEvalUnfoldMode::SINGLE) + { + // do single step for all + do_unfold = true; + } if (do_unfold || hasSymCons) { // note that this is replicated for different values diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index 32e58f6ce..869c8d1b7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -70,7 +70,8 @@ class SygusEvalUnfold : protected EnvObj * function, i.e. op is a builtin operator encoded by constructor C_op. * * We decide which kind of lemma to send ([A] or [B]) based on the symbol - * C_op. If op is an ITE, or if C_op is a Boolean operator, then we add [B]. + * C_op and the mode of sygus-eval-unfold. By default, if op is an ITE, or if + * C_op is a Boolean operator, then we add [B]. * Otherwise, we add [A]. The intuition of why [B] is better than [A] for the * former is that evaluation unfolding can lead to useful conflict analysis. * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 983ab6c60..dd1816d13 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -196,14 +196,6 @@ Node CegGrammarConstructor::process(Node q, Assert(itta != templates_arg.end()); TNode templ_arg = itta->second; Assert(!templ_arg.isNull()); - // if there is a template for this argument, make a sygus type on top of it - if (options().quantifiers.sygusTemplEmbedGrammar) - { - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ - << " with arg " << templ_arg << std::endl; - Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; - tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); - } } // ev is the first-order variable corresponding to this synth fun @@ -246,35 +238,39 @@ Node CegGrammarConstructor::process(Node q, Assert(!templ_arg.isNull()); // if there is a template for this argument, make a sygus type on top of // it - if (!options().quantifiers.sygusTemplEmbedGrammar) + // otherwise, apply it as a preprocessing pass + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ + << " with arg " << templ_arg << std::endl; + Trace("cegqi-debug") + << " apply this template as a substituion during preprocess..." + << std::endl; + std::vector schildren; + std::vector largs; + for (unsigned j = 0; j < sfvl.getNumChildren(); j++) { - // otherwise, apply it as a preprocessing pass - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ - << " with arg " << templ_arg << std::endl; - Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; - std::vector< Node > schildren; - std::vector< Node > largs; - for( unsigned j=0; jmkBoundVar(sfvl[j].getType())); - } - std::vector< Node > subsfn_children; - subsfn_children.push_back( sf ); - subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() ); - Node subsfn = nm->mkNode(kind::APPLY_UF, subsfn_children); - TNode subsf = subsfn; - Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl; - templ = templ.substitute( templ_arg, subsf ); - // substitute lambda arguments - templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() ); - Node subsn = - nm->mkNode(kind::LAMBDA, nm->mkNode(BOUND_VAR_LIST, largs), templ); - TNode var = sf; - TNode subs = subsn; - Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl; - qbody_subs = qbody_subs.substitute( var, subs ); - Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; + schildren.push_back(sfvl[j]); + largs.push_back(nm->mkBoundVar(sfvl[j].getType())); } + std::vector subsfn_children; + subsfn_children.push_back(sf); + subsfn_children.insert( + subsfn_children.end(), schildren.begin(), schildren.end()); + Node subsfn = nm->mkNode(kind::APPLY_UF, subsfn_children); + TNode subsf = subsfn; + Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " + << subsf << std::endl; + templ = templ.substitute(templ_arg, subsf); + // substitute lambda arguments + templ = templ.substitute( + schildren.begin(), schildren.end(), largs.begin(), largs.end()); + Node subsn = + nm->mkNode(kind::LAMBDA, nm->mkNode(BOUND_VAR_LIST, largs), templ); + TNode var = sf; + TNode subs = subsn; + Trace("cegqi-debug") << " substitute : " << var << " -> " << subs + << std::endl; + qbody_subs = qbody_subs.substitute(var, subs); + Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; } d_tds->registerSygusType(tn); Assert(tn.isDatatype()); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index df725ac55..1979aba0b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1029,30 +1029,21 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, { Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl; - // if it was not embedded into the grammar - if (!options().quantifiers.sygusTemplEmbedGrammar) - { - TNode templa = d_templInfer->getTemplateArg(sf); - // make the builtin version of the full solution - sol = d_tds->sygusToBuiltin(sol, sol.getType()); - Trace("cegqi-inv") << "Builtin version of solution is : " << sol - << ", type : " << sol.getType() << std::endl; - TNode tsol = sol; - sol = templ.substitute(templa, tsol); - Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; - sol = rewrite(sol); - Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; - // now, reconstruct to the syntax - sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); - sol = sol.getKind() == LAMBDA ? sol[1] : sol; - Trace("cegqi-inv-debug") - << "Reconstructed to syntax : " << sol << std::endl; - } - else - { - Trace("cegqi-inv-debug") - << "...was embedding into grammar." << std::endl; - } + TNode templa = d_templInfer->getTemplateArg(sf); + // make the builtin version of the full solution + sol = d_tds->sygusToBuiltin(sol, sol.getType()); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol + << ", type : " << sol.getType() << std::endl; + TNode tsol = sol; + sol = templ.substitute(templa, tsol); + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = rewrite(sol); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + // now, reconstruct to the syntax + sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); + sol = sol.getKind() == LAMBDA ? sol[1] : sol; + Trace("cegqi-inv-debug") + << "Reconstructed to syntax : " << sol << std::endl; } else { diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 5cefb4275..36fdc3970 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -98,7 +98,9 @@ void TermRegistry::addTerm(Node n, bool withinQuant) || options().quantifiers.termDbCd) { d_termDb->addTerm(n); - if (d_sygusTdb.get() && options().quantifiers.sygusEvalUnfold) + if (d_sygusTdb.get() + && options().quantifiers.sygusEvalUnfoldMode + != options::SygusEvalUnfoldMode::NONE) { d_sygusTdb->getEvalUnfold()->registerEvalTerm(n); }