theory/quantifiers/conjecture_generator.cpp \
theory/quantifiers/ce_guided_instantiation.h \
theory/quantifiers/ce_guided_instantiation.cpp \
+ theory/quantifiers/ce_guided_single_inv.h \
+ theory/quantifiers/ce_guided_single_inv.cpp \
theory/quantifiers/local_theory_ext.h \
theory/quantifiers/local_theory_ext.cpp \
theory/quantifiers/fun_def_process.h \
}
//apply counterexample guided instantiation options
+ if( options::cegqiSingleInv() ){
+ options::ceGuidedInst.set( true );
+ }
if( options::ceGuidedInst() ){
if( !options::quantConflictFind.wasSetByUser() ){
options::quantConflictFind.set( false );
Assert( pdt.isSygus() );
csIndex = Datatype::cindexOf(selectorExpr);
sIndex = Datatype::indexOf(selectorExpr);
- TypeNode tnnp = n[0].getType();
+ tnnp = n[0].getType();
//register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
//check if we can strengthen the first argument
if( !arg1.isNull() ){
const Datatype& dt1 = ((DatatypeType)(tn1).toType()).getDatatype();
+ Kind k = d_util->getArgKind( tnnp, csIndex );
+ //size comparison for arguments (if necessary)
+ Node sz_leq;
+ if( tn1==tnn && d_util->isComm( k ) ){
+ sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) );
+ }
std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i );
if( it!=d_sygus_pc_arg_pos[tnn][csIndex].end() ){
Assert( !it->second.empty() );
std::vector< Node > lem_c;
for( unsigned j=0; j<it->second.size(); j++ ){
- lem_c.push_back( DatatypesRewriter::mkTester( arg1, it->second[j], dt1 ) );
+ Node tt = DatatypesRewriter::mkTester( arg1, it->second[j], dt1 );
+ //if commutative operator, and children have same constructor type, then first arg is larger than second arg
+ if( it->second[j]==(int)i && !sz_leq.isNull() ){
+ tt = NodeManager::currentNM()->mkNode( AND, tt, sz_leq );
+ }
+ lem_c.push_back( tt );
}
Node argStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c );
Trace("sygus-str") << "...strengthen corresponding first argument of " << test << " : " << argStr << std::endl;
test_c.push_back( argStr );
narrow = true;
+ }else{
+ if( !sz_leq.isNull() ){
+ test_c.push_back( NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( arg1, i, dt1 ).negate(), sz_leq ) );
+ narrow = true;
+ }
}
}
//other constraints on arguments
Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
addSplit = !isGenericRedundant( tnnp, g );
}
+ /*
+ else{
+ Trace("sygus-nf-temp") << "Check " << dt[i].getName() << " as argument " << sIndex << " under " << parentKind << std::endl;
+ std::map< int, Node > prec;
+ std::map< TypeNode, int > var_count;
+ Node gc = d_util->mkGeneric( dt, i, var_count, prec );
+ std::map< int, Node > pre;
+ pre[sIndex] = gc;
+ Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
+ bool tmp = !isGenericRedundant( tnnp, g, false );
+ }
+ */
}
}
d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
}
Kind nk = UNDEFINED_KIND;
Kind reqk = UNDEFINED_KIND; //required kind for all children
- std::map< int, Kind > reqk_arg; //TODO
if( parent==NOT ){
if( k==AND ) {
nk = OR;reqk = NOT;
int pcr = d_util->getKindArg( tnp, nk );
if( pcr!=-1 ){
Assert( pcr<(int)pdt.getNumConstructors() );
- //must have same number of arguments
- if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
- bool success = true;
- std::map< int, TypeNode > childTypes;
- for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
- TypeNode tna = getArgType( pdt[pcr], i );
- Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
- if( reqk!=UNDEFINED_KIND ){
- //child must have a NOT
- int nindex = d_util->getKindArg( tna, reqk );
- if( nindex!=-1 ){
- const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
- childTypes[i] = getArgType( adt[nindex], 0 );
- }else{
- Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
- success = false;
- break;
- }
- }else{
- childTypes[i] = tna;
- }
- }
- if( success ){
- //children types of reduced operator must match types of original
+ if( reqk!=UNDEFINED_KIND ){
+ //must have same number of arguments
+ if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
+ bool success = true;
+ std::map< int, TypeNode > childTypes;
for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
- if( getArgType( dt[c], i )!=childTypes[i] ){
- Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
- success = false;
- break;
+ TypeNode tna = getArgType( pdt[pcr], i );
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
+ if( reqk!=UNDEFINED_KIND ){
+ //child must have a NOT
+ int nindex = d_util->getKindArg( tna, reqk );
+ if( nindex!=-1 ){
+ const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
+ if( getArgType( dt[c], i )!=getArgType( adt[nindex], 0 ) ){
+ Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
+ success = false;
+ break;
+ }
+ }else{
+ Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
+ success = false;
+ break;
+ }
+ }else{
+ childTypes[i] = tna;
}
}
- if( !success ){
- //check based on commutativity TODO
- }
if( success ){
Trace("sygus-split-debug") << "...success" << std::endl;
return false;
}
+ }else{
+ Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
}
}else{
- Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
+ return !isTypeMatch( pdt[pcr], dt[c] );
}
}else{
Trace("sygus-split-debug") << "...operator not available." << std::endl;
}
}
+ }
+ if( parent==MINUS || parent==BITVECTOR_SUB ){
+
+
}
return true;
}
}
}
-bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
+bool SygusSplit::isGenericRedundant( TypeNode tn, Node g, bool active ) {
//everything added to this cache should be mutually exclusive cases
std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
if( it==d_gen_redundant[tn].end() ){
Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
Node gr = d_util->getNormalized( tn, g, false );
Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
- std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
- bool red = true;
- if( itg==d_gen_terms[tn].end() ){
- red = false;
- d_gen_terms[tn][gr] = g;
- Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
+ if( active ){
+ std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
+ bool red = true;
+ if( itg==d_gen_terms[tn].end() ){
+ red = false;
+ d_gen_terms[tn][gr] = g;
+ d_gen_terms_inactive[tn][gr] = g;
+ Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
+ }else{
+ Trace("sygus-gnf-debug") << "...redundant." << std::endl;
+ Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+ }
+ d_gen_redundant[tn][g] = red;
+ return red;
}else{
- Trace("sygus-gnf-debug") << "...redundant." << std::endl;
- Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+ std::map< Node, Node >::iterator itg = d_gen_terms_inactive[tn].find( gr );
+ if( itg==d_gen_terms_inactive[tn].end() ){
+ Trace("sygus-nf-temp") << "..." << g << " rewrites to " << gr << std::endl;
+ d_gen_terms_inactive[tn][gr] = g;
+ }else{
+ Trace("sygus-nf-temp") << "* Note " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+ }
+ return false;
}
- d_gen_redundant[tn][g] = red;
- return red;
}else{
return it->second;
}
}else{
Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl;
}
- return false;
- }else{
- return true;
+ //for now, continue adding lemmas (since we are not forcing conflicts)
+ //return false;
}
+ return true;
}
bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) {
std::map< TypeNode, TypeNode > d_register; //stores sygus type
// type to (rewritten) to original
std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
+ std::map< TypeNode, std::map< Node, Node > > d_gen_terms_inactive;
std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
private:
/** register sygus type */
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
private:
// generic cache
- bool isGenericRedundant( TypeNode tn, Node g );
+ bool isGenericRedundant( TypeNode tn, Node g, bool active = true );
public:
SygusSplit( SygusUtil * util ) : d_util( util ) {}
/** get sygus splits */
}else{
//check if we have reached the maximum number of testers
// in this case, add the positive tester
- if( lbl->size()==dt.getNumConstructors()-1 ){
+ //this should not be done for sygus, since cases may be limited
+ if( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){
std::vector< bool > pcons;
getPossibleCons( eqc, n, pcons );
int testerIndex = -1;
std::map< Node, Node > msum;
if (QuantArith::getMonomialSumLit( lit, msum )){
Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
- for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
- Trace("bound-int-debug") << " ";
- if( !it->second.isNull() ){
- Trace("bound-int-debug") << it->second;
- if( !it->first.isNull() ){
- Trace("bound-int-debug") << " * ";
- }
- }
- if( !it->first.isNull() ){
- Trace("bound-int-debug") << it->first;
- }
- Trace("bound-int-debug") << std::endl;
- }
- Trace("bound-int-debug") << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){
Node veq;
namespace CVC4 {
-void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
- if( n.getKind()==OR ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- collectDisjuncts( n[i], d );
- }
- }else{
- d.push_back( n );
- }
-}
-
-CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
d_refine_count = 0;
+ d_ceg_si = NULL;
}
-void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
+void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
Assert( d_quant.isNull() );
Assert( q.getKind()==FORALL );
d_quant = q;
}
}
d_syntax_guided = true;
- if( options::sygusSingleInv() ){
- analyzeSygusConjecture();
+ if( options::cegqiSingleInv() ){
+ d_ceg_si = new CegConjectureSingleInv( q, this );
+ d_ceg_si->initialize();
}
}else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
d_syntax_guided = false;
}
}
-
-
-void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
- Node q = d_quant;
- // conj -> conj*
- std::map< Node, std::vector< Node > > children;
- // conj X prog -> inv*
- std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke;
- std::vector< Node > progs;
- std::map< Node, std::map< Node, bool > > contains;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- progs.push_back( q[0][i] );
- }
- //collect information about conjunctions
- if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
- //try to phrase as single invocation property
- bool singleInvocation = true;
- Trace("cegqi-analyze") << "...success." << std::endl;
- std::map< Node, std::vector< Node > > invocations;
- std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args;
- std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from;
- for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
- for( unsigned j=0; j<it->second.size(); j++ ){
- Node conj = it->second[j];
- Trace("cegqi-analyze-debug") << "Process child " << conj << " from " << it->first << std::endl;
- std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj );
- if( itp!=prog_invoke.end() ){
- for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
- if( it2->second.size()>1 ){
- singleInvocation = false;
- break;
- }else if( it2->second.size()==1 ){
- Node prog = it2->first;
- Node inv = it2->second[0];
- Assert( inv[0]==prog );
- invocations[prog].push_back( inv );
- for( unsigned k=1; k<inv.getNumChildren(); k++ ){
- Node arg = inv[k];
- Trace("cegqi-analyze-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl;
- single_invoke_args_from[prog][k-1][arg].push_back( conj );
- if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){
- single_invoke_args[prog][k-1].push_back( arg );
- }
- }
- }
- }
- }
- }
- }
- if( singleInvocation ){
- Trace("cegqi-analyze") << "Property is single invocation with : " << std::endl;
- std::vector< Node > pbvs;
- std::vector< Node > new_vars;
- std::map< Node, std::vector< Node > > new_assumptions;
- for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
- Assert( !it->second.empty() );
- Node prog = it->first;
- Node inv = it->second[0];
- std::vector< Node > invc;
- invc.push_back( inv.getOperator() );
- invc.push_back( prog );
- Node pv = NodeManager::currentNM()->mkBoundVar( "F", inv.getType() );
- d_single_inv_map[prog] = pv;
- d_single_inv_map_to_prog[pv] = prog;
- pbvs.push_back( pv );
- Trace("cegqi-analyze-debug2") << "Make variable " << pv << " for " << prog << std::endl;
- for( unsigned k=1; k<inv.getNumChildren(); k++ ){
- Assert( !single_invoke_args[prog][k-1].empty() );
- if( single_invoke_args[prog][k-1].size()==1 ){
- invc.push_back( single_invoke_args[prog][k-1][0] );
- }else{
- //introduce fresh variable, assign all
- Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
- new_vars.push_back( v );
- invc.push_back( v );
-
- for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
- Node arg = single_invoke_args[prog][k-1][i];
- Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate();
- Trace("cegqi-analyze-debug") << " ..." << arg << " occurs in ";
- Trace("cegqi-analyze-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl;
- for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){
- Node conj = single_invoke_args_from[prog][k-1][arg][j];
- Trace("cegqi-analyze-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
- Trace("cegqi-analyze-debug") << " ...add assumption " << asum << " to " << conj << std::endl;
- if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){
- new_assumptions[conj].push_back( asum );
- }
- }
- }
- }
- }
- Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc );
- Trace("cegqi-analyze") << " " << prog << " -> " << sinv << std::endl;
- d_single_inv_app_map[prog] = sinv;
- }
- //construct the single invocation version of the property
- Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl;
- //std::vector< Node > si_conj;
- Assert( !pbvs.empty() );
- Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
- for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
- //should hold since we prevent miniscoping
- Assert( d_single_inv.isNull() );
- std::vector< Node > tmp;
- for( unsigned i=0; i<it->second.size(); i++ ){
- Node c = it->second[i];
- std::vector< Node > disj;
- //insert new assumptions
- disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() );
- //get replaced version
- Node cr;
- std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c );
- if( itp!=prog_invoke.end() ){
- std::vector< Node > terms;
- std::vector< Node > subs;
- for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
- if( !it2->second.empty() ){
- Node prog = it2->first;
- Node inv = it2->second[0];
- Assert( it2->second.size()==1 );
- terms.push_back( inv );
- subs.push_back( d_single_inv_map[prog] );
- Trace("cegqi-analyze-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
- }
- }
- cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
- }else{
- cr = c;
- }
- if( cr.getKind()==OR ){
- for( unsigned j=0; j<cr.getNumChildren(); j++ ){
- disj.push_back( cr[j] );
- }
- }else{
- disj.push_back( cr );
- }
- Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
- Trace("cegqi-analyze") << " " << curr;
- tmp.push_back( curr.negate() );
- if( !it->first.isNull() ){
- Trace("cegqi-analyze-debug") << " under " << it->first;
- }
- Trace("cegqi-analyze") << std::endl;
- }
- Assert( !tmp.empty() );
- Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp );
- if( !it->first.isNull() ){
- // apply substitution for skolem variables
- std::vector< Node > vars;
- d_single_inv_arg_sk.clear();
- for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
- std::stringstream ss;
- ss << "k_" << it->first[j];
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
- vars.push_back( it->first[j] );
- d_single_inv_arg_sk.push_back( v );
- }
- bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() );
-
- Trace("cegqi-analyze-debug") << " -> " << bd << std::endl;
- }
- d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
- //equality resolution
- for( unsigned j=0; j<tmp.size(); j++ ){
- Node conj = tmp[j];
- std::map< Node, std::vector< Node > > case_vals;
- bool exh = processSingleInvLiteral( conj, false, case_vals );
- Trace("cegqi-analyze-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
- for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
- Trace("cegqi-analyze-er") << " " << it->first << " -> ";
- for( unsigned k=0; k<it->second.size(); k++ ){
- Trace("cegqi-analyze-er") << it->second[k] << " ";
- }
- Trace("cegqi-analyze-er") << std::endl;
- }
-
- }
- }
- Trace("cegqi-analyze-debug") << "...formula is : " << d_single_inv << std::endl;
- }else{
- Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
- }
- }
-}
-
-bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
- if( lit.getKind()==NOT ){
- return processSingleInvLiteral( lit[0], !pol, case_vals );
- }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
- bool exh = true;
- for( unsigned k=0; k<lit.getNumChildren(); k++ ){
- bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
- exh = exh && curr;
- }
- return exh;
- }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
- if( pol ){
- for( unsigned r=0; r<2; r++ ){
- std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
- if( it!=d_single_inv_map_to_prog.end() ){
- if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
- case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
- return true;
- }
- }
- }
- }
- }
- return false;
-}
-
-bool CegInstantiation::CegConjecture::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
- std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
- std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
- if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
- return false;
- }
- }
- }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){
- if( !p.isNull() ){
- //do not allow nested quantifiers
- return false;
- }
- analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
- }else{
- if( pol ){
- n = n.negate();
- }
- Trace("cegqi-analyze") << "Sygus conjunct : " << n << std::endl;
- children[p].push_back( n );
- for( unsigned i=0; i<progs.size(); i++ ){
- prog_invoke[n][progs[i]].clear();
- }
- bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] );
- for( unsigned i=0; i<progs.size(); i++ ){
- std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] );
- Trace("cegqi-analyze") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
- for( unsigned j=0; j<it->second.size(); j++ ){
- Trace("cegqi-analyze") << " " << it->second[j] << std::endl;
- }
- }
- return success;
- }
- return true;
-}
-
-bool CegInstantiation::CegConjecture::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) {
- if( n.getNumChildren()>0 ){
- if( n.getKind()==FORALL ){
- //do not allow nested quantifiers
- return false;
- }
- //look at first argument in evaluator
- Node p = n[0];
- std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p );
- if( it!=prog_invoke.end() ){
- if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){
- it->second.push_back( n );
- }
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){
- return false;
- }
- }
- }else{
- //record this conjunct contains n
- contains[n] = true;
- }
- return true;
-}
-
-void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
+void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
if( d_guard.isNull() ){
d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
//specify guard behavior
Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
qe->getOutputChannel().lemma( lem );
- }else if( !d_single_inv.isNull() ){
- Assert( d_single_inv.getKind()==FORALL );
- std::vector< Node > vars;
- d_single_inv_sk.clear();
- for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
- std::stringstream ss;
- ss << "k_" << d_single_inv[0][i];
- Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
- vars.push_back( d_single_inv[0][i] );
- d_single_inv_sk.push_back( k );
- }
- Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
- Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() );
- Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
- qe->getOutputChannel().lemma( lem );
- if( Trace.isOn("cegqi-debug") ){
- lem = Rewriter::rewrite( lem );
- Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+ }else if( d_ceg_si ){
+ Node lem = d_ceg_si->getSingleInvLemma( d_guard );
+ if( !lem.isNull() ){
+ Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
+ qe->getOutputChannel().lemma( lem );
+ if( Trace.isOn("cegqi-debug") ){
+ lem = Rewriter::rewrite( lem );
+ Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+ }
}
}
}
}
-Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
if( d_measure_term.isNull() ){
return Node::null();
}else{
CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
d_conj = new CegConjecture( d_quantEngine->getSatContext() );
+ d_last_inst_si = false;
}
bool CegInstantiation::needsCheck( Theory::Effort e ) {
if( conj->d_ce_sk.empty() ){
Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl;
if( getTermDatabase()->isQAttrSygus( q ) ){
-
+ if( conj->d_ceg_si ){
+ std::vector< Node > lems;
+ conj->d_ceg_si->check( d_quantEngine, lems );
+ if( !lems.empty() ){
+ d_last_inst_si = true;
+ for( unsigned j=0; j<lems.size(); j++ ){
+ Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl;
+ d_quantEngine->addLemma( lems[j] );
+ }
+ Trace("cegqi-engine") << " ...try single invocation." << std::endl;
+ return;
+ }
+ }
std::vector< Node > model_values;
if( getModelValues( conj, conj->d_candidates, model_values ) ){
//check if we must apply fairness lemmas
- std::vector< Node > lems;
if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+ std::vector< Node > lems;
for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
}
- }
- if( !lems.empty() ){
- for( unsigned j=0; j<lems.size(); j++ ){
- Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
- d_quantEngine->addLemma( lems[j] );
- }
- Trace("cegqi-engine") << " ...refine size." << std::endl;
- }else{
- //must get a counterexample to the value of the current candidate
- Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
- //check whether we will run CEGIS on inner skolem variables
- bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
- if( sk_refine ){
- conj->d_ce_sk.push_back( std::vector< Node >() );
+ if( !lems.empty() ){
+ for( unsigned j=0; j<lems.size(); j++ ){
+ Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
+ d_quantEngine->addLemma( lems[j] );
+ }
+ Trace("cegqi-engine") << " ...refine size." << std::endl;
+ return;
}
- std::vector< Node > ic;
- ic.push_back( q.negate() );
- std::vector< Node > d;
- collectDisjuncts( inst, d );
- Assert( d.size()==conj->d_base_disj.size() );
- //immediately skolemize inner existentials
- for( unsigned i=0; i<d.size(); i++ ){
- Node dr = Rewriter::rewrite( d[i] );
- if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
- ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
- if( sk_refine ){
- conj->d_ce_sk.back().push_back( dr[0] );
- }
- }else{
- ic.push_back( dr );
- if( sk_refine ){
- conj->d_ce_sk.back().push_back( Node::null() );
- }
- if( !conj->d_inner_vars_disj[i].empty() ){
- Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
- }
+ }
+ //must get a counterexample to the value of the current candidate
+ Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
+ //check whether we will run CEGIS on inner skolem variables
+ bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
+ if( sk_refine ){
+ conj->d_ce_sk.push_back( std::vector< Node >() );
+ }
+ std::vector< Node > ic;
+ ic.push_back( q.negate() );
+ std::vector< Node > d;
+ collectDisjuncts( inst, d );
+ Assert( d.size()==conj->d_base_disj.size() );
+ //immediately skolemize inner existentials
+ for( unsigned i=0; i<d.size(); i++ ){
+ Node dr = Rewriter::rewrite( d[i] );
+ if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+ ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+ if( sk_refine ){
+ conj->d_ce_sk.back().push_back( dr[0] );
+ }
+ }else{
+ ic.push_back( dr );
+ if( sk_refine ){
+ conj->d_ce_sk.back().push_back( Node::null() );
+ }
+ if( !conj->d_inner_vars_disj[i].empty() ){
+ Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
}
}
- Node lem = NodeManager::currentNM()->mkNode( OR, ic );
- lem = Rewriter::rewrite( lem );
- Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
- d_quantEngine->addLemma( lem );
- Trace("cegqi-engine") << " ...find counterexample." << std::endl;
}
+ Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+ lem = Rewriter::rewrite( lem );
+ d_last_inst_si = false;
+ Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+ d_quantEngine->addLemma( lem );
+ Trace("cegqi-engine") << " ...find counterexample." << std::endl;
}
}else if( getTermDatabase()->isQAttrSynthesis( q ) ){
Assert( dt.isSygus() );
out << dt.getSygusVarList() << " ";
out << dt.getSygusType() << " ";
- if( d_conj->d_candidate_inst[i].empty() ){
- out << "?";
+ if( d_last_inst_si ){
+ Assert( d_conj->d_ceg_si );
+ Node sol = d_conj->d_ceg_si->getSolution( i, Node::fromExpr( dt.getSygusVarList() ) );
+ out << sol;
}else{
- printSygusTerm( out, d_conj->d_candidate_inst[i].back() );
+ if( d_conj->d_candidate_inst[i].empty() ){
+ out << "?";
+ }else{
+ printSygusTerm( out, d_conj->d_candidate_inst[i].back() );
+ }
}
out << ")" << std::endl;
}
out << n;
}
+void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
+ if( n.getKind()==OR ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ collectDisjuncts( n[i], d );
+ }
+ }else{
+ d.push_back( n );
+ }
+}
+
}
#include "cvc4_private.h"
-#ifndef CE_GUIDED_INSTANTIATION_H
-#define CE_GUIDED_INSTANTIATION_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
#include "context/cdhashmap.h"
#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
+/** a synthesis conjecture */
+class CegConjecture {
+public:
+ CegConjecture( context::Context* c );
+ /** is conjecture active */
+ context::CDO< bool > d_active;
+ /** is conjecture infeasible */
+ context::CDO< bool > d_infeasible;
+ /** quantified formula */
+ Node d_quant;
+ /** guard */
+ Node d_guard;
+ /** base instantiation */
+ Node d_base_inst;
+ /** expand base inst to disjuncts */
+ std::vector< Node > d_base_disj;
+ /** guard split */
+ Node d_guard_split;
+ /** is syntax-guided */
+ bool d_syntax_guided;
+ /** list of constants for quantified formula */
+ std::vector< Node > d_candidates;
+ /** list of variables on inner quantification */
+ std::vector< Node > d_inner_vars;
+ std::vector< std::vector< Node > > d_inner_vars_disj;
+ /** list of terms we have instantiated candidates with */
+ std::map< int, std::vector< Node > > d_candidate_inst;
+ /** initialize guard */
+ void initializeGuard( QuantifiersEngine * qe );
+ /** measure term */
+ Node d_measure_term;
+ /** measure sum size */
+ int d_measure_term_size;
+ /** refine count */
+ unsigned d_refine_count;
+ /** assign */
+ void assign( QuantifiersEngine * qe, Node q );
+ /** is assigned */
+ bool isAssigned() { return !d_quant.isNull(); }
+ /** current extential quantifeirs whose couterexamples we must refine */
+ std::vector< std::vector< Node > > d_ce_sk;
+ /** single invocation utility */
+ CegConjectureSingleInv * d_ceg_si;
+public: //for fairness
+ /** the cardinality literals */
+ std::map< int, Node > d_lits;
+ /** current cardinality */
+ context::CDO< int > d_curr_lit;
+ /** allocate literal */
+ Node getLiteral( QuantifiersEngine * qe, int i );
+ /** is ground */
+ bool isGround() { return d_inner_vars.empty(); }
+};
+
+
class CegInstantiation : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
- /** collect disjuncts */
- static void collectDisjuncts( Node n, std::vector< Node >& ex );
- /** a synthesis conjecture */
- class CegConjecture {
- public:
- CegConjecture( context::Context* c );
- /** is conjecture active */
- context::CDO< bool > d_active;
- /** is conjecture infeasible */
- context::CDO< bool > d_infeasible;
- /** quantified formula */
- Node d_quant;
- /** guard */
- Node d_guard;
- /** base instantiation */
- Node d_base_inst;
- /** expand base inst to disjuncts */
- std::vector< Node > d_base_disj;
- /** guard split */
- Node d_guard_split;
- /** is syntax-guided */
- bool d_syntax_guided;
- /** list of constants for quantified formula */
- std::vector< Node > d_candidates;
- /** list of variables on inner quantification */
- std::vector< Node > d_inner_vars;
- std::vector< std::vector< Node > > d_inner_vars_disj;
- /** list of terms we have instantiated candidates with */
- std::map< int, std::vector< Node > > d_candidate_inst;
- /** initialize guard */
- void initializeGuard( QuantifiersEngine * qe );
- /** measure term */
- Node d_measure_term;
- /** measure sum size */
- int d_measure_term_size;
- /** refine count */
- unsigned d_refine_count;
- /** assign */
- void assign( QuantifiersEngine * qe, Node q );
- /** is assigned */
- bool isAssigned() { return !d_quant.isNull(); }
- /** current extential quantifeirs whose couterexamples we must refine */
- std::vector< std::vector< Node > > d_ce_sk;
- private: //for single invocation
- void analyzeSygusConjecture();
- bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
- std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
- std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
- bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
- bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
- public:
- Node d_single_inv;
- //map from programs to variables in single invocation property
- std::map< Node, Node > d_single_inv_map;
- std::map< Node, Node > d_single_inv_map_to_prog;
- //map from programs to evaluator term representing the above variable
- std::map< Node, Node > d_single_inv_app_map;
- //list of skolems for each argument of programs
- std::vector< Node > d_single_inv_arg_sk;
- //list of skolems for each program
- std::vector< Node > d_single_inv_sk;
- public: //for fairness
- /** the cardinality literals */
- std::map< int, Node > d_lits;
- /** current cardinality */
- context::CDO< int > d_curr_lit;
- /** allocate literal */
- Node getLiteral( QuantifiersEngine * qe, int i );
- /** is ground */
- bool isGround() { return d_inner_vars.empty(); }
- };
/** the quantified formula stating the synthesis conjecture */
CegConjecture * d_conj;
+ /** last instantiation by single invocation module? */
+ bool d_last_inst_si;
private: //for enforcing fairness
/** measure functions */
std::map< TypeNode, Node > d_uf_measure;
std::string identify() const { return "CegInstantiation"; }
/** print solution for synthesis conjectures */
void printSynthSolution( std::ostream& out );
+ /** collect disjuncts */
+ static void collectDisjuncts( Node n, std::vector< Node >& ex );
};
}
--- /dev/null
+/********************* */
+/*! \file ce_guided_single_inv.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/datatype.h"
+#include "theory/quantifiers/quant_util.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegConjectureSingleInv::CegConjectureSingleInv( Node q, CegConjecture * p ) : d_parent( p ), d_quant( q ){
+
+}
+
+Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
+ if( !d_single_inv.isNull() ) {
+ Assert( d_single_inv.getKind()==FORALL );
+ d_single_inv_var.clear();
+ d_single_inv_sk.clear();
+ for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+ std::stringstream ss;
+ ss << "k_" << d_single_inv[0][i];
+ Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+ d_single_inv_var.push_back( d_single_inv[0][i] );
+ d_single_inv_sk.push_back( k );
+ d_single_inv_sk_index[k] = i;
+ }
+ Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+ Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
+ return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst.negate() );
+ }else{
+ return Node::null();
+ }
+}
+
+void CegConjectureSingleInv::initialize() {
+ Node q = d_quant;
+ Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl;
+ // conj -> conj*
+ std::map< Node, std::vector< Node > > children;
+ // conj X prog -> inv*
+ std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke;
+ std::vector< Node > progs;
+ std::map< Node, std::map< Node, bool > > contains;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ progs.push_back( q[0][i] );
+ }
+ //collect information about conjunctions
+ if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
+ //try to phrase as single invocation property
+ bool singleInvocation = true;
+ Trace("cegqi-si") << "...success." << std::endl;
+ std::map< Node, std::vector< Node > > invocations;
+ std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args;
+ std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from;
+ for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
+ for( unsigned j=0; j<it->second.size(); j++ ){
+ Node conj = it->second[j];
+ Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl;
+ std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj );
+ if( itp!=prog_invoke.end() ){
+ for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
+ if( it2->second.size()>1 ){
+ singleInvocation = false;
+ break;
+ }else if( it2->second.size()==1 ){
+ Node prog = it2->first;
+ Node inv = it2->second[0];
+ Assert( inv[0]==prog );
+ invocations[prog].push_back( inv );
+ for( unsigned k=1; k<inv.getNumChildren(); k++ ){
+ Node arg = inv[k];
+ Trace("cegqi-si-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl;
+ single_invoke_args_from[prog][k-1][arg].push_back( conj );
+ if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){
+ single_invoke_args[prog][k-1].push_back( arg );
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ if( singleInvocation ){
+ Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
+ std::vector< Node > pbvs;
+ std::vector< Node > new_vars;
+ std::map< Node, std::vector< Node > > new_assumptions;
+ for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
+ Assert( !it->second.empty() );
+ Node prog = it->first;
+ Node inv = it->second[0];
+ std::vector< Node > invc;
+ invc.push_back( inv.getOperator() );
+ invc.push_back( prog );
+ std::stringstream ss;
+ ss << "F_" << prog;
+ Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() );
+ d_single_inv_map[prog] = pv;
+ d_single_inv_map_to_prog[pv] = prog;
+ pbvs.push_back( pv );
+ Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl;
+ for( unsigned k=1; k<inv.getNumChildren(); k++ ){
+ Assert( !single_invoke_args[prog][k-1].empty() );
+ if( single_invoke_args[prog][k-1].size()==1 ){
+ invc.push_back( single_invoke_args[prog][k-1][0] );
+ }else{
+ //introduce fresh variable, assign all
+ Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
+ new_vars.push_back( v );
+ invc.push_back( v );
+
+ for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
+ Node arg = single_invoke_args[prog][k-1][i];
+ Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate();
+ Trace("cegqi-si-debug") << " ..." << arg << " occurs in ";
+ Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl;
+ for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){
+ Node conj = single_invoke_args_from[prog][k-1][arg][j];
+ Trace("cegqi-si-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
+ Trace("cegqi-si-debug") << " ...add assumption " << asum << " to " << conj << std::endl;
+ if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){
+ new_assumptions[conj].push_back( asum );
+ }
+ }
+ }
+ }
+ }
+ Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc );
+ Trace("cegqi-si") << " " << prog << " -> " << sinv << std::endl;
+ d_single_inv_app_map[prog] = sinv;
+ }
+ //construct the single invocation version of the property
+ Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
+ //std::vector< Node > si_conj;
+ Assert( !pbvs.empty() );
+ Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+ for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
+ //should hold since we prevent miniscoping
+ Assert( d_single_inv.isNull() );
+ std::vector< Node > tmp;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Node c = it->second[i];
+ std::vector< Node > disj;
+ //insert new assumptions
+ disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() );
+ //get replaced version
+ Node cr;
+ std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c );
+ if( itp!=prog_invoke.end() ){
+ std::vector< Node > terms;
+ std::vector< Node > subs;
+ for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
+ if( !it2->second.empty() ){
+ Node prog = it2->first;
+ Node inv = it2->second[0];
+ Assert( it2->second.size()==1 );
+ terms.push_back( inv );
+ subs.push_back( d_single_inv_map[prog] );
+ Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
+ }
+ }
+ cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+ }else{
+ cr = c;
+ }
+ if( cr.getKind()==OR ){
+ for( unsigned j=0; j<cr.getNumChildren(); j++ ){
+ disj.push_back( cr[j] );
+ }
+ }else{
+ disj.push_back( cr );
+ }
+ Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
+ Trace("cegqi-si") << " " << curr;
+ tmp.push_back( curr.negate() );
+ if( !it->first.isNull() ){
+ Trace("cegqi-si-debug") << " under " << it->first;
+ }
+ Trace("cegqi-si") << std::endl;
+ }
+ Assert( !tmp.empty() );
+ Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp );
+ if( !it->first.isNull() ){
+ // apply substitution for skolem variables
+ std::vector< Node > vars;
+ d_single_inv_arg_sk.clear();
+ for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+ std::stringstream ss;
+ ss << "k_" << it->first[j];
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+ vars.push_back( it->first[j] );
+ d_single_inv_arg_sk.push_back( v );
+ }
+ bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() );
+
+ Trace("cegqi-si-debug") << " -> " << bd << std::endl;
+ }
+ d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+ //equality resolution
+ for( unsigned j=0; j<tmp.size(); j++ ){
+ Node conj = tmp[j];
+ std::map< Node, std::vector< Node > > case_vals;
+ bool exh = processSingleInvLiteral( conj, false, case_vals );
+ Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
+ for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
+ Trace("cegqi-si-er") << " " << it->first << " -> ";
+ for( unsigned k=0; k<it->second.size(); k++ ){
+ Trace("cegqi-si-er") << it->second[k] << " ";
+ }
+ Trace("cegqi-si-er") << std::endl;
+ }
+
+ }
+ }
+ Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+ }else{
+ Trace("cegqi-si") << "Property is not single invocation." << std::endl;
+ if( options::cegqiSingleInvAbort() ){
+ Message() << "Property is not single invocation." << std::endl;
+ exit( 0 );
+ }
+ }
+ }
+}
+
+bool CegConjectureSingleInv::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
+ if( lit.getKind()==NOT ){
+ return processSingleInvLiteral( lit[0], !pol, case_vals );
+ }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
+ bool exh = true;
+ for( unsigned k=0; k<lit.getNumChildren(); k++ ){
+ bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
+ exh = exh && curr;
+ }
+ return exh;
+ }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+ if( pol ){
+ for( unsigned r=0; r<2; r++ ){
+ std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
+ if( it!=d_single_inv_map_to_prog.end() ){
+ if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
+ case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
+ return true;
+ }
+ }
+ }
+ }
+ }
+ return false;
+}
+
+bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
+ std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+ std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
+ if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
+ return false;
+ }
+ }
+ }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){
+ if( !p.isNull() ){
+ //do not allow nested quantifiers
+ return false;
+ }
+ analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
+ }else{
+ if( pol ){
+ n = n.negate();
+ }
+ Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl;
+ children[p].push_back( n );
+ for( unsigned i=0; i<progs.size(); i++ ){
+ prog_invoke[n][progs[i]].clear();
+ }
+ bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] );
+ for( unsigned i=0; i<progs.size(); i++ ){
+ std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] );
+ Trace("cegqi-si") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
+ for( unsigned j=0; j<it->second.size(); j++ ){
+ Trace("cegqi-si") << " " << it->second[j] << std::endl;
+ }
+ }
+ return success;
+ }
+ return true;
+}
+
+bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) {
+ if( n.getNumChildren()>0 ){
+ if( n.getKind()==FORALL ){
+ //do not allow nested quantifiers
+ return false;
+ }
+ //look at first argument in evaluator
+ Node p = n[0];
+ std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p );
+ if( it!=prog_invoke.end() ){
+ if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){
+ it->second.push_back( n );
+ }
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){
+ return false;
+ }
+ }
+ }else{
+ //record this conjunct contains n
+ contains[n] = true;
+ }
+ return true;
+}
+
+
+void CegConjectureSingleInv::check( QuantifiersEngine * qe, std::vector< Node >& lems ) {
+ if( !d_single_inv.isNull() ) {
+ eq::EqualityEngine* ee = qe->getMasterEqualityEngine();
+ Trace("cegqi-engine") << " * single invocation: " << std::endl;
+ std::vector< Node > subs;
+ std::map< Node, int > subs_from_model;
+ std::vector< Node > waiting_to_slv;
+ for( unsigned i=0; i<d_single_inv_sk.size(); i++ ){
+ Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+ Node pv = d_single_inv_sk[i];
+ Trace("cegqi-engine") << " * " << v;
+ Trace("cegqi-engine") << " (" << pv << ")";
+ Trace("cegqi-engine") << " -> ";
+ Node slv;
+ if( ee->hasTerm( pv ) ){
+ Node r = ee->getRepresentative( pv );
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ bool isWaitingSlv = false;
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ if( n!=pv ){
+ if( slv.isNull() || isWaitingSlv ){
+ std::vector< Node > vars;
+ collectProgVars( n, vars );
+ if( slv.isNull() || vars.empty() ){
+ // n cannot contain pv
+ bool isLoop = std::find( vars.begin(), vars.end(), pv )!=vars.end();
+ if( !isLoop ){
+ for( unsigned j=0; j<vars.size(); j++ ){
+ if( std::find( waiting_to_slv.begin(), waiting_to_slv.end(), vars[j] )!=waiting_to_slv.end() ){
+ isLoop = true;
+ break;
+ }
+ }
+ if( !isLoop ){
+ slv = n;
+ isWaitingSlv = !vars.empty();
+ }
+ }
+ }
+ }
+ }
+ ++eqc_i;
+ }
+ if( isWaitingSlv ){
+ Trace("cegqi-engine-debug") << "waiting:";
+ waiting_to_slv.push_back( pv );
+ }
+ }else{
+ Trace("cegqi-engine-debug") << "N/A:";
+ }
+ if( slv.isNull() ){
+ //get model value
+ Node mv = qe->getModel()->getValue( pv );
+ subs.push_back( mv );
+ subs_from_model[pv] = i;
+ if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){
+ Trace("cegqi-engine") << "M:" << mv;
+ }
+ }else{
+ subs.push_back( slv );
+ Trace("cegqi-engine") << slv;
+ }
+ Trace("cegqi-engine") << std::endl;
+ }
+ for( int i=(int)(waiting_to_slv.size()-1); i>=0; --i ){
+ int index = d_single_inv_sk_index[waiting_to_slv[i]];
+ Trace("cegqi-engine-debug") << "Go back and solve " << d_single_inv_sk[index] << std::endl;
+ Trace("cegqi-engine-debug") << "Substitute " << subs[index] << " to ";
+ subs[index] = applyProgVarSubstitution( subs[index], subs_from_model, subs );
+ Trace("cegqi-engine-debug") << subs[index] << std::endl;
+ }
+ //try to improve substitutions : look for terms that contain terms in question
+ if( !subs_from_model.empty() ){
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+ while( !eqcs_i.isFinished() ){
+ Node r = *eqcs_i;
+ int res = -1;
+ Node slv_n;
+ Node const_n;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ if( slv_n.isNull() || const_n.isNull() ){
+ std::vector< Node > vars;
+ int curr_res = classifyTerm( n, subs_from_model );
+ Trace("cegqi-si-debug2") << "Term : " << n << " classify : " << curr_res << std::endl;
+ if( curr_res!=-2 ){
+ if( curr_res!=-1 && slv_n.isNull() ){
+ res = curr_res;
+ slv_n = n;
+ }else if( const_n.isNull() ){
+ const_n = n;
+ }
+ }
+ }
+ ++eqc_i;
+ }
+ if( !slv_n.isNull() && !const_n.isNull() ){
+ if( slv_n.getType().isInteger() || slv_n.getType().isReal() ){
+ Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[res] << " based on " << slv_n << " = " << const_n << std::endl;
+ subs_from_model.erase( d_single_inv_sk[res] );
+ Node prev_subs_res = subs[res];
+ subs[res] = d_single_inv_sk[res];
+ Node eq = slv_n.eqNode( const_n );
+ bool success = false;
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( eq, msum ) ){
+ Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
+ QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
+ Node veq;
+ if( QuantArith::isolate( d_single_inv_sk[res], msum, veq, EQUAL ) ){
+ Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[res] << " : " << veq << std::endl;
+ Node sol;
+ for( unsigned r=0; r<2; r++ ){
+ if( veq[r]==d_single_inv_sk[res] ){
+ sol = veq[ r==0 ? 1 : 0 ];
+ }
+ }
+ if( !sol.isNull() ){
+ sol = applyProgVarSubstitution( sol, subs_from_model, subs );
+ Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
+ subs[res] = sol;
+ Trace("cegqi-engine") << " ...by arithmetic, " << d_single_inv_sk[res] << " -> " << sol << std::endl;
+ success = true;
+ }
+ }
+ }
+ if( !success ){
+ subs[res] = prev_subs_res;
+ }
+ }
+ }
+ ++eqcs_i;
+ }
+ }
+ Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
+ lem = Rewriter::rewrite( lem );
+ Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
+ if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
+ lems.push_back( lem );
+ d_lemmas_produced.push_back( lem );
+ d_inst.push_back( std::vector< Node >() );
+ d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+ }
+ }
+}
+
+Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
+ std::vector< Node > vars;
+ collectProgVars( n, vars );
+ if( !vars.empty() ){
+ std::vector< Node > ssubs;
+ //get substitution
+ for( unsigned i=0; i<vars.size(); i++ ){
+ Assert( d_single_inv_sk_index.find( vars[i] )!=d_single_inv_sk_index.end() );
+ int index = d_single_inv_sk_index[vars[i]];
+ ssubs.push_back( subs[index] );
+ //it is now constrained
+ if( subs_from_model.find( vars[i] )!=subs_from_model.end() ){
+ subs_from_model.erase( vars[i] );
+ }
+ }
+ return n.substitute( vars.begin(), vars.end(), ssubs.begin(), ssubs.end() );
+ }else{
+ return n;
+ }
+}
+
+int CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model ) {
+ if( n.getKind()==SKOLEM ){
+ std::map< Node, int >::iterator it = subs_from_model.find( n );
+ if( it!=subs_from_model.end() ){
+ return it->second;
+ }else{
+ // if it is symbolic argument, we are also fine
+ if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){
+ return -1;
+ }else{
+ //if it is another program, we are also fine
+ if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+ return -1;
+ }else{
+ return -2;
+ }
+ }
+ }
+ }else{
+ int curr_res = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ int res = classifyTerm( n[i], subs_from_model );
+ if( res==-2 ){
+ return res;
+ }else if( res!=-1 ){
+ curr_res = res;
+ }
+ }
+ return curr_res;
+ }
+}
+
+void CegConjectureSingleInv::collectProgVars( Node n, std::vector< Node >& vars ) {
+ if( n.getKind()==SKOLEM ){
+ if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+ if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+ vars.push_back( n );
+ }
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ collectProgVars( n[i], vars );
+ }
+ }
+}
+
+Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+ Assert( index<d_inst.size() );
+ Assert( i<d_inst[index].size() );
+ if( index==d_inst.size()-1 ){
+ return d_inst[index][i];
+ }else{
+ Node cond = d_lemmas_produced[index];
+ Node ite1 = d_inst[index][i];
+ Node ite2 = constructSolution( i, index+1 );
+ return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
+ }
+}
+
+Node CegConjectureSingleInv::getSolution( unsigned i, Node varList ){
+ Assert( !d_lemmas_produced.empty() );
+ Node s = constructSolution( i, 0 );
+ //TODO : not in grammar
+ std::vector< Node > vars;
+ for( unsigned i=0; i<varList.getNumChildren(); i++ ){
+ vars.push_back( varList[i] );
+ }
+ Assert( vars.size()==d_single_inv_arg_sk.size() );
+ s = s.substitute( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), vars.begin(), vars.end() );
+ return s;
+}
+
+}
\ No newline at end of file
--- /dev/null
+/********************* */
+/*! \file ce_guided_single_inv.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+class CegConjectureSingleInv
+{
+private:
+ CegConjecture * d_parent;
+ bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
+ std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+ std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
+ bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
+ bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
+
+ Node constructSolution( unsigned i, unsigned index );
+ int classifyTerm( Node n, std::map< Node, int >& subs_from_model );
+ void collectProgVars( Node n, std::vector< Node >& vars );
+ Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
+public:
+ CegConjectureSingleInv( Node q, CegConjecture * p );
+ // original conjecture
+ Node d_quant;
+ // single invocation version of quant
+ Node d_single_inv;
+ //map from programs to variables in single invocation property
+ std::map< Node, Node > d_single_inv_map;
+ std::map< Node, Node > d_single_inv_map_to_prog;
+ //map from programs to evaluator term representing the above variable
+ std::map< Node, Node > d_single_inv_app_map;
+ //list of skolems for each argument of programs
+ std::vector< Node > d_single_inv_arg_sk;
+ //list of skolems for each program
+ std::vector< Node > d_single_inv_sk;
+ std::map< Node, int > d_single_inv_sk_index;
+ //list of skolems for each program
+ std::vector< Node > d_single_inv_var;
+ //lemmas produced
+ std::vector< Node > d_lemmas_produced;
+ std::vector< std::vector< Node > > d_inst;
+public:
+ //get the single invocation lemma
+ Node getSingleInvLemma( Node guard );
+ //initialize
+ void initialize();
+ //check
+ void check( QuantifiersEngine * qe, std::vector< Node >& lems );
+ //get solution
+ Node getSolution( unsigned i, Node varList );
+};
+
+}
+}
+}
+
+#endif
counterexample-guided quantifier instantiation
option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
if and how to apply fairness for cegqi
-option sygusSingleInv --sygus-single-inv bool :default false
+option cegqiSingleInv --cegqi-si bool :default false
process single invocation synthesis conjectures
+option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
+ reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvAbort --cegqi-si-abort bool :default false
+ abort if our synthesis conjecture is not single invocation
+
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
if( r.isOne() ){
veq = negate(veq);
}else{
- //TODO
+ //TODO : lcd computation
return false;
}
}
return tt;
}
+void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) {
+ for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ Trace(c) << " ";
+ if( !it->second.isNull() ){
+ Trace(c) << it->second;
+ if( !it->first.isNull() ){
+ Trace(c) << " * ";
+ }
+ }
+ if( !it->first.isNull() ){
+ Trace(c) << it->first;
+ }
+ Trace(c) << std::endl;
+ }
+ Trace(c) << std::endl;
+}
+
void QuantRelevance::registerQuantifier( Node f ){
//compute symbols in f
static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
static Node negate( Node t );
static Node offset( Node t, int i );
+ static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
};
projects / cvc5.git / commitdiff