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() ){
//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 ) ){
if( d_register[tn].isNull() ){
Trace("sygus-split") << "...not sygus." << std::endl;
}else{
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Expr sop = dt[i].getSygusOp();
- Assert( !sop.isNull() );
- Node n = Node::fromExpr( sop );
- Trace("sygus-split") << " Operator #" << i << " : " << sop;
- if( sop.getKind() == kind::BUILTIN ){
- Kind sk = NodeManager::operatorToKind( n );
- Trace("sygus-split") << ", kind = " << sk;
- d_kinds[tn][sk] = i;
- d_arg_kind[tn][i] = sk;
- }else if( sop.isConst() ){
- Trace("sygus-split") << ", constant";
- d_consts[tn][n] = i;
- d_arg_const[tn][i] = n;
- }
- d_ops[tn][n] = i;
- Trace("sygus-split") << std::endl;
- }
+ d_util->registerSygusType( tn );
//compute the redundant operators
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
bool nred = true;
if( options::sygusNormalForm() ){
Trace("sygus-split-debug") << "Is " << dt[i].getName() << " a redundant operator?" << std::endl;
- std::map< int, Kind >::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
}
}
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;
//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; i<dt.getNumConstructors(); i++ ){
Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
bool addSplit = d_sygus_nred[tnn][i];
if( addSplit && hasParentKind ){
- if( d_arg_kind.find( tnn )!=d_arg_kind.end() && d_arg_kind[tnn].find( i )!=d_arg_kind[tnn].end() ){
- addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_arg_kind[tnn][i], parentKind, sIndex );
+ if( d_util->d_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;
}
}
}
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<dto.getNumConstructors(); i++ ){
- if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
- //arguments that can be removed
- std::map< int, bool > 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; j<dt.getNumConstructors(); j++ ){
- if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
- Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl;
- bool rem = false;
- if( isPComm && j>i && 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<dto.getNumConstructors(); i++ ){
+ if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
+ //arguments that can be removed
+ std::map< int, bool > 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; j<dt.getNumConstructors(); j++ ){
+ if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
+ Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl;
+ bool rem = false;
+ if( isPComm && j>i && 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<dt.getNumConstructors(); j++ ){
- if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
- d_sygus_pc_arg_pos[tnno][csIndex][i].push_back( j );
- Trace("sygus-split-debug") << " " << dt[j].getName() << std::endl;
- }
+ if( rem ){
+ rem_arg[j] = true;
+ }else{
+ argConsider = true;
+ larg_consider[j] = true;
}
- //if there are no possibilities for first argument, then this child is redundant
- if( d_sygus_pc_arg_pos[tnno][csIndex][i].empty() ){
- Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dto[i].getName();
- Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
- d_sygus_pc_nred[tnno][csIndex][osIndex][i] = false;
+ }
+ }
+ 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<dt.getNumConstructors(); j++ ){
+ if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
+ d_sygus_pc_arg_pos[tnno][csIndex][i].push_back( j );
+ Trace("sygus-split-debug") << " " << dt[j].getName() << std::endl;
}
}
+ //if there are no possibilities for first argument, then this child is redundant
+ if( d_sygus_pc_arg_pos[tnno][csIndex][i].empty() ){
+ Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dto[i].getName();
+ Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
+ d_sygus_pc_nred[tnno][csIndex][osIndex][i] = false;
+ }
}
}
}
}
}
-bool SygusSplit::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 SygusSplit::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 SygusSplit::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 SygusSplit::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 SygusSplit::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 SygusSplit::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<BitVectorSize>(), uv);
- n = NodeManager::currentNM()->mkConst<BitVector>(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<BitVectorSize>());
- }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 );
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
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 );
//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;
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;
}
}
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;
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{
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
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();
if( curr_depth<depth ){
for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
Node sel = NodeManager::currentNM()->mkNode( 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();
}
}
}
-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<testers.size(); i++ ){
+ // Trace("sygus-nf-gen-debug") << "* " << testers[i] << std::endl;
+ //}
+ Trace("sygus-nf-gen-debug2") << "Tester tree is : " << std::endl;
+ for( std::map< Node, std::vector< Node > >::iterator it = testers_u.begin(); it != testers_u.end(); ++it ){
+ Trace("sygus-nf-gen-debug2") << " " << it->first << " -> " << std::endl;
+ for( unsigned i=0; i<it->second.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; i<testers_u[a].size(); i++ ){
+ TypeNode tn = testers_u[a][i][0].getType();
+ norm_children[i] = d_util->getNormalized( 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<testers_u[a].size(); i++ ){
+ if( rlv[i] ){
+ collectTesters( testers_u[a][i], testers_u, rlv_testers );
+ }else{
+ Trace("sygus-nf") << " - argument " << i << " is not relevant." << std::endl;
+ }
+ }
+ Trace("sygus-nf-gen-debug") << "Relevant testers : " << std::endl;
+ conflict_gen_set = true;
+ for( unsigned i=0; i<testers.size(); i++ ){
+ bool rl = std::find( rlv_testers.begin(), rlv_testers.end(), testers[i] )!=rlv_testers.end();
+ Trace("sygus-nf-gen-debug") << "* " << testers[i] << " -> " << rl << std::endl;
+ d_conflict_gen[at][prog].push_back( rl );
+ }
+ }
+ }
+ }
+ if( !conflict_gen_set ){
+ for( unsigned i=0; i<testers.size(); i++ ){
+ d_conflict_gen[at][prog].push_back( true );
+ }
+ }
+ }
+ }else{
+ red = it->second;
}
- 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; i<testers.size(); i++ ){
+ if( d_conflict_gen[at][prog][i] ){
+ gtesters.push_back( testers[i] );
+ }
+ }
+ d_util->d_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; i<it->second.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 );
}
}
+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() );
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;
+ */
}
}
}
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<BitVectorSize>(), uv);
+ n = NodeManager::currentNM()->mkConst<BitVector>(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<BitVectorSize>());
+ }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<dt.getNumConstructors(); i++ ){
+ Expr sop = dt[i].getSygusOp();
+ Assert( !sop.isNull() );
+ Node n = Node::fromExpr( sop );
+ Trace("sygus-util") << " Operator #" << i << " : " << sop;
+ if( sop.getKind() == kind::BUILTIN ){
+ Kind sk = NodeManager::operatorToKind( n );
+ Trace("sygus-util") << ", kind = " << sk;
+ d_kinds[tn][sk] = i;
+ d_arg_kind[tn][i] = sk;
+ }else if( sop.isConst() ){
+ Trace("sygus-util") << ", constant";
+ d_consts[tn][n] = i;
+ d_arg_const[tn][i] = n;
+ }
+ d_ops[tn][n] = i;
+ Trace("sygus-util") << std::endl;
+ }
+ }
+ }
+ }
+}
+
+bool SygusUtil::isRegistered( TypeNode tn ) {
+ return d_register.find( tn )!=d_register.end();
+}
+
+int SygusUtil::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 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;
+ }
+}
+
+
+
+
+
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;
/** 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 */
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();
}
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 */
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; }
projects / cvc5.git / commitdiff