From 4db1c674588a280da61033c5a60e33327887c57d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 30 Jan 2015 20:59:05 +0100 Subject: [PATCH] Generalize conflict clauses in sygus sym break, merge caches, refactor. Preparation for single invocation properties. Set output lang to SMT2 for sygus. --- src/main/driver_unified.cpp | 2 + src/theory/datatypes/datatypes_sygus.cpp | 822 +++++++++++------- src/theory/datatypes/datatypes_sygus.h | 75 +- src/theory/datatypes/theory_datatypes.cpp | 18 +- .../quantifiers/ce_guided_instantiation.cpp | 60 +- .../quantifiers/ce_guided_instantiation.h | 2 + src/theory/quantifiers/options | 2 + 7 files changed, 619 insertions(+), 362 deletions(-) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c011671f8..c3372d2c8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -202,6 +202,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { opts.set(options::inputLanguage, language::input::LANG_SYGUS); + //since there is no sygus output language, set this to SMT lib 2 + opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0); } } } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 4e7aaad53..3063e85bb 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -30,73 +30,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -bool SygusSplit::isRegistered( TypeNode tn ) { - return d_register.find( tn )!=d_register.end(); -} - -int SygusSplit::getKindArg( TypeNode tn, Kind k ) { - Assert( isRegistered( tn ) ); - std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn ); - if( itt!=d_kinds.end() ){ - std::map< Kind, int >::iterator it = itt->second.find( k ); - if( it!=itt->second.end() ){ - return it->second; - } - } - return -1; -} - -int SygusSplit::getConstArg( TypeNode tn, Node n ){ - Assert( isRegistered( tn ) ); - std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn ); - if( itt!=d_consts.end() ){ - std::map< Node, int >::iterator it = itt->second.find( n ); - if( it!=itt->second.end() ){ - return it->second; - } - } - return -1; -} - -int SygusSplit::getOpArg( TypeNode tn, Node n ) { - std::map< Node, int >::iterator it = d_ops[tn].find( n ); - if( it!=d_ops[tn].end() ){ - return it->second; - }else{ - return -1; - } -} - -bool SygusSplit::hasKind( TypeNode tn, Kind k ) { - return getKindArg( tn, k )!=-1; -} -bool SygusSplit::hasConst( TypeNode tn, Node n ) { - return getConstArg( tn, n )!=-1; -} -bool SygusSplit::hasOp( TypeNode tn, Node n ) { - return getOpArg( tn, n )!=-1; -} - -bool SygusSplit::isKindArg( TypeNode tn, int i ) { - Assert( isRegistered( tn ) ); - std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn ); - if( itt!=d_arg_kind.end() ){ - return itt->second.find( i )!=itt->second.end(); - }else{ - return false; - } -} - -bool SygusSplit::isConstArg( TypeNode tn, int i ) { - Assert( isRegistered( tn ) ); - std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn ); - if( itt!=d_arg_const.end() ){ - return itt->second.find( i )!=itt->second.end(); - }else{ - return false; - } -} - void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) { Assert( dt.isSygus() ); if( d_splits.find( n )==d_splits.end() ){ @@ -123,7 +56,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex ); - if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){ + if( options::sygusNormalFormArg() && sIndex==1 && pdt[csIndex].getNumArgs()==2 ){ arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] ); tn1 = arg1.getType(); if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){ @@ -221,35 +154,18 @@ void SygusSplit::registerSygusType( TypeNode tn ) { if( d_register[tn].isNull() ){ Trace("sygus-split") << "...not sygus." << std::endl; }else{ - for( unsigned i=0; iregisterSygusType( tn ); //compute the redundant operators for( unsigned i=0; i::iterator it = d_arg_kind[tn].find( i ); - if( it!=d_arg_kind[tn].end() ){ + std::map< int, Kind >::iterator it = d_util->d_arg_kind[tn].find( i ); + if( it!=d_util->d_arg_kind[tn].end() ){ Kind dk; - if( isAntisymmetric( it->second, dk ) ){ - int j = getKindArg( tn, dk ); + if( d_util->isAntisymmetric( it->second, dk ) ){ + int j = d_util->getKindArg( tn, dk ); if( j!=-1 ){ Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl; //check for type mismatches @@ -265,14 +181,11 @@ void SygusSplit::registerSygusType( TypeNode tn ) { } } if( success ){ - Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl; + Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_util->d_arg_kind[tn][i] << " terms." << std::endl; nred = false; } } } - //if( it->second==MINUS || it->second==BITVECTOR_SUB ){ - //} - //NAND,NOR } if( nred ){ Trace("sygus-split-debug") << "Check " << dt[i].getName() << " based on generic rewriting" << std::endl; @@ -307,24 +220,24 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& //get parent kind bool hasParentKind = false; Kind parentKind; - if( isKindArg( tnnp, csIndex ) ){ + if( d_util->isKindArg( tnnp, csIndex ) ){ hasParentKind = true; - parentKind = d_arg_kind[tnnp][csIndex]; + parentKind = d_util->d_arg_kind[tnnp][csIndex]; } for( unsigned i=0; id_arg_kind.find( tnn )!=d_util->d_arg_kind.end() && d_util->d_arg_kind[tnn].find( i )!=d_util->d_arg_kind[tnn].end() ){ + addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_util->d_arg_kind[tnn][i], parentKind, sIndex ); if( !addSplit ){ - Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_arg_kind[tnn][i]; + Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_util->d_arg_kind[tnn][i]; Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl; } - }else if( d_arg_const.find( tnn )!=d_arg_const.end() && d_arg_const[tnn].find( i )!=d_arg_const[tnn].end() ){ - addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_arg_const[tnn][i], parentKind, sIndex ); + }else if( d_util->d_arg_const.find( tnn )!=d_util->d_arg_const.end() && d_util->d_arg_const[tnn].find( i )!=d_util->d_arg_const[tnn].end() ){ + addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_util->d_arg_const[tnn][i], parentKind, sIndex ); if( !addSplit ){ - Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_arg_const[tnn][i]; + Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_util->d_arg_const[tnn][i]; Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl; } } @@ -343,83 +256,81 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& } d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit ); } - if( options::sygusNormalFormArg() ){ - //compute argument relationships for 2-arg constructors - if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){ - int osIndex = sIndex==0 ? 1 : 0; - TypeNode tnno = getArgType( pdt[csIndex], osIndex ); - if( DatatypesRewriter::isTypeDatatype( tnno ) ){ - const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype(); - registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex ); - //compute relationships when doing 0-arg - if( sIndex==0 ){ - Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); - Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); + //compute argument relationships for 2-arg constructors + if( d_util->isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){ + int osIndex = sIndex==0 ? 1 : 0; + TypeNode tnno = getArgType( pdt[csIndex], osIndex ); + if( DatatypesRewriter::isTypeDatatype( tnno ) ){ + const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype(); + registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex ); + //compute relationships when doing 0-arg + if( sIndex==0 ){ + Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); + Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); - Kind parentKind = d_arg_kind[tnnp][csIndex]; - bool isPComm = isComm( parentKind ); - std::map< int, bool > larg_consider; - for( unsigned i=0; i rem_arg; - //collect information about this index - bool isSingularConst = isConstArg( tnno, i ) && isSingularArg( d_arg_const[tnno][i], parentKind, 1 ); - bool argConsider = false; - for( unsigned j=0; ji && tnn==tnno ){ - //based on commutativity - // use term ordering : constructor index of first argument is not greater than constructor index of second argument - rem = true; - Trace("sygus-nf") << "* Sygus norm : commutativity of " << parentKind << " : consider " << dt[j].getSygusOp() << " before " << dto[i].getSygusOp() << std::endl; - }else if( isSingularConst && argConsider ){ - rem = true; - Trace("sygus-nf") << "* Sygus norm : RHS singularity arg " << dto[i].getSygusOp() << " of " << parentKind; - Trace("sygus-nf") << " : do not consider " << dt[j].getSygusOp() << " as first arg." << std::endl; - }else if( isConstArg( tnn, j ) && isSingularArg( d_arg_const[tnn][j], parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){ - rem = true; - Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind; - Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl; - }else{ - if( parentKind!=UNDEFINED_KIND ){ - //&& dto[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){ - std::map< TypeNode, int > var_count; - std::map< int, Node > pre; - Node g1 = d_util->mkGeneric( dt, j, var_count, pre ); - Node g2 = d_util->mkGeneric( dto, i, var_count, pre ); - Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 ); - if( isGenericRedundant( tnnp, g ) ){ - rem = true; - } + Kind parentKind = d_util->d_arg_kind[tnnp][csIndex]; + bool isPComm = d_util->isComm( parentKind ); + std::map< int, bool > larg_consider; + for( unsigned i=0; i rem_arg; + //collect information about this index + bool isSingularConst = d_util->isConstArg( tnno, i ) && d_util->isSingularArg( d_util->d_arg_const[tnno][i], parentKind, 1 ); + bool argConsider = false; + for( unsigned j=0; ji && tnn==tnno ){ + //based on commutativity + // use term ordering : constructor index of first argument is not greater than constructor index of second argument + rem = true; + Trace("sygus-nf") << "* Sygus norm : commutativity of " << parentKind << " : consider " << dt[j].getSygusOp() << " before " << dto[i].getSygusOp() << std::endl; + }else if( isSingularConst && argConsider ){ + rem = true; + Trace("sygus-nf") << "* Sygus norm : RHS singularity arg " << dto[i].getSygusOp() << " of " << parentKind; + Trace("sygus-nf") << " : do not consider " << dt[j].getSygusOp() << " as first arg." << std::endl; + }else if( d_util->isConstArg( tnn, j ) && d_util->isSingularArg( d_util->d_arg_const[tnn][j], parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){ + rem = true; + Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind; + Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl; + }else{ + if( parentKind!=UNDEFINED_KIND ){ + //&& dto[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){ + std::map< TypeNode, int > var_count; + std::map< int, Node > pre; + Node g1 = d_util->mkGeneric( dt, j, var_count, pre ); + Node g2 = d_util->mkGeneric( dto, i, var_count, pre ); + Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 ); + if( isGenericRedundant( tnnp, g ) ){ + rem = true; } } - if( rem ){ - rem_arg[j] = true; - }else{ - argConsider = true; - larg_consider[j] = true; - } } - } - if( !rem_arg.empty() ){ - d_sygus_pc_arg_pos[tnno][csIndex][i].clear(); - Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dto[i].getName() << " : " << std::endl; - for( unsigned j=0; j::iterator it = d_type_value[tn].find( val ); - if( it==d_type_value[tn].end() ){ - Node n; - if( tn.isInteger() || tn.isReal() ){ - Rational c(val); - n = NodeManager::currentNM()->mkConst( c ); - }else if( tn.isBitVector() ){ - unsigned int uv = val; - BitVector bval(tn.getConst(), uv); - n = NodeManager::currentNM()->mkConst(bval); - }else if( tn.isBoolean() ){ - if( val==0 ){ - n = NodeManager::currentNM()->mkConst( false ); - } - } - d_type_value[tn][val] = n; - return n; - }else{ - return it->second; - } -} - -Node SygusSplit::getTypeMaxValue( TypeNode tn ) { - std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn ); - if( it==d_type_max_value.end() ){ - Node n; - if( tn.isBitVector() ){ - n = bv::utils::mkOnes(tn.getConst()); - }else if( tn.isBoolean() ){ - n = NodeManager::currentNM()->mkConst( true ); - } - d_type_max_value[tn] = n; - return n; - }else{ - return it->second; - } -} - //this function gets all easy redundant cases, before consulting rewriters bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) { - Assert( hasKind( tn, k ) ); - Assert( hasKind( tnp, parent ) ); + Assert( d_util->hasKind( tn, k ) ); + Assert( d_util->hasKind( tnp, parent ) ); Trace("sygus-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl; - int c = getKindArg( tn, k ); - int pc = getKindArg( tnp, parent ); + int c = d_util->getKindArg( tn, k ); + int pc = d_util->getKindArg( tnp, parent ); if( k==parent ){ //check for associativity - if( isAssoc( k ) ){ + if( d_util->isAssoc( k ) ){ //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position int firstArg = getFirstArgOccurrence( pdt[pc], dt ); Assert( firstArg!=-1 ); @@ -607,7 +405,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt Trace("sygus-split-debug") << ", reqk = " << reqk; } Trace("sygus-split-debug") << "?" << std::endl; - int pcr = getKindArg( tnp, nk ); + int pcr = d_util->getKindArg( tnp, nk ); if( pcr!=-1 ){ Assert( pcr<(int)pdt.getNumConstructors() ); //must have same number of arguments @@ -619,7 +417,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) ); if( reqk!=UNDEFINED_KIND ){ //child must have a NOT - int nindex = getKindArg( tna, reqk ); + int nindex = d_util->getKindArg( tna, reqk ); if( nindex!=-1 ){ const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype(); childTypes[i] = getArgType( adt[nindex], 0 ); @@ -662,11 +460,11 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt //this function gets all easy redundant cases, before consulting rewriters bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ) { - Assert( hasConst( tn, c ) ); - Assert( hasKind( tnp, parent ) ); - int pc = getKindArg( tnp, parent ); + Assert( d_util->hasConst( tn, c ) ); + Assert( d_util->hasKind( tnp, parent ) ); + int pc = d_util->getKindArg( tnp, parent ); Trace("sygus-split") << "Consider sygus split const " << c << ", parent = " << parent << ", arg = " << arg << "?" << std::endl; - if( isIdempotentArg( c, parent, arg ) ){ + if( d_util->isIdempotentArg( c, parent, arg ) ){ Trace("sygus-split-debug") << " " << c << " is idempotent arg " << arg << " of " << parent << "..." << std::endl; if( pdt[pc].getNumArgs()==2 ){ int oarg = arg==0 ? 1 : 0; @@ -675,9 +473,9 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd return false; } } - }else if( isSingularArg( c, parent, arg ) ){ + }else if( d_util->isSingularArg( c, parent, arg ) ){ Trace("sygus-split-debug") << " " << c << " is singular arg " << arg << " of " << parent << "..." << std::endl; - if( hasConst( tnp, c ) ){ + if( d_util->hasConst( tnp, c ) ){ return false; } } @@ -714,11 +512,7 @@ bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) { 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 = Rewriter::rewrite( g ); - //replace variables in order left to right - std::map< TypeNode, int > var_count; - std::map< Node, Node > subs; - gr = d_util->getSygusNormalized( gr, var_count, subs ); + 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; @@ -839,10 +633,11 @@ bool SygusSymBreak::ProgSearch::processProgramDepth( int depth ){ Trace("sygus-sym-break-debug") << "Program is set for depth " << depth << std::endl; std::map< TypeNode, int > var_count; std::vector< Node > testers; + std::map< Node, std::vector< Node > > testers_u; //now have entire information about candidate program at given depth - Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers ); + 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 ) ){ + if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers, testers_u ) ){ return false; } }else{ @@ -862,10 +657,11 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept Assert( n.getKind()==APPLY_SELECTOR_TOTAL ); std::map< TypeNode, int > var_count; std::vector< Node > testers; + std::map< Node, std::vector< Node > > testers_u; //now have entire information about candidate program at given depth - Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, var_count, testers ); + 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 ) ){ + if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers, testers_u ) ){ return false; } //also try higher levels @@ -877,13 +673,15 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept return true; } -Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) { +Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count, + std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { Assert( depth>=curr_depth ); Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl; NodeMap::const_iterator it = d_testers.find( prog ); if( it!=d_testers.end() ){ Node tst = (*it).second; testers.push_back( tst ); + testers_u[parent].push_back( tst ); Assert( tst[0]==prog ); int tindex = Datatype::indexOf( tst.getOperator().toExpr() ); TypeNode tn = prog.getType(); @@ -893,7 +691,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog if( curr_depthmkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog ); - pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers ); + pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, prog, var_count, testers, testers_u ); if( pre[i].isNull() ){ return Node::null(); } @@ -906,39 +704,164 @@ 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, Node >::iterator it = d_normalized[at].find( prog ); - if( it==d_normalized[at].end() ){ +bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, + std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { + Assert( a.getType()==at ); + std::map< Node, bool >::iterator it = d_redundant[at].find( prog ); + bool red; + if( it==d_redundant[at].end() ){ Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl; - Node progr = Rewriter::rewrite( prog ); - std::map< TypeNode, int > var_count; - std::map< Node, Node > subs; - progr = d_util->getSygusNormalized( progr, var_count, subs ); - Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; - d_normalized[at][prog] = progr; + 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() ){ d_normalized_to_orig[at][progr] = prog; - d_redundant[at][prog] = false; + 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; + d_redundant[at][prog] = true; + red = true; + }else{ + d_redundant[at][prog] = false; + red = false; + } }else{ d_redundant[at][prog] = true; - Assert( !testers.empty() ); + red = true; Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl; } + if( red ){ + Assert( !testers.empty() ); + Assert( prog!=it->second ); + bool conflict_gen_set = false; + if( options::sygusNormalFormGlobalGen() ){ + //generalize conflict + if( prog.getNumChildren()>0 ){ + Assert( !testers.empty() ); + d_util->registerSygusType( at ); + //Trace("sygus-nf-gen-debug") << "Testers are : " << std::endl; + //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; + for( unsigned i=0; igetNormalized( tn, prog[i], true ); + rlv[i] = true; + Trace("sygus-nf-gen") << "- child " << i << " normalizes to " << norm_children[i] << 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() ); + //quick checks based on constants + for( std::map< int, Node >::iterator it = norm_children.begin(); it != norm_children.end(); ++it ){ + if( it->second.isConst() ){ + if( parentOpKind==kind::BUILTIN ){ + Trace("sygus-nf-gen") << "-- constant arg " << it->first << " 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 ){ + rlv[itr->first] = false; + } + } + 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; i " << rl << std::endl; + d_conflict_gen[at][prog].push_back( rl ); + } + } + } + } + if( !conflict_gen_set ){ + for( unsigned i=0; isecond; } - Assert( d_redundant[at].find( prog )!=d_redundant[at].end() ); - if( d_redundant[at][prog] ){ - d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers ); + if( red ){ + Assert( d_conflict_gen[at][prog].size()==testers.size() ); + std::vector< Node > gtesters; + for( unsigned i=0; id_conflictNode = gtesters.size()==1 ? gtesters[0] : NodeManager::currentNM()->mkNode( AND, gtesters ); Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl; d_util->d_conflict = true; - d_redundant[at][prog] = true; - // TODO : generalize conflict return false; }else{ return true; } } +bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, + Kind k, int i, Node arg, std::map< int, 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; + }else if( d_util->isIdempotentArg( arg, k, i ) ){ + if( pdt[pc].getNumArgs()==2 ){ + int oi = i==0 ? 1 : 0; + TypeNode otn = TypeNode::fromType( ((SelectorType)pdt[pc][oi].getType()).getRangeType() ); + if( otn==tnp ){ + return false; + } + } + }else if( d_util->isSingularArg( arg, k, i ) ){ + if( d_util->hasConst( tnp, arg ) ){ + return false; + } + } + TypeNode tn = arg.getType(); + 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 ); + } + } +} + SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) { d_split = new SygusSplit( this ); d_sym_break = new SygusSymBreak( this, c ); @@ -977,6 +900,11 @@ Node SygusUtil::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) { } } +TypeNode SygusUtil::getSygusType( Node v ) { + Assert( d_fv_stype.find( v )!=d_fv_stype.end() ); + return d_fv_stype[v]; +} + Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) { Assert( c>=0 && c<(int)dt.getNumConstructors() ); Assert( dt.isSygus() ); @@ -1004,11 +932,14 @@ Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& if( children.size()==1 ){ return children[0]; }else{ + return NodeManager::currentNM()->mkNode( APPLY, children ); + /* Node n = NodeManager::currentNM()->mkNode( APPLY, children ); //must expand definitions Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) ); Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; return ne; + */ } } } @@ -1048,3 +979,244 @@ Node SygusUtil::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count return n; } } + +Node SygusUtil::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) { + if( do_pre_norm ){ + std::map< TypeNode, int > var_count; + std::map< Node, Node > subs; + prog = getSygusNormalized( prog, var_count, subs ); + } + std::map< Node, Node >::iterator itn = d_normalized[t].find( prog ); + if( itn==d_normalized[t].end() ){ + Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) ); + progr = Rewriter::rewrite( progr ); + std::map< TypeNode, int > var_count; + std::map< Node, Node > subs; + progr = getSygusNormalized( progr, var_count, subs ); + Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; + d_normalized[t][prog] = progr; + return progr; + }else{ + return itn->second; + } +} + + +bool SygusUtil::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; +} + +bool SygusUtil::isComm( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; +} + +bool SygusUtil::isAntisymmetric( Kind k, Kind& dk ) { + if( k==GT ){ + dk = LT; + return true; + }else if( k==GEQ ){ + dk = LEQ; + return true; + }else if( k==BITVECTOR_UGT ){ + dk = BITVECTOR_ULT; + return true; + }else if( k==BITVECTOR_UGE ){ + dk = BITVECTOR_ULE; + return true; + }else if( k==BITVECTOR_SGT ){ + dk = BITVECTOR_SLT; + return true; + }else if( k==BITVECTOR_SGE ){ + dk = BITVECTOR_SLE; + return true; + }else{ + return false; + } +} + +bool SygusUtil::isIdempotentArg( Node n, Kind ik, int arg ) { + TypeNode tn = n.getType(); + if( n==getTypeValue( tn, 0 ) ){ + if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){ + return true; + }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){ + return arg==1; + } + }else if( n==getTypeValue( tn, 1 ) ){ + if( ik==MULT || ik==BITVECTOR_MULT ){ + return true; + }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){ + return arg==1; + } + }else if( n==getTypeMaxValue( tn ) ){ + if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){ + return true; + } + } + return false; +} + + +bool SygusUtil::isSingularArg( Node n, Kind ik, int arg ) { + TypeNode tn = n.getType(); + if( n==getTypeValue( tn, 0 ) ){ + if( ik==AND || ik==MULT || ik==BITVECTOR_AND || ik==BITVECTOR_MULT ){ + return true; + }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){ + return arg==0; + } + }else if( n==getTypeMaxValue( tn ) ){ + if( ik==OR || ik==BITVECTOR_OR ){ + return true; + } + } + return false; +} + + +Node SygusUtil::getTypeValue( TypeNode tn, int val ) { + std::map< int, Node >::iterator it = d_type_value[tn].find( val ); + if( it==d_type_value[tn].end() ){ + Node n; + if( tn.isInteger() || tn.isReal() ){ + Rational c(val); + n = NodeManager::currentNM()->mkConst( c ); + }else if( tn.isBitVector() ){ + unsigned int uv = val; + BitVector bval(tn.getConst(), uv); + n = NodeManager::currentNM()->mkConst(bval); + }else if( tn.isBoolean() ){ + if( val==0 ){ + n = NodeManager::currentNM()->mkConst( false ); + } + } + d_type_value[tn][val] = n; + return n; + }else{ + return it->second; + } +} + +Node SygusUtil::getTypeMaxValue( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn ); + if( it==d_type_max_value.end() ){ + Node n; + if( tn.isBitVector() ){ + n = bv::utils::mkOnes(tn.getConst()); + }else if( tn.isBoolean() ){ + n = NodeManager::currentNM()->mkConst( true ); + } + d_type_max_value[tn] = n; + return n; + }else{ + return it->second; + } +} + +void SygusUtil::registerSygusType( TypeNode tn ){ + if( d_register.find( tn )==d_register.end() ){ + if( !DatatypesRewriter::isTypeDatatype( tn ) ){ + d_register[tn] = TypeNode::null(); + }else{ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl; + d_register[tn] = TypeNode::fromType( dt.getSygusType() ); + if( d_register[tn].isNull() ){ + Trace("sygus-util") << "...not sygus." << std::endl; + }else{ + for( unsigned i=0; i >::iterator itt = d_kinds.find( tn ); + if( itt!=d_kinds.end() ){ + std::map< Kind, int >::iterator it = itt->second.find( k ); + if( it!=itt->second.end() ){ + return it->second; + } + } + return -1; +} + +int SygusUtil::getConstArg( TypeNode tn, Node n ){ + Assert( isRegistered( tn ) ); + std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn ); + if( itt!=d_consts.end() ){ + std::map< Node, int >::iterator it = itt->second.find( n ); + if( it!=itt->second.end() ){ + return it->second; + } + } + return -1; +} + +int SygusUtil::getOpArg( TypeNode tn, Node n ) { + std::map< Node, int >::iterator it = d_ops[tn].find( n ); + if( it!=d_ops[tn].end() ){ + return it->second; + }else{ + return -1; + } +} + +bool SygusUtil::hasKind( TypeNode tn, Kind k ) { + return getKindArg( tn, k )!=-1; +} +bool SygusUtil::hasConst( TypeNode tn, Node n ) { + return getConstArg( tn, n )!=-1; +} +bool SygusUtil::hasOp( TypeNode tn, Node n ) { + return getOpArg( tn, n )!=-1; +} + +bool SygusUtil::isKindArg( TypeNode tn, int i ) { + Assert( isRegistered( tn ) ); + std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn ); + if( itt!=d_arg_kind.end() ){ + return itt->second.find( i )!=itt->second.end(); + }else{ + return false; + } +} + +bool SygusUtil::isConstArg( TypeNode tn, int i ) { + Assert( isRegistered( tn ) ); + std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn ); + if( itt!=d_arg_const.end() ){ + return itt->second.find( i )!=itt->second.end(); + }else{ + return false; + } +} + + + + + diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index cf43b0a31..f30a0fd0a 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -42,16 +42,7 @@ private: std::map< TypeNode, std::vector< bool > > d_sygus_nred; std::map< TypeNode, std::map< int, std::map< int, std::vector< bool > > > > d_sygus_pc_nred; std::map< TypeNode, std::map< int, std::map< int, std::vector< int > > > > d_sygus_pc_arg_pos; - //information for builtin types - std::map< TypeNode, std::map< int, Node > > d_type_value; - std::map< TypeNode, Node > d_type_max_value; - //information for sygus types std::map< TypeNode, TypeNode > d_register; //stores sygus type - std::map< TypeNode, std::map< int, Kind > > d_arg_kind; - std::map< TypeNode, std::map< Kind, int > > d_kinds; - 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; // type to (rewritten) to original std::map< TypeNode, std::map< Node, Node > > d_gen_terms; std::map< TypeNode, std::map< Node, bool > > d_gen_redundant; @@ -76,20 +67,6 @@ private: /** consider sygus split */ bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ); bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ); - /** is assoc */ - bool isAssoc( Kind k ); - /** is comm */ - bool isComm( Kind k ); - /** isAntisymmetric */ - bool isAntisymmetric( Kind k, Kind& dk ); - /** is idempotent arg */ - bool isIdempotentArg( Node n, Kind ik, int arg ); - /** is singular arg */ - bool isSingularArg( Node n, Kind ik, int arg ); - /** get value */ - Node getTypeValue( TypeNode tn, int val ); - /** get value */ - Node getTypeMaxValue( TypeNode tn ); /** get first occurrence */ int getFirstArgOccurrence( const DatatypeConstructor& c, const Datatype& dt ); /** is arg datatype */ @@ -119,12 +96,13 @@ private: typedef context::CDHashMap< int, int > IntIntMap; private: SygusSymBreak * d_parent; - Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ); + Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count, + std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ); bool processProgramDepth( int depth ); bool processSubprograms( Node n, int depth, int odepth ); bool assignTester( Node tst, int depth ); public: - ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) : + ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) : d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) { d_anchor_type = d_anchor.getType(); } @@ -137,11 +115,14 @@ private: void addTester( Node tst ); }; std::map< Node, ProgSearch * > d_prog_search; - std::map< TypeNode, std::map< Node, Node > > d_normalized; 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< bool > > > d_conflict_gen; Node getAnchor( Node n ); - bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ); + 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 ); public: SygusSymBreak( SygusUtil * util, context::Context* c ); /** add tester */ @@ -157,11 +138,51 @@ private: std::map< Node, TypeNode > d_fv_stype; SygusSplit * d_split; SygusSymBreak * d_sym_break; + std::map< TypeNode, std::map< Node, Node > > d_normalized; +private: + //information for sygus types + std::map< TypeNode, TypeNode > d_register; //stores sygus type + std::map< TypeNode, std::map< int, Kind > > d_arg_kind; + std::map< TypeNode, std::map< Kind, int > > d_kinds; + 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; +private: + bool isRegistered( TypeNode tn ); + int getKindArg( TypeNode tn, Kind k ); + int getConstArg( TypeNode tn, Node n ); + int getOpArg( TypeNode tn, Node n ); + bool hasKind( TypeNode tn, Kind k ); + bool hasConst( TypeNode tn, Node n ); + bool hasOp( TypeNode tn, Node n ); + bool isKindArg( TypeNode tn, int i ); + bool isConstArg( TypeNode tn, int i ); + void registerSygusType( TypeNode tn ); +private: + //information for builtin types + std::map< TypeNode, std::map< int, Node > > d_type_value; + std::map< TypeNode, Node > d_type_max_value; + /** is assoc */ + bool isAssoc( Kind k ); + /** is comm */ + bool isComm( Kind k ); + /** isAntisymmetric */ + bool isAntisymmetric( Kind k, Kind& dk ); + /** is idempotent arg */ + bool isIdempotentArg( Node n, Kind ik, int arg ); + /** is singular arg */ + bool isSingularArg( Node n, Kind ik, int arg ); + /** get value */ + Node getTypeValue( TypeNode tn, int val ); + /** 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 ); + Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false ); public: SygusUtil( context::Context* c ); SygusSplit * getSplit() { return d_split; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 264158ed4..42d06cdb5 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -368,10 +368,13 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ if( !d_conflict && polarity ){ Trace("dt-tester") << "Assert tester : " << atom << std::endl; if( d_sygus_util ){ + Assert( !d_sygus_util->d_conflict ); d_sygus_util->getSymBreak()->addTester( atom ); if( d_sygus_util->d_conflict ){ d_conflict = true; - d_conflictNode = d_sygus_util->d_conflictNode; + std::vector< TNode > assumptions; + explain( d_sygus_util->d_conflictNode, assumptions ); + d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); return; @@ -599,8 +602,17 @@ bool TheoryDatatypes::propagate(TNode literal){ void TheoryDatatypes::addAssumptions( std::vector& assumptions, std::vector& tassumptions ) { for( unsigned i=0; imkBoundVar( "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 si_conj; Assert( !pbvs.empty() ); Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); - Node si; for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( si.isNull() ); + //should hold since we prevent miniscoping + Assert( d_single_inv.isNull() ); std::vector< Node > tmp; for( unsigned i=0; isecond.size(); i++ ){ Node c = it->second[i]; @@ -237,15 +238,54 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() { Trace("cegqi-analyze-debug") << " -> " << bd << std::endl; } - si = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + //equality resolution + for( unsigned j=0; j > 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; ksecond.size(); k++ ){ + Trace("cegqi-analyze-er") << it->second[k] << " "; + } + Trace("cegqi-analyze-er") << std::endl; + } + + } } - Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl; - d_single_inv = si; + 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::iterator it = d_single_inv_map_to_prog.find( lit[0] ); + 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, @@ -615,7 +655,13 @@ bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node > for( unsigned i=0; i " << nv << " "; + if( Trace.isOn("cegqi-engine") ){ + TypeNode tn = nv.getType(); + Trace("cegqi-engine") << n[i] << " -> "; + std::stringstream ss; + printSygusTerm( ss, nv ); + Trace("cegqi-engine") << ss.str() << " "; + } if( nv.isNull() ){ success = false; } @@ -752,7 +798,7 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { return; } } - out << n << std::endl; + out << n; } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index ad94b51a5..aa553fb58 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -78,10 +78,12 @@ private: 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 diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 9d4281186..4a093b617 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -204,6 +204,8 @@ 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 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 localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions -- 2.30.2