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"
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"
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"
{
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;
}
}
// 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;
{
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
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)
{
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)
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
* 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.
*
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
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<Node> schildren;
+ std::vector<Node> 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; j<sfvl.getNumChildren(); j++ ){
- schildren.push_back( sfvl[j] );
- largs.push_back(nm->mkBoundVar(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<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;
}
d_tds->registerSygusType(tn);
Assert(tn.isDatatype());
{
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
{
|| 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);
}
projects / cvc5.git / commitdiff