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() ){
}
}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 : "
}
// 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<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<bool>());
+ // 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<bool> check_subsumed_by;
+ if (status == 0)
+ {
+ if (!cv.getConst<bool>())
+ {
+ check_subsumed_by.push_back(spol);
}
- // check for subsumed nodes
- for( unsigned i=0; i<check_subsumed_by.size(); i++ ){
- Node csval = check_subsumed_by[i] ? pbe->d_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<bool>())
+ {
+ 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<Node, SubsumeTrie>::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<bool> check_subsume;
+ if (status == 0)
+ {
+ if (checkExistsOnly)
+ {
+ std::map<Node, SubsumeTrie>::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; i<check_subsume.size(); i++ ){
- Node csval = check_subsume[i] ? pbe->d_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<bool>())
+ {
+ 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<bool>())
+ {
+ 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<bool>(check_subsume[i]);
+ std::map<Node, SubsumeTrie>::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<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<Node>& vals,
+ bool pol)
+{
+ std::vector<Node> 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<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<Node>& vals, bool pol, std::vector<Node>& 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<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& 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<bool>() == pol;
+ for (std::map<Node, SubsumeTrie>::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<bool>() ? 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<vals.size() && vals[curr_index]!=poln ){
- curr_index++;
- }
- d_next[0] = curr_index;
- Trace("sygus-pbe-debug") << "0 -> " << curr_index << std::endl;
- unsigned i = curr_index;
- while( i<vals.size() ){
- while( i<vals.size() && vals[i]!=poln ){
- i++;
- }
- i++;
- d_next[curr_index+1] = i;
- Trace("sygus-pbe-debug") << curr_index+1 << " -> " << i << std::endl;
- curr_index = i;
- }
-
- // verify it is correct
- unsigned j = start();
- for( unsigned k=0; k<j; k++ ){
- AlwaysAssert( vals[k]!=poln );
- }
- Trace("sygus-pbe-debug") << "...start : " << j << std::endl;
- unsigned counter = 0;
- while( j<vals.size() ){
- Trace("sygus-pbe-debug") << "...at : " << j << std::endl;
- AlwaysAssert( vals[j]==poln );
- unsigned jj = next( j );
- AlwaysAssert( jj>j );
- for( unsigned k=(j+1); k<jj; k++ ){
- AlwaysAssert( vals[k]!=poln );
- }
- AlwaysAssert( counter<=vals.size() );
- counter++;
- j = jj;
- }
-
-
-}
-
-unsigned CegConjecturePbe::IndexFilter::start() {
- std::map< unsigned, unsigned >::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.size() ){
- if( vals[index]!=v ){
- return false;
- }
- index = next( index );
- }
- return true;
+void CegConjecturePbe::SubsumeTrie::getLeaves(
+ const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v)
+{
+ getLeavesInternal(vals, pol, v, 0, -2);
}
Node CegConjecturePbe::constructSolution( Node c ){
{
// could be conditionally solved
std::vector<Node> 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);
// 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++;
}
Node cond = einfo_child.d_enum_vals[k];
std::vector<Node> solved;
itnt->second.d_term_trie.getSubsumedBy(
- this,
einfo_child.d_enum_vals_res[k],
branch_pol,
solved);
// distinguishable
std::map<int, std::vector<Node> > possible_cond;
std::map<Node, int> 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<int, std::vector<Node> >::iterator itpc =
possible_cond.find(0);
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; i<vals.size(); i++ ){
if( vals[i]!=poln ){
- if( d_vals[i]==pbe->d_true ){
- d_vals[i] = pbe->d_false;
+ if (d_vals[i] == d_true)
+ {
+ d_vals[i] = d_false;
changed = true;
}
}
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() );
Assert( pbe->d_examples.find( c )!=pbe->d_examples.end() );
unsigned sz = pbe->d_examples[c].size();
for( unsigned i=0; i<sz; i++ ){
- d_vals.push_back( pbe->d_true );
+ d_vals.push_back(d_true);
}
if( !pbe->d_examples_out[c].empty() ){
//--------------------------------- 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<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<Node>& vals, bool pol);
+ /**
+ * Returns the set of terms that are subsumed by (pol ? vals : !vals).
+ */
+ void getSubsumed(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<Node>& vals,
+ bool pol,
+ std::vector<Node>& 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<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& 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:
/** the children nodes of this trie */
std::map<Node, SubsumeTrie> d_children;
/** helper function for above functions */
- Node addTermInternal(CegConjecturePbe* pbe,
- Node t,
- std::vector<Node>& vals,
+ Node addTermInternal(Node t,
+ const std::vector<Node>& vals,
bool pol,
std::vector<Node>& subsumed,
bool spol,
- IndexFilter* f,
unsigned index,
int status,
bool checkExistsOnly,
bool checkSubsume);
/** helper function for above functions */
- void getLeavesInternal(CegConjecturePbe* pbe,
- std::vector<Node>& vals,
+ void getLeavesInternal(const std::vector<Node>& vals,
bool pol,
std::map<int, std::vector<Node> >& 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.
void setConditional() { d_is_conditional = true; }
/** is conditional */
bool isConditional() { return d_is_conditional; }
- void addEnumValue(CegConjecturePbe* pbe,
- Node v,
- std::vector<Node>& 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<Node> 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<Node>& 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<Node> 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<std::vector<Node> > 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<Node> d_enum_subsume;
+ /** Map from values to their index in d_enum_vals. */
std::map<Node, unsigned> 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;
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<std::pair<Node, NodeRole> > d_cenum;
- /** the arguments for the (templated) solution */
- std::vector<Node> d_sol_templ_args;
- /** the template for the solution */
- Node d_sol_templ;
- };
+ class EnumTypeInfoStrat;
/** represents a node in the strategy graph
*
//------------------------------ 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<Node> d_vals;
- /** update the examples
+ std::vector<Node> 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<Node>& vals, bool pol);
- //----------end for ITE strategy
+ bool updateContext(CegConjecturePbe* pbe,
+ std::vector<Node>& 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
* str.++( "abc", "c" ) is a prefix of "abcdcd" and
* str.++( "aa", "c" ) is a prefix of "aacd".
*/
- std::vector<unsigned> d_str_pos;
- /** has string position
+ std::vector<unsigned> 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<unsigned>& pos);
- /** get current strings
+ bool updateStringPosition(CegConjecturePbe* pbe,
+ std::vector<unsigned>& 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<Node>& vals,
- std::vector<String>& ex_vals);
- /** get string increment
+ void getCurrentStrings(CegConjecturePbe* pbe,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals);
+ /** get string increment
*
* If this method returns true, then inc and tot are updated such that
* for all active indices i,
* 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<String>& ex_vals,
- const std::vector<Node>& vals,
- std::vector<unsigned>& inc,
- unsigned& tot);
- /** returns true if ex_vals[i] = vals[i] for all active indices i. */
- bool isStringSolved(CegConjecturePbe* pbe,
- const std::vector<String>& ex_vals,
- const std::vector<Node>& vals);
- //----------end for CONCAT strategies
-
- /** is return value modified?
+ bool getStringIncrement(CegConjecturePbe* pbe,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot);
+ /** returns true if ex_vals[i] = vals[i] for all active indices i. */
+ bool isStringSolved(CegConjecturePbe* pbe,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& 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<Node, std::map<NodeRole, bool> > d_visit_role;
-
- /** unif context enumerator information */
- class UEnumInfo
- {
- public:
- UEnumInfo() {}
- /** map from conditions and branch positions to a solved node
+ std::map<Node, std::map<NodeRole, bool> > 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
* resulting in 2 and 4, are equal to the output value for the respective
* pairs.
*/
- std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+ std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
};
/** map from enumerators to the above info class */
- std::map< Node, UEnumInfo > d_uinfo;
+ std::map<Node, UEnumInfo> d_uinfo;
+
+ private:
+ /** true and false nodes */
+ Node d_true;
+ Node d_false;
};
/** construct solution
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<std::pair<Node, NodeRole> > d_cenum;
+ /** the arguments for the (templated) solution */
+ std::vector<Node> 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 */
projects / cvc5.git / commitdiff