From: Andrew Reynolds Date: Tue, 27 Mar 2018 02:02:32 +0000 (-0500) Subject: Documentation and simplifications for PBE (#1677) X-Git-Tag: cvc5-1.0.0~5203 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab70f7a01939515792221b33372ec994bd425fde;p=cvc5.git Documentation and simplifications for PBE (#1677) --- diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 1c61544e1..528f47624 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -1252,11 +1252,12 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& itv->second.setSolved( v ); // it subsumes everything itv->second.d_term_trie.clear(); - itv->second.d_term_trie.addTerm( this, v, results, true, subsume ); + itv->second.d_term_trie.addTerm(v, results, true, subsume); } keep = true; }else{ - Node val = itv->second.d_term_trie.addTerm( this, v, results, true, subsume ); + Node val = + itv->second.d_term_trie.addTerm(v, results, true, subsume); if( val==v ){ Trace("sygus-pbe-enum") << " ...success"; if( !subsume.empty() ){ @@ -1275,7 +1276,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& } }else{ // must be unique up to examples - Node val = itv->second.d_term_trie.addCond(this, v, results, true); + Node val = itv->second.d_term_trie.addCond(v, results, true); if (val == v) { Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " @@ -1473,238 +1474,264 @@ bool CegConjecturePbe::CandidateInfo::isNonTrivial() { } // status : 0 : exact, -1 : vals is subset, 1 : vals is superset -Node CegConjecturePbe::SubsumeTrie::addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, - std::vector< Node >& subsumed, bool spol, IndexFilter * f, - unsigned index, int status, bool checkExistsOnly, bool checkSubsume ) { - if( index==vals.size() ){ - if( status==0 ){ +Node CegConjecturePbe::SubsumeTrie::addTermInternal( + Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed, + bool spol, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume) +{ + if (index == vals.size()) + { + if (status == 0) + { // set the term if checkExistsOnly = false - if( d_term.isNull() && !checkExistsOnly ){ + if (d_term.isNull() && !checkExistsOnly) + { d_term = t; } - }else if( status==1 ){ - Assert( checkSubsume ); + } + else if (status == 1) + { + Assert(checkSubsume); // found a subsumed term - if( !d_term.isNull() ){ - subsumed.push_back( d_term ); - if( !checkExistsOnly ){ + if (!d_term.isNull()) + { + subsumed.push_back(d_term); + if (!checkExistsOnly) + { // remove it if checkExistsOnly = false d_term = Node::null(); } } - }else{ - Assert( !checkExistsOnly && checkSubsume ); + } + else + { + Assert(!checkExistsOnly && checkSubsume); } return d_term; - }else{ - // the current value - Assert( pol || ( vals[index].isConst() && vals[index].getType().isBoolean() ) ); - Node cv = pol ? vals[index] : ( vals[index]==pbe->d_true ? pbe->d_false : pbe->d_true ); - // if checkExistsOnly = false, check if the current value is subsumed if checkSubsume = true, if so, don't add - if( !checkExistsOnly && checkSubsume ){ - std::vector< bool > check_subsumed_by; - if( status==0 ){ - if( cv==pbe->d_false ){ - check_subsumed_by.push_back( spol ); - } - }else if( status==-1 ){ - check_subsumed_by.push_back( spol ); - if( cv==pbe->d_false ){ - check_subsumed_by.push_back( !spol ); - } + } + NodeManager* nm = NodeManager::currentNM(); + // the current value + Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean())); + Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst()); + // if checkExistsOnly = false, check if the current value is subsumed if + // checkSubsume = true, if so, don't add + if (!checkExistsOnly && checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + std::vector check_subsumed_by; + if (status == 0) + { + if (!cv.getConst()) + { + check_subsumed_by.push_back(spol); } - // check for subsumed nodes - for( unsigned i=0; id_true : pbe->d_false; - // check if subsumed - std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval ); - if( itc!=d_children.end() ){ - unsigned next_index = f ? f->next( index ) : index+1; - Node ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, -1, checkExistsOnly, checkSubsume ); - // ret subsumes t - if( !ret.isNull() ){ - return ret; - } - } + } + else if (status == -1) + { + check_subsumed_by.push_back(spol); + if (!cv.getConst()) + { + check_subsumed_by.push_back(!spol); } } - Node ret; - std::vector< bool > check_subsume; - if( status==0 ){ - unsigned next_index = f ? f->next( index ) : index+1; - if( checkExistsOnly ){ - std::map< Node, SubsumeTrie >::iterator itc = d_children.find( cv ); - if( itc!=d_children.end() ){ - ret = itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume ); - } - }else{ - Assert( spol ); - ret = d_children[cv].addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 0, checkExistsOnly, checkSubsume ); - if( ret!=t ){ - // we were subsumed by ret, return + // check for subsumed nodes + for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++) + { + bool csbi = check_subsumed_by[i]; + Node csval = nm->mkConst(csbi); + // check if subsumed + std::map::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + Node ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + -1, + checkExistsOnly, + checkSubsume); + // ret subsumes t + if (!ret.isNull()) + { return ret; } } - if( checkSubsume ){ - // check for subsuming - if( cv==pbe->d_true ){ - check_subsume.push_back( !spol ); - } + } + } + Node ret; + std::vector check_subsume; + if (status == 0) + { + if (checkExistsOnly) + { + std::map::iterator itc = d_children.find(cv); + if (itc != d_children.end()) + { + ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); } - }else if( status==1 ){ - Assert( checkSubsume ); - check_subsume.push_back( !spol ); - if( cv==pbe->d_true ){ - check_subsume.push_back( spol ); + } + else + { + Assert(spol); + ret = d_children[cv].addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); + if (ret != t) + { + // we were subsumed by ret, return + return ret; } } - if( checkSubsume ){ - // check for subsumed terms - for( unsigned i=0; id_true : pbe->d_false; - std::map< Node, SubsumeTrie >::iterator itc = d_children.find( csval ); - if( itc!=d_children.end() ){ - unsigned next_index = f ? f->next( index ) : index+1; - itc->second.addTermInternal( pbe, t, vals, pol, subsumed, spol, f, next_index, 1, checkExistsOnly, checkSubsume ); - // clean up - if( itc->second.isEmpty() ){ - Assert( !checkExistsOnly ); - d_children.erase( csval ); - } + if (checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + // check for subsuming + if (cv.getConst()) + { + check_subsume.push_back(!spol); + } + } + } + else if (status == 1) + { + Assert(checkSubsume); + Assert(cv.isConst() && cv.getType().isBoolean()); + check_subsume.push_back(!spol); + if (cv.getConst()) + { + check_subsume.push_back(spol); + } + } + if (checkSubsume) + { + // check for subsumed terms + for (unsigned i = 0, size = check_subsume.size(); i < size; i++) + { + Node csval = nm->mkConst(check_subsume[i]); + std::map::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 1, + checkExistsOnly, + checkSubsume); + // clean up + if (itc->second.isEmpty()) + { + Assert(!checkExistsOnly); + d_children.erase(csval); } } } - return ret; } + return ret; } -Node CegConjecturePbe::SubsumeTrie::addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ) { - unsigned start_index = f ? f->start() : 0; - return addTermInternal( pbe, t, vals, pol, subsumed, true, f, start_index, 0, false, true ); +Node CegConjecturePbe::SubsumeTrie::addTerm(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed) +{ + return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true); } -Node CegConjecturePbe::SubsumeTrie::addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f ) { - unsigned start_index = f ? f->start() : 0; - std::vector< Node > subsumed; - return addTermInternal( pbe, c, vals, pol, subsumed, true, f, start_index, 0, false, false ); +Node CegConjecturePbe::SubsumeTrie::addCond(Node c, + const std::vector& vals, + bool pol) +{ + std::vector subsumed; + return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false); } -void CegConjecturePbe::SubsumeTrie::getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f ){ - unsigned start_index = f ? f->start() : 0; - addTermInternal( pbe, Node::null(), vals, pol, subsumed, true, f, start_index, 1, true, true ); +void CegConjecturePbe::SubsumeTrie::getSubsumed(const std::vector& vals, + bool pol, + std::vector& subsumed) +{ + addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true); } -void CegConjecturePbe::SubsumeTrie::getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f ){ +void CegConjecturePbe::SubsumeTrie::getSubsumedBy( + const std::vector& vals, bool pol, std::vector& subsumed_by) +{ // flip polarities - unsigned start_index = f ? f->start() : 0; - addTermInternal( pbe, Node::null(), vals, !pol, subsumed_by, false, f, start_index, 1, true, true ); + addTermInternal( + Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true); } -void CegConjecturePbe::SubsumeTrie::getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, - IndexFilter * f, unsigned index, int status ) { - if( index==vals.size() ){ - Assert( !d_term.isNull() ); - Assert( std::find( v[status].begin(), v[status].end(), d_term )==v[status].end() ); - v[status].push_back( d_term ); - }else{ - Assert( vals[index].isConst() && vals[index].getType().isBoolean() ); - // filter should be for cv - Assert( f==NULL || vals[index]==( pol ? pbe->d_true : pbe->d_false ) ); - for( std::map< Node, SubsumeTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ +void CegConjecturePbe::SubsumeTrie::getLeavesInternal( + const std::vector& vals, + bool pol, + std::map >& v, + unsigned index, + int status) +{ + if (index == vals.size()) + { + Assert(!d_term.isNull()); + Assert(std::find(v[status].begin(), v[status].end(), d_term) + == v[status].end()); + v[status].push_back(d_term); + } + else + { + Assert(vals[index].isConst() && vals[index].getType().isBoolean()); + bool curr_val_true = vals[index].getConst() == pol; + for (std::map::iterator it = d_children.begin(); + it != d_children.end(); + ++it) + { int new_status = status; // if the current value is true - if( vals[index]==( pol ? pbe->d_true : pbe->d_false ) ){ - if( status!=0 ){ - new_status = ( it->first == pbe->d_true ? 1 : -1 ); - if( status!=-2 && new_status!=status ){ + if (curr_val_true) + { + if (status != 0) + { + Assert(it->first.isConst() && it->first.getType().isBoolean()); + new_status = (it->first.getConst() ? 1 : -1); + if (status != -2 && new_status != status) + { new_status = 0; } } } - unsigned next_index = f ? f->next( index ) : index+1; - it->second.getLeavesInternal( pbe, vals, pol, v, f, next_index, new_status ); + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); } } } -void CegConjecturePbe::SubsumeTrie::getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f ) { - unsigned start_index = f ? f->start() : 0; - getLeavesInternal( pbe, vals, pol, v, f, start_index, -2 ); -} - -void CegConjecturePbe::IndexFilter::mk( std::vector< Node >& vals, bool pol ) { - Trace("sygus-pbe-debug") << "Make for : "; - print_val( "sygus-pbe-debug", vals, pol ); - Trace("sygus-pbe-debug") << std::endl; - Node poln = NodeManager::currentNM()->mkConst( pol ); - - unsigned curr_index = 0; - while( curr_index " << curr_index << std::endl; - unsigned i = curr_index; - while( i " << i << std::endl; - curr_index = i; - } - - // verify it is correct - unsigned j = start(); - for( unsigned k=0; kj ); - for( unsigned k=(j+1); k::iterator it = d_next.find( 0 ); - if( it==d_next.end() ){ - return 0; - }else{ - return it->second; - } -} - -unsigned CegConjecturePbe::IndexFilter::next( unsigned i ) { - std::map< unsigned, unsigned >::iterator it = d_next.find( i+1 ); - if( it==d_next.end() ){ - return i+1; - }else{ - return it->second; - } -} - -bool CegConjecturePbe::IndexFilter::isEq( std::vector< Node >& vals, Node v ) { - unsigned index = start(); - while( index& vals, + bool pol, + std::map >& v) +{ + getLeavesInternal(vals, pol, v, 0, -2); } Node CegConjecturePbe::constructSolution( Node c ){ @@ -1839,7 +1866,7 @@ Node CegConjecturePbe::constructSolution( { // could be conditionally solved std::vector subsumed_by; - einfo.d_term_trie.getSubsumedBy(this, x.d_vals, true, subsumed_by); + einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); if (!subsumed_by.empty()) { ret_dt = constructBestSolvedTerm(subsumed_by, x); @@ -2016,7 +2043,7 @@ Node CegConjecturePbe::constructSolution( // get an eligible strategy index unsigned sindex = 0; while (sindex < snode.d_strats.size() - && !x.isValidStrategy(snode.d_strats[sindex])) + && !snode.d_strats[sindex]->isValid(this, x)) { sindex++; } @@ -2117,7 +2144,6 @@ Node CegConjecturePbe::constructSolution( Node cond = einfo_child.d_enum_vals[k]; std::vector solved; itnt->second.d_term_trie.getSubsumedBy( - this, einfo_child.d_enum_vals_res[k], branch_pol, solved); @@ -2145,8 +2171,7 @@ Node CegConjecturePbe::constructSolution( // distinguishable std::map > possible_cond; std::map solved_cond; // stores branch - einfo_child.d_term_trie.getLeaves( - this, x.d_vals, true, possible_cond); + einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); std::map >::iterator itpc = possible_cond.find(0); @@ -2289,14 +2314,34 @@ Node CegConjecturePbe::constructSolution( return ret_dt; } +bool CegConjecturePbe::EnumTypeInfoStrat::isValid(CegConjecturePbe* pbe, + UnifContext& x) +{ + if ((x.d_has_string_pos == role_string_prefix + && d_this == strat_CONCAT_SUFFIX) + || (x.d_has_string_pos == role_string_suffix + && d_this == strat_CONCAT_PREFIX)) + { + return false; + } + return true; +} + +CegConjecturePbe::UnifContext::UnifContext() : d_has_string_pos(role_invalid) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ) { Assert( d_vals.size()==vals.size() ); bool changed = false; - Node poln = pol ? pbe->d_true : pbe->d_false; + Node poln = pol ? d_true : d_false; for( unsigned i=0; id_true ){ - d_vals[i] = pbe->d_false; + if (d_vals[i] == d_true) + { + d_vals[i] = d_false; changed = true; } } @@ -2332,20 +2377,6 @@ bool CegConjecturePbe::UnifContext::isReturnValueModified() { return false; } -bool CegConjecturePbe::UnifContext::isValidStrategy(EnumTypeInfoStrat* etis) -{ - StrategyType st = etis->d_this; - if (d_has_string_pos == role_string_prefix && st == strat_CONCAT_SUFFIX) - { - return false; - } - if (d_has_string_pos == role_string_suffix && st == strat_CONCAT_PREFIX) - { - return false; - } - return true; -} - void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) { Assert( d_vals.empty() ); Assert( d_str_pos.empty() ); @@ -2354,7 +2385,7 @@ void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) Assert( pbe->d_examples.find( c )!=pbe->d_examples.end() ); unsigned sz = pbe->d_examples[c].size(); for( unsigned i=0; id_true ); + d_vals.push_back(d_true); } if( !pbe->d_examples_out[c].empty() ){ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 2b800db81..38a170fbe 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -322,37 +322,73 @@ class CegConjecturePbe : public SygusModule //--------------------------------- end PBE search values // -------------------------------- decision tree learning - // index filter - class IndexFilter { - public: - IndexFilter(){} - void mk( std::vector< Node >& vals, bool pol = true ); - std::map< unsigned, unsigned > d_next; - unsigned start(); - unsigned next( unsigned i ); - void clear() { d_next.clear(); } - bool isEq( std::vector< Node >& vs, Node v ); - }; - // subsumption trie - class SubsumeTrie { - public: - SubsumeTrie(){} - // adds term to the trie, removes based on subsumption - Node addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); - // adds condition to the trie (does not do subsumption) - Node addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f = NULL ); - // returns the set of terms that are subsets of vals - void getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); - // returns the set of terms that are supersets of vals - void getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f = NULL ); - // v[-1,1,0] -> children always false, always true, both - void getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f = NULL ); + /** Subsumption trie + * + * This class manages a set of terms for a PBE sygus enumerator. + * + * In PBE sygus, we are interested in, for each term t, the set of I/O examples + * that it satisfies, which can be represented by a vector of Booleans. + * For example, given conjecture: + * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5 + * If solutions for f are of the form (lambda x. [term]), then: + * Term x satisfies 0001, + * Term x+1 satisfies 1100, + * Term 2 satisfies 0100. + * Above, term 2 is subsumed by term x+1, since the set of I/O examples that + * x+1 satisfies are a superset of those satisfied by 2. + */ + class SubsumeTrie + { + public: + SubsumeTrie() {} + /** + * Adds term t to the trie, removes all terms that are subsumed by t from the + * trie and adds them to subsumed. The set of I/O examples that t satisfies + * is given by (pol ? vals : !vals). + */ + Node addTerm(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed); + /** + * Adds term c to the trie, without calculating/updating based on + * subsumption. This is useful for using this class to store conditionals + * in ITE strategies, where any conditional whose set of vals is unique + * (as opposed to not subsumed) is useful. + */ + Node addCond(Node c, const std::vector& vals, bool pol); + /** + * Returns the set of terms that are subsumed by (pol ? vals : !vals). + */ + void getSubsumed(const std::vector& vals, + bool pol, + std::vector& subsumed); + /** + * Returns the set of terms that subsume (pol ? vals : !vals). This + * is for instance useful when determining whether there exists a term + * that satisfies all active examples in the decision tree learning + * algorithm. + */ + void getSubsumedBy(const std::vector& vals, + bool pol, + std::vector& subsumed_by); + /** + * Get the leaves of the trie, which we store in the map v. + * v[-1] stores the children that always evaluate to !pol, + * v[1] stores the children that always evaluate to pol, + * v[0] stores the children that both evaluate to true and false for at least + * one example. + */ + void getLeaves(const std::vector& vals, + bool pol, + std::map >& v); /** is this trie empty? */ bool isEmpty() { return d_term.isNull() && d_children.empty(); } /** clear this trie */ - void clear() { + void clear() + { d_term = Node::null(); - d_children.clear(); + d_children.clear(); } private: @@ -361,40 +397,43 @@ class CegConjecturePbe : public SygusModule /** the children nodes of this trie */ std::map d_children; /** helper function for above functions */ - Node addTermInternal(CegConjecturePbe* pbe, - Node t, - std::vector& vals, + Node addTermInternal(Node t, + const std::vector& vals, bool pol, std::vector& subsumed, bool spol, - IndexFilter* f, unsigned index, int status, bool checkExistsOnly, bool checkSubsume); /** helper function for above functions */ - void getLeavesInternal(CegConjecturePbe* pbe, - std::vector& vals, + void getLeavesInternal(const std::vector& vals, bool pol, std::map >& v, - IndexFilter* f, unsigned index, int status); }; // -------------------------------- end decision tree learning //------------------------------ representation of a enumeration strategy - - /** information about an enumerator - * - * We say an enumerator is a master enumerator if it is the variable that - * we use to enumerate values for its sort. Master enumerators may have - * (possibly multiple) slave enumerators, stored in d_enum_slave, - */ - class EnumInfo { + /** + * This class stores information regarding an enumerator, including: + * - Information regarding the role of this enumerator (see EnumRole), its + * parent, whether it is templated, its slave enumerators, and so on, and + * - A database of values that have been enumerated for this enumerator. + * + * We say an enumerator is a master enumerator if it is the variable that + * we use to enumerate values for its sort. Master enumerators may have + * (possibly multiple) slave enumerators, stored in d_enum_slave. We make + * the first enumerator for each type a master enumerator, and any additional + * ones slaves of it. + */ + class EnumInfo + { public: EnumInfo() : d_role(enum_io), d_is_conditional(false) {} /** initialize this class + * * c is the parent function-to-synthesize * role is the "role" the enumerator plays in the high-level strategy, * which is one of enum_* above. @@ -412,36 +451,78 @@ class CegConjecturePbe : public SygusModule void setConditional() { d_is_conditional = true; } /** is conditional */ bool isConditional() { return d_is_conditional; } - void addEnumValue(CegConjecturePbe* pbe, - Node v, - std::vector& results); - void setSolved(Node slv); - bool isSolved() { return !d_enum_solved.isNull(); } - Node getSolved() { return d_enum_solved; } + /** get the role of this enumerator */ EnumRole getRole() { return d_role; } + /** + * The candidate variable that this enumerator is for (see sygus_pbe.h). + */ Node d_parent_candidate; - // for template + /** enumerator template + * + * If d_template non-null, enumerated values V are immediately transformed to + * d_template { d_template_arg -> V }. + */ Node d_template; Node d_template_arg; - + /** + * The active guard of this enumerator (see + * TermDbSygus::d_enum_to_active_guard). + */ Node d_active_guard; + /** + * Slave enumerators of this enumerator. These are other enumerators that + * have the same type, but a different role in the strategy tree. We + * generally + * only use one enumerator per type, and hence these slaves are notified when + * values are enumerated for this enumerator. + */ std::vector d_enum_slave; - /** values we have enumerated */ + + //---------------------------enumerated values + /** + * Notify this class that the term v has been enumerated for this enumerator. + * Its evaluation under the set of examples in pbe are stored in results. + */ + void addEnumValue(CegConjecturePbe* pbe, + Node v, + std::vector& results); + /** + * Notify this class that slv is the complete solution to the synthesis + * conjecture. This occurs rarely, for instance, when during an ITE strategy + * we find that a single enumerated term covers all examples. + */ + void setSolved(Node slv); + /** Have we been notified that a complete solution exists? */ + bool isSolved() { return !d_enum_solved.isNull(); } + /** Get the complete solution to the synthesis conjecture. */ + Node getSolved() { return d_enum_solved; } + /** Values that have been enumerated for this enumerator */ std::vector d_enum_vals; /** * This either stores the values of f( I ) for inputs * or the value of f( I ) = O if d_role==enum_io */ std::vector > d_enum_vals_res; + /** + * The set of values in d_enum_vals that have been "subsumed" by others + * (see SubsumeTrie for explanation of subsumed). + */ std::vector d_enum_subsume; + /** Map from values to their index in d_enum_vals. */ std::map d_enum_val_to_index; + /** + * A subsumption trie containing the values in d_enum_vals. Depending on the + * role of this enumerator, values may either be added to d_term_trie with + * subsumption (if role=enum_io), or without (if role=enum_ite_condition or + * enum_concat_term). + */ SubsumeTrie d_term_trie; - + //---------------------------end enumerated values private: /** - * Whether an enumerated value for this conjecture has solved the entire - * conjecture. - */ + * Whether an enumerated value for this conjecture has solved the entire + * conjecture. + */ Node d_enum_solved; /** the role of this enumerator (one of enum_* above). */ EnumRole d_role; @@ -452,37 +533,7 @@ class CegConjecturePbe : public SygusModule std::map< Node, EnumInfo > d_einfo; class CandidateInfo; - - /** represents a strategy for a SyGuS datatype type - * - * This represents a possible strategy to apply when processing a strategy - * node in constructSolution. When applying the strategy represented by this - * class, we may make recursive calls to the children of the strategy, - * given in d_cenum. If all recursive calls to constructSolution are - * successful, say: - * constructSolution( c, d_cenum[1], ... ) = t1, - * ..., - * constructSolution( c, d_cenum[n], ... ) = tn, - * Then, the solution returned by this strategy is - * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } - */ - class EnumTypeInfoStrat { - public: - /** the type of strategy this represents */ - StrategyType d_this; - /** the sygus datatype constructor that induced this strategy - * - * For example, this may be a sygus datatype whose sygus operator is ITE, - * if the strategy type above is strat_ITE. - */ - Node d_cons; - /** children of this strategy */ - std::vector > d_cenum; - /** the arguments for the (templated) solution */ - std::vector d_sol_templ_args; - /** the template for the solution */ - Node d_sol_templ; - }; + class EnumTypeInfoStrat; /** represents a node in the strategy graph * @@ -636,31 +687,40 @@ class CegConjecturePbe : public SygusModule //------------------------------ end strategy registration //------------------------------ constructing solutions - class UnifContext { - public: - UnifContext() : d_has_string_pos(role_invalid) {} - /** this intiializes this context for function-to-synthesize c */ - void initialize(CegConjecturePbe* pbe, Node c); + /** Unification context + * + * This class maintains state information during calls to + * CegConjecturePbe::constructSolution, which implements unification-based + * approaches for construction solutions to synthesis conjectures. + */ + class UnifContext + { + public: + UnifContext(); + /** this intiializes this context for function-to-synthesize c */ + void initialize(CegConjecturePbe* pbe, Node c); - //----------for ITE strategy - /** the value of the context conditional + //----------for ITE strategy + /** the value of the context conditional * * This stores a list of Boolean constants that is the same length of the * number of input/output example pairs we are considering. For each i, * if d_vals[i] = true, i/o pair #i is active according to this context * if d_vals[i] = false, i/o pair #i is inactive according to this context */ - std::vector d_vals; - /** update the examples + std::vector d_vals; + /** update the examples * * if pol=true, this method updates d_vals to d_vals & vals * if pol=false, this method updates d_vals to d_vals & ( ~vals ) */ - bool updateContext(CegConjecturePbe* pbe, std::vector& vals, bool pol); - //----------end for ITE strategy + bool updateContext(CegConjecturePbe* pbe, + std::vector& vals, + bool pol); + //----------end for ITE strategy - //----------for CONCAT strategies - /** the position in the strings + //----------for CONCAT strategies + /** the position in the strings * * For each i/o example pair, this stores the length of the current solution * for the input of the pair, where the solution for that input is a prefix @@ -673,30 +733,31 @@ class CegConjecturePbe : public SygusModule * str.++( "abc", "c" ) is a prefix of "abcdcd" and * str.++( "aa", "c" ) is a prefix of "aacd". */ - std::vector d_str_pos; - /** has string position + std::vector d_str_pos; + /** has string position * * Whether the solution positions indicate a prefix or suffix of the output * examples. If this is role_invalid, then we have not updated the string * position. */ - NodeRole d_has_string_pos; - /** update the string examples + NodeRole d_has_string_pos; + /** update the string examples * * This method updates d_str_pos to d_str_pos + pos. */ - bool updateStringPosition(CegConjecturePbe* pbe, std::vector& pos); - /** get current strings + bool updateStringPosition(CegConjecturePbe* pbe, + std::vector& pos); + /** get current strings * * This returns the prefix/suffix of the string constants stored in vals * of size d_str_pos, and stores the result in ex_vals. For example, if vals * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add * "d" and "de" to ex_vals. */ - void getCurrentStrings(CegConjecturePbe* pbe, - const std::vector& vals, - std::vector& ex_vals); - /** get string increment + void getCurrentStrings(CegConjecturePbe* pbe, + const std::vector& vals, + std::vector& ex_vals); + /** get string increment * * If this method returns true, then inc and tot are updated such that * for all active indices i, @@ -706,40 +767,38 @@ class CegConjecturePbe : public SygusModule * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total * number of characters incremented across all examples. */ - bool getStringIncrement(CegConjecturePbe* pbe, - bool isPrefix, - const std::vector& ex_vals, - const std::vector& vals, - std::vector& inc, - unsigned& tot); - /** returns true if ex_vals[i] = vals[i] for all active indices i. */ - bool isStringSolved(CegConjecturePbe* pbe, - const std::vector& ex_vals, - const std::vector& vals); - //----------end for CONCAT strategies - - /** is return value modified? + bool getStringIncrement(CegConjecturePbe* pbe, + bool isPrefix, + const std::vector& ex_vals, + const std::vector& vals, + std::vector& inc, + unsigned& tot); + /** returns true if ex_vals[i] = vals[i] for all active indices i. */ + bool isStringSolved(CegConjecturePbe* pbe, + const std::vector& ex_vals, + const std::vector& vals); + //----------end for CONCAT strategies + + /** is return value modified? * * This returns true if we are currently in a state where the return value * of the solution has been modified, e.g. by a previous node that solved * for a prefix. */ - bool isReturnValueModified(); - /** returns true if argument is valid strategy in this context */ - bool isValidStrategy(EnumTypeInfoStrat* etis); - /** visited role + bool isReturnValueModified(); + /** visited role * * This is the current set of enumerator/node role pairs we are currently * visiting. This set is cleared when the context is updated. */ - std::map > d_visit_role; - - /** unif context enumerator information */ - class UEnumInfo - { - public: - UEnumInfo() {} - /** map from conditions and branch positions to a solved node + std::map > d_visit_role; + + /** unif context enumerator information */ + class UEnumInfo + { + public: + UEnumInfo() {} + /** map from conditions and branch positions to a solved node * * For example, if we have: * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 @@ -752,10 +811,15 @@ class CegConjecturePbe : public SygusModule * resulting in 2 and 4, are equal to the output value for the respective * pairs. */ - std::map > d_look_ahead_sols; + std::map > d_look_ahead_sols; }; /** map from enumerators to the above info class */ - std::map< Node, UEnumInfo > d_uinfo; + std::map d_uinfo; + + private: + /** true and false nodes */ + Node d_true; + Node d_false; }; /** construct solution @@ -799,6 +863,41 @@ class CegConjecturePbe : public SygusModule std::map< Node, std::vector< unsigned > > incr, UnifContext& x ); //------------------------------ end constructing solutions + + /** represents a strategy for a SyGuS datatype type + * + * This represents a possible strategy to apply when processing a strategy + * node in constructSolution. When applying the strategy represented by this + * class, we may make recursive calls to the children of the strategy, + * given in d_cenum. If all recursive calls to constructSolution for these + * children are successful, say: + * constructSolution( c, d_cenum[1], ... ) = t1, + * ..., + * constructSolution( c, d_cenum[n], ... ) = tn, + * Then, the solution returned by this strategy is + * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } + * where * is application of substitution. + */ + class EnumTypeInfoStrat + { + public: + /** the type of strategy this represents */ + StrategyType d_this; + /** the sygus datatype constructor that induced this strategy + * + * For example, this may be a sygus datatype whose sygus operator is ITE, + * if the strategy type above is strat_ITE. + */ + Node d_cons; + /** children of this strategy */ + std::vector > d_cenum; + /** the arguments for the (templated) solution */ + std::vector d_sol_templ_args; + /** the template for the solution */ + Node d_sol_templ; + /** Returns true if argument is valid strategy in context x */ + bool isValid(CegConjecturePbe* pbe, UnifContext& x); + }; }; }/* namespace CVC4::theory::quantifiers */