}
}
+Node SygusSplit::getVar( TypeNode tn, int i ) {
+ while( i>=(int)d_fv[tn].size() ){
+ std::stringstream ss;
+ TypeNode vtn = tn;
+ if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ ss << "fv_" << dt.getName() << "_" << i;
+ Assert( d_register.find( tn )!=d_register.end() );
+ if( !d_register[tn].isNull() ){
+ vtn = d_register[tn];
+ }
+ }else{
+ ss << "fv_" << tn << "_" << i;
+ }
+ Assert( !vtn.isNull() );
+ Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" );
+ d_fv_stype[v] = tn;
+ d_fv[tn].push_back( v );
+ }
+ return d_fv[tn][i];
+}
+
+Node SygusSplit::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) {
+ std::map< TypeNode, int >::iterator it = var_count.find( tn );
+ if( it==var_count.end() ){
+ var_count[tn] = 1;
+ return getVar( tn, 0 );
+ }else{
+ int index = it->second;
+ var_count[tn]++;
+ return getVar( tn, index );
+ }
+}
+
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() ){
Trace("sygus-split") << "Get sygus splits " << n << std::endl;
//get the kinds for child datatype
TypeNode tnn = n.getType();
- registerSygusType( tnn, dt );
+ registerSygusType( tnn );
//get parent information, if possible
int csIndex = -1;
int sIndex = -1;
Node arg1;
- Kind parentKind = UNDEFINED_KIND;
+ TypeNode tn1;
TypeNode tnnp;
Node ptest;
if( n.getKind()==APPLY_SELECTOR_TOTAL ){
Assert( pdt.isSygus() );
csIndex = Datatype::cindexOf(selectorExpr);
sIndex = Datatype::indexOf(selectorExpr);
- tnnp = n[0].getType();
+ TypeNode 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 );
-
- //relationships between arguments
- if( isKindArg( tnnp, csIndex ) ){
- if( sIndex==1 ){
- //if commutative, normalize based on term ordering (the constructor index of left arg must be less than or equal to the right arg)
- Trace("sygus-split-debug") << "Commutative operator : " << parentKind << std::endl;
- if( pdt[csIndex].getNumArgs()==2 && isArgDatatype( pdt[csIndex], 0, dt ) ){
- registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, 0 );
- arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
- }
+ if( 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 ) ){
+ arg1 = Node::null();
}
}
-
// we are splitting on a term that may later have no semantics : guard this case
ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt );
Trace("sygus-split-debug") << "Parent guard : " << ptest << std::endl;
}
+
std::vector< Node > ptest_c;
bool narrow = false;
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << i << " : ";
+ Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << dt[i].getName() << " : ";
Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
bool addSplit = d_sygus_nred[tnn][i];
if( addSplit ){
addSplit = d_sygus_pc_nred[tnn][csIndex][sIndex][i];
}
if( addSplit ){
+ //check based on generic rewriting TODO
+ //std::vector< int > csIndices;
+ //std::vector< int > sIndices;
+ //csIndices.push_back( i );
+ //TypeNode tng;
+ //Node g = getGeneric( n, csIndices, sIndices, tng );
+ //Trace("sygus-split-debug") << "Generic template " << n << " " << dt[i].getName() << " is " << g << ", sygus type : " << tng << std::endl;
+ //if( isGenericRedundant( tng, g ) ){
+ // addSplit = false;
+ // Trace("sygus-split-debug2") << "generic redundant" << std::endl;
+ //}
+
+ std::vector< Node > test_c;
Node test = DatatypesRewriter::mkTester( n, i, dt );
-
+ test_c.push_back( test );
//check if we can strengthen the first argument
if( !arg1.isNull() ){
+ const Datatype& dt1 = ((DatatypeType)(tn1).toType()).getDatatype();
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], dt ) );
+ lem_c.push_back( DatatypesRewriter::mkTester( arg1, it->second[j], dt1 ) );
}
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 = NodeManager::currentNM()->mkNode( AND, test, argStr );
+ test_c.push_back( argStr );
narrow = true;
}
}
Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n );
Node szr = NodeManager::currentNM()->mkNode( DT_SIZE, DatatypesRewriter::getInstCons( n, dt, i ) );
szr = Rewriter::rewrite( szr );
- test = NodeManager::currentNM()->mkNode( AND, test, szl.eqNode( szr ) );
+ test_c.push_back( szl.eqNode( szr ) );
}
+ test = test_c.size()==1 ? test_c[0] : NodeManager::currentNM()->mkNode( AND, test_c );
d_splits[n].push_back( test );
Trace("sygus-split-debug2") << "SUCCESS" << std::endl;
- Trace("sygus-split") << "Disjunct #" << d_splits[n].size() << " : " << test << std::endl;
+ Trace("sygus-split-debug") << "Disjunct #" << d_splits[n].size() << " : " << test << std::endl;
}else{
Trace("sygus-split-debug2") << "redundant argument" << std::endl;
narrow = true;
ptest_c.push_back( DatatypesRewriter::mkTester( n, i, dt ) );
}
}
- if( d_splits[n].empty() ){
- //possible
- exit( 3 );
-
- Assert( false );
- }
if( narrow && !ptest.isNull() ){
- Node split = d_splits[n].size()==1 ? d_splits[n][0] : NodeManager::currentNM()->mkNode( OR, d_splits[n] );
- d_splits[n].clear();
- split = NodeManager::currentNM()->mkNode( AND, ptest, split );
+ Node split = d_splits[n].empty() ? NodeManager::currentNM()->mkConst( false ) :
+ ( d_splits[n].size()==1 ? d_splits[n][0] : NodeManager::currentNM()->mkNode( OR, d_splits[n] ) );
+ if( !d_splits[n].empty() ){
+ d_splits[n].clear();
+ split = NodeManager::currentNM()->mkNode( AND, ptest, split );
+ }
d_splits[n].push_back( split );
if( !ptest_c.empty() ){
ptest = NodeManager::currentNM()->mkNode( AND, ptest.negate(), NodeManager::currentNM()->mkNode( OR, ptest_c ) );
}
d_splits[n].push_back( ptest );
+ }else{
+ Assert( !d_splits[n].empty() );
}
}
splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
}
-void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) {
+void SygusSplit::registerSygusType( TypeNode tn ) {
if( d_register.find( tn )==d_register.end() ){
- Trace("sygus-split") << "Register sygus type " << dt.getName() << "..." << std::endl;
- d_register[tn] = true;
- 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;
- }
+ if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+ d_register[tn] = TypeNode::null();
+ }else{
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Trace("sygus-split") << "Register type " << dt.getName() << "..." << std::endl;
+ d_register[tn] = TypeNode::fromType( dt.getSygusType() );
+ 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;
+ }
- //compute the redundant operators
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- bool nred = true;
- if( options::sygusNormalForm() ){
- std::map< int, Kind >::iterator it = d_arg_kind[tn].find( i );
- if( it!=d_arg_kind[tn].end() ){
- Kind dk;
- if( isAntisymmetric( it->second, dk ) ){
- std::map< Kind, int >::iterator ita = d_kinds[tn].find( dk );
- if( ita!=d_kinds[tn].end() ){
- Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
- //check for type mismatches
- bool success = true;
- unsigned j = ita->second;
- for( unsigned k=0; k<2; k++ ){
- unsigned ko = k==0 ? 1 : 0;
- TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
- TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
- if( tni!=tnj ){
- Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
- success = false;
- break;
+ //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() ){
+ Kind dk;
+ if( isAntisymmetric( it->second, dk ) ){
+ int j = getKindArg( tn, dk );
+ if( j!=-1 ){
+ Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
+ //check for type mismatches
+ bool success = true;
+ for( unsigned k=0; k<2; k++ ){
+ unsigned ko = k==0 ? 1 : 0;
+ TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
+ TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
+ if( tni!=tnj ){
+ Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
+ success = false;
+ break;
+ }
+ }
+ if( success ){
+ Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl;
+ nred = false;
+ }
}
}
- if( success ){
- Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << 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;
+ std::map< TypeNode, int > var_count;
+ std::map< int, Node > pre;
+ Node g = mkGeneric( dt, i, var_count, pre );
+ nred = !isGenericRedundant( tn, g );
+ Trace("sygus-split-debug") << "...done check " << dt[i].getName() << " based on generic rewriting" << std::endl;
}
}
- //NAND,NOR
+ d_sygus_nred[tn].push_back( nred );
}
}
- d_sygus_nred[tn].push_back( nred );
+ Trace("sygus-split-debug") << "...done register type " << dt.getName() << std::endl;
}
}
}
void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& dt, TypeNode tnnp, const Datatype& pdt, int csIndex, int sIndex ) {
std::map< int, std::vector< bool > >::iterator it = d_sygus_pc_nred[tnn][csIndex].find( sIndex );
if( it==d_sygus_pc_nred[tnn][csIndex].end() ){
- registerSygusType( tnnp, pdt );
+ d_sygus_pc_nred[tnn][csIndex][sIndex].clear();
+ registerSygusType( tnn );
+ registerSygusType( tnnp );
Trace("sygus-split") << "Register type constructor arg " << dt.getName() << " " << csIndex << " " << sIndex << std::endl;
if( !options::sygusNormalForm() ){
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
parentKind = 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() ){
Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
}
}
+ if( addSplit ){
+ if( pdt[csIndex].getNumArgs()==1 ){
+ //generic rewriting
+ std::map< int, Node > prec;
+ std::map< TypeNode, int > var_count;
+ Node gc = mkGeneric( dt, i, var_count, prec );
+ std::map< int, Node > pre;
+ pre[sIndex] = gc;
+ Node g = mkGeneric( pdt, csIndex, var_count, pre );
+ addSplit = !isGenericRedundant( tnnp, g );
+ }
+ }
}
d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
}
- //also compute argument relationships
if( options::sygusNormalFormArg() ){
+ //compute argument relationships for 2-arg constructors
if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
int osIndex = sIndex==0 ? 1 : 0;
- if( isArgDatatype( pdt[csIndex], osIndex, dt ) ){
- registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, osIndex );
+ 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[tnn][csIndex].find( osIndex )!=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 );
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( d_sygus_pc_nred[tnn][csIndex][osIndex][i] ){
+ 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;
- if( isComm( parentKind ) ){
- for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
- if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
- if( isPComm && j>i ){
- //based on commutativity
- // use term ordering : constructor index of first argument is not greater than constructor index of second argument
- rem_arg[j] = true;
- }else{
- if( parentKind!=UNDEFINED_KIND && dt[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){
- Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dt[i].getSygusOp() );
- Node nrr = Rewriter::rewrite( nr );
- Trace("sygus-split-debug") << " Test constant args : " << nr << " rewrites to " << nrr << std::endl;
- //based on rewriting
- // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy
- if( hasOp( tnnp, nrr ) ){
- Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl;
- rem_arg[j] = true;
- }
+ //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 = mkGeneric( dt, j, var_count, pre );
+ Node g2 = mkGeneric( dto, i, var_count, pre );
+ Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 );
+ if( isGenericRedundant( tnnp, g ) ){
+ rem = true;
+ }
+ /*
+ Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dto[i].getSygusOp() );
+ Node nrr = Rewriter::rewrite( nr );
+ Trace("sygus-split-debug") << " Test constant args : " << nr << " rewrites to " << nrr << std::endl;
+ //based on rewriting
+ // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy
+ if( hasOp( tnnp, nrr ) ){
+ Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl;
+ rem = true;
}
+ */
}
}
+ if( rem ){
+ rem_arg[j] = true;
+ }else{
+ argConsider = true;
+ larg_consider[j] = true;
+ }
}
}
if( !rem_arg.empty() ){
- d_sygus_pc_arg_pos[tnn][csIndex][i].clear();
- Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dt[i].getName() << " : " << std::endl;
+ 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[tnn][csIndex][i].push_back( j );
+ 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[tnn][csIndex][i].empty() ){
- Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dt[i].getName();
+ 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[tnn][csIndex][osIndex][i] = false;
+ d_sygus_pc_nred[tnno][csIndex][osIndex][i] = false;
}
}
}
bool SygusSplit::isIdempotentArg( Node n, Kind ik, int arg ) {
TypeNode tn = n.getType();
if( n==getTypeValue( tn, 0 ) ){
- if( ik==PLUS || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==OR ){
+ if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){
return true;
- }else if( ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR ){
+ }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){
return arg==1;
}
}else if( n==getTypeValue( tn, 1 ) ){
return arg==1;
}
}else if( n==getTypeMaxValue( tn ) ){
- if( ik==BITVECTOR_AND ){
+ if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
return true;
}
}
bool SygusSplit::isSingularArg( Node n, Kind ik, int arg ) {
TypeNode tn = n.getType();
if( n==getTypeValue( tn, 0 ) ){
- if( ik==MULT || ik==BITVECTOR_MULT || ik==BITVECTOR_AND || ik==AND ){
+ 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==BITVECTOR_OR ){
+ if( ik==OR || ik==BITVECTOR_OR ){
return true;
}
}
BitVector bval(tn.getConst<BitVectorSize>(), uv);
n = NodeManager::currentNM()->mkConst<BitVector>(bval);
}else if( tn.isBoolean() ){
- if( val==0 || val==1 ){
- n = NodeManager::currentNM()->mkConst( val==1 );
+ if( val==0 ){
+ n = NodeManager::currentNM()->mkConst( false );
}
}
d_type_value[tn][val] = n;
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;
return false;
}
Kind nk = UNDEFINED_KIND;
- Kind reqk = 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 = BITVECTOR_XNOR;
}
}
+ if( parent==UMINUS ){
+ if( k==PLUS ){
+ nk = PLUS;reqk = UMINUS;
+ }else if( k==MINUS ){
+ }
+ }
+ if( parent==BITVECTOR_NEG ){
+ if( k==PLUS ){
+ nk = PLUS;reqk = BITVECTOR_NEG;
+ }
+ }
if( nk!=UNDEFINED_KIND ){
Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk;
if( reqk!=UNDEFINED_KIND ){
return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
}
+Node SygusSplit::getGeneric( Node n, std::vector< int >& csIndices, std::vector< int >& sIndices, TypeNode& tng ) {
+ if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+ Node op = n.getOperator();
+ Expr selectorExpr = op.toExpr();
+ csIndices.push_back( Datatype::cindexOf(selectorExpr) );
+ sIndices.push_back( Datatype::indexOf(selectorExpr) );
+ return getGeneric( n[0], csIndices, sIndices, tng );
+ }else{
+ tng = n.getType();
+ Assert( DatatypesRewriter::isTypeDatatype( tng ) );
+ const Datatype& dt = ((DatatypeType)(tng).toType()).getDatatype();
+ Assert( csIndices.size()==sIndices.size()+1 );
+ std::reverse( csIndices.begin(), csIndices.end() );
+ std::reverse( sIndices.begin(), sIndices.end() );
+ Trace("sygus-generic") << "Traversed under " << sIndices.size() << " selectors." << std::endl;
+ std::map< TypeNode, int > var_count;
+ return getGeneric2( dt, var_count, csIndices, sIndices, 0 );
+ }
+}
+
+Node SygusSplit::getGeneric2( const Datatype& dt, std::map< TypeNode, int >& var_count, std::vector< int >& csIndices, std::vector< int >& sIndices, unsigned index ) {
+ Assert( index<csIndices.size() );
+ std::vector< Node > children;
+ int c = csIndices[index];
+ int s = index<sIndices.size() ? sIndices[index] : -1;
+ Assert( c>=0 && c<(int)dt.getNumConstructors() );
+ Assert( dt.isSygus() );
+ Assert( !dt[c].getSygusOp().isNull() );
+ Node op = Node::fromExpr( dt[c].getSygusOp() );
+ if( op.getKind()!=BUILTIN ){
+ children.push_back( op );
+ }
+ Trace("sygus-generic") << "Construct for " << dt[c].getName() << ", arg " << s << ", op " << op << std::endl;
+ std::map< int, Node > pre;
+ if( s!=-1 ){
+ TypeNode tna = getArgType( dt[c], s );
+ Assert( DatatypesRewriter::isTypeDatatype( tna ) );
+ const Datatype& adt = ((DatatypeType)(tna).toType()).getDatatype();
+ pre[s] = getGeneric2( adt, var_count, csIndices, sIndices, index+1 );
+ }
+ return mkGeneric( dt, c, var_count, pre );
+}
+
+Node SygusSplit::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() );
+ Assert( !dt[c].getSygusOp().isNull() );
+ std::vector< Node > children;
+ Node op = Node::fromExpr( dt[c].getSygusOp() );
+ if( op.getKind()!=BUILTIN ){
+ children.push_back( op );
+ }
+ for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
+ TypeNode tna = getArgType( dt[c], i );
+ registerSygusType( tna );
+ Assert( d_register.find( tna )!=d_register.end() );
+ Node a;
+ std::map< int, Node >::iterator it = pre.find( i );
+ if( it!=pre.end() ){
+ a = it->second;
+ }else{
+ a = getVarInc( tna, var_count );
+ }
+ Assert( !a.isNull() );
+ Assert( a.getType()==d_register[tna] );
+ children.push_back( a );
+ }
+ if( Trace.isOn("sygus-split-debug3") ){
+ Trace("sygus-split-debug3") << "mkGeneric " << dt[c].getName() << ", op = " << op << " with arguments : " << std::endl;
+ for( unsigned i=0; i<children.size(); i++ ){
+ Trace("sygus-split-debug3") << " " << children[i] << std::endl;
+ }
+ }
+ if( op.getKind()==BUILTIN ){
+ return NodeManager::currentNM()->mkNode( op, children );
+ }else{
+ if( children.size()==1 ){
+ return children[0];
+ }else{
+ return NodeManager::currentNM()->mkNode( APPLY, children );
+ }
+ }
+}
+
+bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
+ //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 = Rewriter::rewrite( g );
+ //replace variables in order left to right
+ std::map< TypeNode, int > var_count;
+ std::map< Node, Node > subs;
+ gr = getSygusNormalized( gr, var_count, subs );
+ 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;
+ }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{
+ return it->second;
+ }
+}
+
+Node SygusSplit::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
+ return n;
+ if( n.getKind()==SKOLEM ){
+ std::map< Node, Node >::iterator its = subs.find( n );
+ if( its!=subs.end() ){
+ return its->second;
+ }else{
+ std::map< Node, TypeNode >::iterator it = d_fv_stype.find( n );
+ if( it!=d_fv_stype.end() ){
+ Node v = getVarInc( it->second, var_count );
+ subs[n] = v;
+ return v;
+ }else{
+ return n;
+ }
+ }
+ }else{
+ if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = getSygusNormalized( n[i], var_count, subs );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ return n;
+ }
+}
projects / cvc5.git / commitdiff