From f3045ccce9d30114f6e90cfa72de176da344cb1f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 26 Jan 2015 10:41:51 +0100 Subject: [PATCH] Generalize sygus search space narrowing to arbitrary theory rewriting. --- src/theory/datatypes/datatypes_sygus.cpp | 505 +++++++++++++++++------ src/theory/datatypes/datatypes_sygus.h | 34 +- 2 files changed, 417 insertions(+), 122 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index ee8169db7..9bfccc34e 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -96,19 +96,53 @@ bool SygusSplit::isConstArg( TypeNode tn, int i ) { } } +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 ){ @@ -118,31 +152,26 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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 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; jsecond.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; } } @@ -173,11 +216,12 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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; @@ -190,21 +234,20 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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() ); } } @@ -212,63 +255,83 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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::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::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; } } } @@ -276,7 +339,9 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) { 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 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 larg_consider; + for( unsigned i=0; i rem_arg; - if( isComm( parentKind ) ){ - for( unsigned j=0; ji ){ - //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; 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 = 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(), uv); n = NodeManager::currentNM()->mkConst(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; @@ -478,6 +589,8 @@ Node SygusSplit::getTypeMaxValue( TypeNode tn ) { 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; @@ -508,7 +621,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt 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 ) { @@ -532,6 +645,17 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt 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 ){ @@ -655,3 +779,150 @@ TypeNode SygusSplit::getArgType( const DatatypeConstructor& c, int i ) { 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 children; + int c = csIndices[index]; + int s = index=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; imkNode( 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; imkNode( n.getKind(), children ); + } + } + return n; + } +} diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 13be75e71..76ccabd4d 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -26,7 +26,16 @@ namespace CVC4 { namespace theory { namespace datatypes { - + +//class SygusVarTrie +//{ +//public: +// // datatype, constructor, argument +// std::map< Node, std::map< int, SygusVarTrie > > d_children; +// std::map< TypeNode, Node > d_var; +//}; + + class SygusSplit { private: @@ -38,12 +47,18 @@ private: 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, bool > d_register; + 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; + // + std::map< TypeNode, std::vector< Node > > d_fv; + std::map< Node, TypeNode > d_fv_stype; + // 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; private: bool isRegistered( TypeNode tn ); int getKindArg( TypeNode tn, Kind k ); @@ -54,9 +69,12 @@ private: bool hasOp( TypeNode tn, Node n ); bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); +private: + Node getVar( TypeNode tn, int i ); + Node getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); private: /** register sygus type */ - void registerSygusType( TypeNode tn, const Datatype& dt ); + void registerSygusType( TypeNode tn ); /** register sygus operator */ void registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& dt, TypeNode tnnp, const Datatype& pdt, int csIndex, int sIndex ); /** consider sygus split */ @@ -82,12 +100,18 @@ private: bool isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); +private: + Node getGeneric( Node n, std::vector< int >& csIndices, std::vector< int >& sIndices, TypeNode& tng ); + Node getGeneric2( const Datatype& dt, std::map< TypeNode, int >& var_count, std::vector< int >& csIndices, std::vector< int >& sIndices, unsigned index ); + Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); + bool isGenericRedundant( TypeNode tn, Node g ); + Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); public: /** get sygus splits */ void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ); }; - - + + } } } -- 2.30.2