From 011cd46ecf51502344b568c2613f420691724c83 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 1 Feb 2015 20:54:28 +0100 Subject: [PATCH] Generalization of sygus lemmas based on arguments and content. --- src/theory/datatypes/datatypes_sygus.cpp | 338 ++++++++++++++++++---- src/theory/datatypes/datatypes_sygus.h | 28 +- src/theory/datatypes/theory_datatypes.cpp | 8 +- src/theory/quantifiers/options | 10 +- 4 files changed, 315 insertions(+), 69 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index e186c94d1..1fd0e4c52 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -688,7 +688,7 @@ bool SygusSymBreak::ProgSearch::processProgramDepth( int depth ){ //now have entire information about candidate program at given depth Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, Node::null(), var_count, testers, testers_u ); if( !prog.isNull() ){ - if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers, testers_u ) ){ + if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers, testers_u, var_count ) ){ return false; } }else{ @@ -712,7 +712,7 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept //now have entire information about candidate program at given depth Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, Node::null(), var_count, testers, testers_u ); if( !prog.isNull() ){ - if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers, testers_u ) ){ + if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers, testers_u, var_count ) ){ return false; } //also try higher levels @@ -756,7 +756,8 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog } bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, - std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { + std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u, + std::map< TypeNode, int >& var_count ) { Assert( a.getType()==at ); //Assert( !d_util->d_conflict ); std::map< Node, bool >::iterator it = d_redundant[at].find( prog ); @@ -764,8 +765,9 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node if( it==d_redundant[at].end() ){ Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl; Node progr = d_util->getNormalized( at, prog ); - std::map< Node, Node >::iterator it = d_normalized_to_orig[at].find( progr ); - if( it==d_normalized_to_orig[at].end() ){ + Node rep_prog; + std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr ); + if( itnp==d_normalized_to_orig[at].end() ){ d_normalized_to_orig[at][progr] = prog; if( progr.getKind()==SKOLEM && d_util->getSygusType( progr )==at ){ Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl; @@ -776,15 +778,26 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node red = false; } }else{ + Assert( prog!=itnp->second ); d_redundant[at][prog] = true; red = true; - Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl; + rep_prog = itnp->second; + Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << rep_prog << " both rewrite to " << progr << std::endl; } if( red ){ Assert( !testers.empty() ); - Assert( prog!=it->second ); bool conflict_gen_set = false; if( options::sygusNormalFormGlobalGen() ){ + bool narrow = false; + Trace("sygus-nf-gen-debug") << "Tester tree is : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = testers_u.begin(); it != testers_u.end(); ++it ){ + Trace("sygus-nf-gen-debug") << " " << it->first << " -> " << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + Trace("sygus-nf-gen-debug") << " " << it->second[i] << std::endl; + } + } + Trace("sygus-nf-gen-debug") << std::endl; + //generalize conflict if( prog.getNumChildren()>0 ){ Assert( !testers.empty() ); @@ -793,72 +806,182 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node //for( unsigned i=0; i >::iterator it = testers_u.begin(); it != testers_u.end(); ++it ){ - Trace("sygus-nf-gen-debug2") << " " << it->first << " -> " << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - Trace("sygus-nf-gen-debug2") << " " << it->second[i] << std::endl; - } - } - Trace("sygus-nf-gen-debug2") << std::endl; Assert( testers[0][0]==a ); Assert( prog.getNumChildren()==testers_u[a].size() ); //get the normal form for each child Kind parentKind = prog.getKind(); Kind parentOpKind = prog.getOperator().getKind(); Trace("sygus-nf-gen-debug") << "Parent kind is " << parentKind << " " << parentOpKind << std::endl; - std::map< int, Node > norm_children; - std::map< int, bool > rlv; + //std::map< int, Node > norm_children; + + //arguments that are relevant + std::map< unsigned, bool > rlv; + //testers that are irrelevant + std::map< Node, bool > irrlv_tst; + + std::vector< Node > children; + std::vector< TypeNode > children_stype; + std::vector< Node > nchildren; for( unsigned i=0; igetNormalized( tn, prog[i], true ); + children.push_back( prog[i] ); + children_stype.push_back( tn ); + Node nc = d_util->getNormalized( tn, prog[i], true ); + //norm_children[i] = nc; rlv[i] = true; - Trace("sygus-nf-gen") << "- child " << i << " normalizes to " << norm_children[i] << std::endl; + nchildren.push_back( nc ); + Trace("sygus-nf-gen") << "- child " << i << " normalizes to " << nc << std::endl; } - //now, determine a minimal subset of the arguments that the rewriting depended on if( testers_u[a].size()>1 ){ const Datatype & pdt = ((DatatypeType)(at).toType()).getDatatype(); int pc = Datatype::indexOf( testers[0].getOperator().toExpr() ); + // [1] determine a minimal subset of the arguments that the rewriting depended on //quick checks based on constants - for( std::map< int, Node >::iterator it = norm_children.begin(); it != norm_children.end(); ++it ){ - if( it->second.isConst() ){ + bool singleArg = false; + for( unsigned i=0; ifirst << " under builtin operator." << std::endl; - if( !processConstantArg( at, pdt, pc, parentKind, it->first, it->second, rlv ) ){ - for( std::map< int, bool >::iterator itr = rlv.begin(); itr != rlv.end(); ++itr ){ - if( itr->first!=it->first ){ + Trace("sygus-nf-gen") << "-- constant arg " <::iterator itr = rlv.begin(); itr != rlv.end(); ++itr ){ + if( itr->first!=i ){ rlv[itr->first] = false; } } + narrow = true; + singleArg = true; break; } } } } - //relevant testers : root + recursive collection of relevant children - Trace("sygus-nf-gen-debug") << "Collect relevant testers..." << std::endl; - std::vector< Node > rlv_testers; - rlv_testers.push_back( testers[0] ); - for( unsigned i=0; igetVarInc( children_stype[i], var_count ); + Node progcn = NodeManager::currentNM()->mkNode( prog.getKind(), children ); + Node progcr = Rewriter::rewrite( progcn ); + Trace("sygus-nf-gen-debug") << "Var replace argument " << i << " : " << progcn << " -> " << progcr << std::endl; + if( progcr==progr ){ + //this argument is not relevant, continue with it remaining as variable + rlv[i] = false; + argChanged = true; + narrow = true; + Trace("sygus-nf") << " - argument " << i << " is not relevant." << std::endl; + }else{ + //go back to original + children[i] = prev; + var_count[children_stype[i]]--; + } + } + if( argChanged ){ + progc = NodeManager::currentNM()->mkNode( prog.getKind(), children ); + } + } + Trace("sygus-nf-gen-debug") << "Relevant template (post argument analysis) is : " << progc << std::endl; + + // [3] generalize content + if( options::sygusNormalFormGlobalContent() ){ + std::map< Node, std::vector< Node > > nodes; + std::vector< Node > curr_vars; + std::vector< Node > curr_subs; + collectSubterms( progc, testers[0], testers_u, nodes ); + for( std::map< Node, std::vector< Node > >::iterator it = nodes.begin(); it != nodes.end(); ++it ){ + if( it->second.size()>1 ){ + Trace("sygus-nf-gen-debug") << it->first << " occurs " << it->second.size() << " times, at : " << std::endl; + for( unsigned j=0; jsecond.size(); j++ ){ + Trace("sygus-nf-gen-debug") << " " << it->second[j] << " "; + } + Trace("sygus-nf-gen-debug") << std::endl; + Node prev = progc; + //try a substitution on all terms of this form simultaneously to see if the content of this subterm is irrelevant + TypeNode tn = it->second[0][0].getType(); + TNode st = it->first; + //we may already have substituted within this subterm + if( !curr_subs.empty() ){ + st = st.substitute( curr_vars.begin(), curr_vars.end(), curr_subs.begin(), curr_subs.end() ); + Trace("sygus-nf-gen-debug") << "...substituted : " << st << std::endl; + } + TNode nv = d_util->getVarInc( tn, var_count ); + progc = progc.substitute( st, nv ); + Node progcr = Rewriter::rewrite( progc ); + Trace("sygus-nf-gen-debug") << "Var replace content " << st << " : " << progc << " -> " << progcr << std::endl; + if( progcr==progr ){ + narrow = true; + Trace("sygus-nf") << " - content " << st << " is not relevant." << std::endl; + int t_prev = -1; + for( unsigned i=0; isecond.size(); i++ ){ + irrlv_tst[it->second[i]] = true; + Trace("sygus-nf-gen-debug") << "By content, " << it->second[i] << " is irrelevant." << std::endl; + int t_curr = std::find( testers.begin(), testers.end(), it->second[i] )-testers.begin(); + Assert( testers[t_curr]==it->second[i] ); + if( t_prev!=-1 ){ + d_lemma_inc_eq[at][prog].push_back( std::pair< int, int >( t_prev, t_curr ) ); + Trace("sygus-nf-gen-debug") << "Which requires " << testers[t_prev][0] << " = " << testers[t_curr][0] << std::endl; + } + t_prev = t_curr; + } + curr_vars.push_back( st ); + curr_subs.push_back( nv ); + }else{ + var_count[tn]--; + progc = prev; + } + } + } } + Trace("sygus-nf-gen-debug") << "Relevant template (post content analysis) is : " << progc << std::endl; } - Trace("sygus-nf-gen-debug") << "Relevant testers : " << std::endl; - conflict_gen_set = true; - for( unsigned i=0; i " << rl << std::endl; - d_lemma_gen[at][prog].push_back( rl ); + if( narrow ){ + //relevant testers : root + recursive collection of relevant children + Trace("sygus-nf-gen-debug") << "Collect relevant testers..." << std::endl; + std::vector< Node > rlv_testers; + rlv_testers.push_back( testers[0] ); + for( unsigned i=0; i::iterator itav = d_anchor_var.find( at ); + if( itav==d_anchor_var.end() ){ + anc_var = NodeManager::currentNM()->mkSkolem( "a", at, "Sygus nf global gen anchor var" ); + d_anchor_var[at] = anc_var; + }else{ + anc_var = itav->second; + } + int status = 0; + Node anc_temp = getSeparationTemplate( at, rep_prog, anc_var, status ); + Trace("sygus-nf") << " -- separation template is " << anc_temp << ", status = " << status << std::endl; + d_lemma_inc_eq_gr[status][at][prog].push_back( anc_temp ); + }else{ + Trace("sygus-nf") << " -- no separation necessary" << std::endl; + } + Trace("sygus-nf-gen-debug") << "Relevant testers : " << std::endl; + for( unsigned i=0; i " << rl << std::endl; + d_lemma_inc_tst[at][prog].push_back( rl ); + } + + conflict_gen_set = true; } } } } if( !conflict_gen_set ){ for( unsigned i=0; i gtesters; + Assert( d_lemma_inc_tst[at][prog].size()==testers.size() ); + std::vector< Node > disj; + //get the guard equalities + for( unsigned r=0; r<2; r++ ){ + for( unsigned i=0; imkNode( OR, gtesters ); + Node lem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); d_util->d_lemmas.push_back( lem ); - Trace("sygus-sym-break2") << "Sym break lemma : " << lem << std::endl; + Trace("sygus-sym-break-lemma") << "Sym break lemma : " << lem << std::endl; }else{ Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl; } @@ -887,8 +1030,65 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node } } +bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) { + Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << std::endl; + TypeNode tn = tst_curr[0].getType(); + Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator(); + //we can continue if the tester in question is relevant + if( std::find( rlv_testers.begin(), rlv_testers.end(), tst_curr )!=rlv_testers.end() ){ + unsigned tindex = Datatype::indexOf( tst_curr.getOperator().toExpr() ); + Node op = d_util->getArgOp( tn, tindex ); + if( op!=rop ){ + Trace("sygus-nf-gen-debug") << "mismatch, success." << std::endl; + return true; + }else if( !testers_u[tst_curr[0]].empty() ){ + Assert( testers_u[tst_curr[0]].size()==rep_prog.getNumChildren() ); + for( unsigned i=0; iisVar( rep_prog ) ){ + status = 1; + return anc_var; + }else{ + Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator(); + int rop_arg = d_util->getOpArg( tn, rop ); + Assert( rop_arg>=0 && rop_arg<(int)dt.getNumConstructors() ); + Assert( rep_prog.getNumChildren()==dt[rop_arg].getNumArgs() ); + + std::vector< Node > children; + children.push_back( Node::fromExpr( dt[rop_arg].getConstructor() ) ); + for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[rop_arg][i].getSelector() ), anc_var ); + arg = arg.substitute( tanc_var, tanc_var_subs ); + status = 1; + } + children.push_back( arg ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + } +} + bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, - Kind k, int i, Node arg, std::map< int, bool >& rlv ) { + Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ) { Assert( d_util->hasKind( tnp, k ) ); if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){ return false; @@ -909,12 +1109,23 @@ bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int return true; } -void SygusSymBreak::collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers ) { - testers.push_back( tst ); - std::map< Node, std::vector< Node > >::iterator it = testers_u.find( tst[0] ); - if( it!=testers_u.end() ){ - for( unsigned i=0; isecond.size(); i++ ){ - collectTesters( it->second[i], testers_u, testers ); +void SygusSymBreak::collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers, std::map< Node, bool >& irrlv_tst ) { + if( irrlv_tst.find( tst )==irrlv_tst.end() ){ + testers.push_back( tst ); + std::map< Node, std::vector< Node > >::iterator it = testers_u.find( tst[0] ); + if( it!=testers_u.end() ){ + for( unsigned i=0; isecond.size(); i++ ){ + collectTesters( it->second[i], testers_u, testers, irrlv_tst ); + } + } + } +} + +void SygusSymBreak::collectSubterms( Node n, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::map< Node, std::vector< Node > >& nodes ) { + if( !d_util->isVar( n ) ){ + nodes[n].push_back( tst_curr ); + for( unsigned i=0; i=(int)d_fv[tn].size() ){ std::stringstream ss; TypeNode vtn = tn; @@ -945,7 +1156,7 @@ Node SygusUtil::getVar( TypeNode tn, int i ) { return d_fv[tn][i]; } -Node SygusUtil::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) { +TNode SygusUtil::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) { std::map< TypeNode, int >::iterator it = var_count.find( tn ); if( it==var_count.end() ){ var_count[tn] = 1; @@ -1242,6 +1453,7 @@ void SygusUtil::registerSygusType( TypeNode tn ){ d_arg_const[tn][i] = n; } d_ops[tn][n] = i; + d_arg_ops[tn][i] = n; Trace("sygus-util") << std::endl; } } @@ -1296,6 +1508,18 @@ bool SygusUtil::hasOp( TypeNode tn, Node n ) { return getOpArg( tn, n )!=-1; } +Node SygusUtil::getArgOp( TypeNode tn, int i ) { + Assert( isRegistered( tn ) ); + std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn ); + if( itt!=d_arg_ops.end() ){ + std::map< int, Node >::iterator itn = itt->second.find( i ); + if( itn!=itt->second.end() ){ + return itn->second; + } + } + return Node::null(); +} + Kind SygusUtil::getArgKind( TypeNode tn, int i ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn ); diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index db44eaa55..954a43875 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -107,12 +107,23 @@ private: std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig; std::map< TypeNode, std::map< Node, bool > > d_redundant; std::map< TypeNode, std::map< Node, std::vector< Node > > > d_lemmas_reported; - std::map< TypeNode, std::map< Node, std::vector< bool > > > d_lemma_gen; + //which testers to include in the lemma + std::map< TypeNode, std::map< Node, std::vector< bool > > > d_lemma_inc_tst; + //additional equalities to include in the lemma + std::map< TypeNode, std::map< Node, std::vector< std::pair< int, int > > > > d_lemma_inc_eq; + //other equalities + std::map< TypeNode, Node > d_anchor_var; + std::map< TypeNode, std::map< Node, std::vector< Node > > > d_lemma_inc_eq_gr[2]; +private: Node getAnchor( Node n ); bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog, - std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ); - bool processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, Kind k, int i, Node arg, std::map< int, bool >& rlv ); - void collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers ); + std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u, + std::map< TypeNode, int >& var_count ); + bool processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ); + void collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers, std::map< Node, bool >& irrlv_tst ); + void collectSubterms( Node n, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::map< Node, std::vector< Node > >& nodes ); + bool isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ); + Node getSeparationTemplate( TypeNode tn, Node rep_prog, Node anc_var, int& status ); public: SygusSymBreak( SygusUtil * util, context::Context* c ); /** add tester */ @@ -126,6 +137,11 @@ class SygusUtil private: std::map< TypeNode, std::vector< Node > > d_fv; std::map< Node, TypeNode > d_fv_stype; +private: + TNode getVar( TypeNode tn, int i ); + TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); + bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); } +private: SygusSplit * d_split; SygusSymBreak * d_sym_break; std::map< TypeNode, std::map< Node, Node > > d_normalized; @@ -137,6 +153,7 @@ private: std::map< TypeNode, std::map< int, Node > > d_arg_const; std::map< TypeNode, std::map< Node, int > > d_consts; std::map< TypeNode, std::map< Node, int > > d_ops; + std::map< TypeNode, std::map< int, Node > > d_arg_ops; private: bool isRegistered( TypeNode tn ); int getKindArg( TypeNode tn, Kind k ); @@ -145,6 +162,7 @@ private: bool hasKind( TypeNode tn, Kind k ); bool hasConst( TypeNode tn, Node n ); bool hasOp( TypeNode tn, Node n ); + Node getArgOp( TypeNode tn, int i ); Kind getArgKind( TypeNode tn, int i ); bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); @@ -174,8 +192,6 @@ private: /** get value */ Node getTypeMaxValue( TypeNode tn ); private: - Node getVar( TypeNode tn, int i ); - Node getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); TypeNode getSygusType( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 063b76102..c73ec8039 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -610,13 +610,12 @@ bool TheoryDatatypes::propagate(TNode literal){ } void TheoryDatatypes::addAssumptions( std::vector& assumptions, std::vector& tassumptions ) { + std::vector ntassumptions; for( unsigned i=0; i& assumptions, std::vect } } } + if( !ntassumptions.empty() ){ + addAssumptions( assumptions, ntassumptions ); + } } void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ) { diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 4a093b617..92285bf12 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -202,10 +202,14 @@ option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true account for relationship between arguments of operations in sygus normal form -option sygusNormalFormGlobal --sygus-nf-global bool :default true +option sygusNormalFormGlobal --sygus-nf-sym bool :default true narrow sygus search space based on global state of current candidate program -option sygusNormalFormGlobalGen --sygus-nf-global-gen bool :default true - generalize conflict lemmas for global search space narrowing +option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true + generalize lemmas for global search space narrowing +option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true + generalize based on arguments in global search space narrowing +option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true + generalize based on content in global search space narrowing option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions -- 2.30.2