From fd2ca646503ffb09caf6a4d1cb4d57c34defdc22 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 29 Jan 2015 17:09:21 +0100 Subject: [PATCH] Apply sygus search space narrowing for all subprograms of current global state. --- src/theory/datatypes/datatypes_sygus.cpp | 128 ++++++++++++++++------- src/theory/datatypes/datatypes_sygus.h | 8 +- 2 files changed, 96 insertions(+), 40 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 62621f389..4e7aaad53 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -787,7 +787,7 @@ void SygusSymBreak::ProgSearch::addTester( Node tst ) { } } -void SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) { +bool SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) { Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tst << ", depth = " << depth << " of " << d_anchor << std::endl; int tindex = Datatype::indexOf( tst.getOperator().toExpr() ); TypeNode tn = tst[0].getType(); @@ -817,52 +817,98 @@ void SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) { Assert( d_watched_count[depth]>0 ); d_watched_count[depth] = d_watched_count[depth] - 1; } - processProgramDepth( depth ); - //assign preexisting testers - for( unsigned i=0; i& var_count, std::vector< Node >& testers ) { - 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 ); - Assert( it!=d_testers.end() ); - Node tst = (*it).second; - testers.push_back( tst ); - Assert( tst[0]==prog ); - int tindex = Datatype::indexOf( tst.getOperator().toExpr() ); - TypeNode tn = prog.getType(); - Assert( DatatypesRewriter::isTypeDatatype( tn ) ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - std::map< int, Node > pre; - if( curr_depthmkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog ); - pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers ); + //determine if any subprograms on the current path are redundant + if( processSubprograms( tst[0], depth, depth ) ){ + if( processProgramDepth( depth ) ){ + //assign preexisting testers + for( unsigned i=0; id_util->mkGeneric( dt, tindex, var_count, pre ); + return false; } -void SygusSymBreak::ProgSearch::processProgramDepth( int depth ){ +bool SygusSymBreak::ProgSearch::processProgramDepth( int depth ){ if( depth==d_prog_depth.get() && ( depth==0 || ( d_watched_count.find( depth )!=d_watched_count.end() && d_watched_count[depth]==0 ) ) ){ d_prog_depth = d_prog_depth + 1; if( depth>0 ){ - Trace("sygus-sym-break-debug") << "Program is set for depth=" << depth << std::endl; + Trace("sygus-sym-break-debug") << "Program is set for depth " << depth << std::endl; std::map< TypeNode, int > var_count; std::vector< Node > testers; //now have entire information about candidate program at given depth Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers ); - d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers ); + if( !prog.isNull() ){ + if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers ) ){ + return false; + } + }else{ + Assert( false ); + } } - processProgramDepth( depth+1 ); + return processProgramDepth( depth+1 ); + }else{ + return true; } } -void SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ) { - if( d_normalized[at].find( prog )==d_normalized[at].end() ){ +bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odepth ) { + Trace("sygus-sym-break-debug") << "Processing subprograms on path " << n << ", which has depth " << depth << std::endl; + depth--; + if( depth>0 ){ + Assert( n.getKind()==APPLY_SELECTOR_TOTAL ); + std::map< TypeNode, int > var_count; + std::vector< Node > testers; + //now have entire information about candidate program at given depth + Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, var_count, testers ); + if( !prog.isNull() ){ + if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers ) ){ + return false; + } + //also try higher levels + return processSubprograms( n[0], depth, odepth ); + }else{ + Trace("sygus-sym-break-debug") << "...program incomplete." << std::endl; + } + } + return true; +} + +Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) { + 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 ); + Assert( tst[0]==prog ); + int tindex = Datatype::indexOf( tst.getOperator().toExpr() ); + TypeNode tn = prog.getType(); + Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + std::map< int, Node > pre; + if( curr_depthmkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog ); + pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers ); + if( pre[i].isNull() ){ + return Node::null(); + } + } + } + return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre ); + }else{ + Trace("sygus-sym-break-debug") << "...failure." << std::endl; + 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() ){ 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; @@ -873,16 +919,24 @@ void SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node 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; }else{ + d_redundant[at][prog] = true; Assert( !testers.empty() ); Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl; - d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers ); - Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl; - d_util->d_conflict = true; - - // TODO : generalize conflict } } + 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 ); + 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; + } } SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index fd0065667..cf43b0a31 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -120,8 +120,9 @@ private: private: SygusSymBreak * d_parent; Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ); - void processProgramDepth( int depth ); - void assignTester( Node tst, int depth ); + 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 ) : d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) { @@ -138,8 +139,9 @@ private: 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; Node getAnchor( Node n ); - void 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 ); public: SygusSymBreak( SygusUtil * util, context::Context* c ); /** add tester */ -- 2.30.2