//add to tester if applicable
Node t_arg;
int tindex = DatatypesRewriter::isTester( atom, t_arg );
- if( tindex!=-1 ){
+ if (tindex >= 0)
+ {
Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
Node rep = getRepresentative( t_arg );
EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
//merge labels
- NodeIntMap::iterator lbl_i = d_labels.find( t2 );
+ NodeUIntMap::iterator lbl_i = d_labels.find(t2);
if( lbl_i != d_labels.end() ){
Trace("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl;
- int n_label = (*lbl_i).second;
- for( int i=0; i<n_label; i++ ){
- Assert( i<(int)d_labels_data[ t2 ].size() );
+ size_t n_label = (*lbl_i).second;
+ for (size_t i = 0; i < n_label; i++)
+ {
+ Assert(i < d_labels_data[t2].size());
Node t = d_labels_data[ t2 ][i];
- Node tt = t.getKind()==kind::NOT ? t[0] : t;
- Node t_arg;
- int tindex = DatatypesRewriter::isTester( tt, t_arg );
- Assert( tindex!=-1 );
+ Node t_arg = d_labels_args[t2][i];
+ unsigned tindex = d_labels_tindex[t2][i];
addTester( tindex, t, eqc1, t1, t_arg );
if( d_conflict ){
Trace("datatypes-debug") << " conflict!" << std::endl;
eqc1->d_selectors = true;
checkInst = true;
}
- NodeIntMap::iterator sel_i = d_selector_apps.find( t2 );
+ NodeUIntMap::iterator sel_i = d_selector_apps.find(t2);
if( sel_i != d_selector_apps.end() ){
Trace("datatypes-debug") << " merge selectors from " << eqc2 << " " << t2 << std::endl;
- int n_sel = (*sel_i).second;
- for( int j=0; j<n_sel; j++ ){
+ size_t n_sel = (*sel_i).second;
+ for (size_t j = 0; j < n_sel; j++)
+ {
addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() );
}
}
}
Node TheoryDatatypes::getLabel( Node n ) {
- NodeIntMap::iterator lbl_i = d_labels.find( n );
+ NodeUIntMap::iterator lbl_i = d_labels.find(n);
if( lbl_i != d_labels.end() ){
- unsigned n_lbl = (*lbl_i).second;
+ size_t n_lbl = (*lbl_i).second;
if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){
return d_labels_data[n][ n_lbl-1 ];
}
}
bool TheoryDatatypes::hasTester( Node n ) {
- NodeIntMap::iterator lbl_i = d_labels.find( n );
+ NodeUIntMap::iterator lbl_i = d_labels.find(n);
if( lbl_i != d_labels.end() ){
return (*lbl_i).second>0;
}else{
if( lindex!=-1 ){
pcons[ lindex ] = true;
}else{
- NodeIntMap::iterator lbl_i = d_labels.find( n );
+ NodeUIntMap::iterator lbl_i = d_labels.find(n);
if( lbl_i != d_labels.end() ){
- int n_lbl = (*lbl_i).second;
- for( int i=0; i<n_lbl; i++ ){
- Node t = d_labels_data[n][i];
- Assert( t.getKind()==NOT );
- int tindex = DatatypesRewriter::isTester( t[0] );
- Assert( tindex!=-1 );
+ size_t n_lbl = (*lbl_i).second;
+ for (size_t i = 0; i < n_lbl; i++)
+ {
+ Assert(d_labels_data[n][i].getKind() == NOT);
+ unsigned tindex = d_labels_tindex[n][i];
pcons[ tindex ] = false;
}
}
}
}
-void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ){
+void TheoryDatatypes::addTester(
+ unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg)
+{
Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
bool tpolarity = t.getKind()!=NOT;
Node j, jt;
bool makeConflict = false;
- int jtindex0 = getLabelIndex( eqc, n );
- if( jtindex0!=-1 ){
+ int prevTIndex = getLabelIndex(eqc, n);
+ if (prevTIndex >= 0)
+ {
+ unsigned ptu = static_cast<unsigned>(prevTIndex);
//if we already know the constructor type, check whether it is in conflict or redundant
- if( (jtindex0==ttindex)!=tpolarity ){
+ if ((ptu == ttindex) != tpolarity)
+ {
if( !eqc->d_constructor.get().isNull() ){
//conflict because equivalence class contains a constructor
std::vector< TNode > assumptions;
}
}else{
//otherwise, scan list of labels
- NodeIntMap::iterator lbl_i = d_labels.find( n );
+ NodeUIntMap::iterator lbl_i = d_labels.find(n);
Assert( lbl_i != d_labels.end() );
- int n_lbl = (*lbl_i).second;
+ size_t n_lbl = (*lbl_i).second;
std::map< int, bool > neg_testers;
- for( int i=0; i<n_lbl; i++ ){
- Node ti = d_labels_data[n][i];
- Assert( ti.getKind()==NOT );
- j = ti;
- jt = j[0];
- int jtindex = DatatypesRewriter::isTester( jt );
- Assert( jtindex!=-1 );
+ for (size_t i = 0; i < n_lbl; i++)
+ {
+ Assert(d_labels_data[n][i].getKind() == NOT);
+ unsigned jtindex = d_labels_tindex[n][i];
if( jtindex==ttindex ){
if( tpolarity ){ //we are in conflict
+ j = d_labels_data[n][i];
+ jt = j[0];
makeConflict = true;
break;
}else{ //it is redundant
}
if( !makeConflict ){
Debug("datatypes-labels") << "Add to labels " << t << std::endl;
- //lbl->push_back( t );
d_labels[n] = n_lbl + 1;
- if( n_lbl<(int)d_labels_data[n].size() ){
+ if (n_lbl < d_labels_data[n].size())
+ {
+ // reuse spot in the vector
d_labels_data[n][n_lbl] = t;
+ d_labels_args[n][n_lbl] = t_arg;
+ d_labels_tindex[n][n_lbl] = ttindex;
}else{
- d_labels_data[n].push_back( t );
+ d_labels_data[n].push_back(t);
+ d_labels_args[n].push_back(t_arg);
+ d_labels_tindex[n].push_back(ttindex);
}
n_lbl++;
Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
if( tpolarity ){
instantiate( eqc, n );
- //TODO : and it is not the other testers FIXME
- for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){
Assert( n.getKind()!=APPLY_CONSTRUCTOR );
Node infer = DatatypesRewriter::mkTester( n, i, dt ).negate();
}else{
//check if we have reached the maximum number of testers
// in this case, add the positive tester
- //this should not be done for sygus, since cases may be limited
- if( n_lbl==(int)dt.getNumConstructors()-1 ){
+ if (n_lbl == dt.getNumConstructors() - 1)
+ {
std::vector< bool > pcons;
getPossibleCons( eqc, n, pcons );
int testerIndex = -1;
//we must explain why each term in the set of testers for this equivalence class is equal
std::vector< Node > eq_terms;
NodeBuilder<> nb(kind::AND);
- //for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-
- for( int i=0; i<n_lbl; i++ ){
+ for (unsigned i = 0; i < n_lbl; i++)
+ {
Node ti = d_labels_data[n][i];
nb << ti;
Assert( ti.getKind()==NOT );
- Node t_arg2;
- DatatypesRewriter::isTester( ti[0], t_arg2 );
- //Assert( tindex!=-1 );
+ Node t_arg2 = d_labels_args[n][i];
if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
eq_terms.push_back( t_arg2 );
if( t_arg2!=t_arg ){
void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
//check to see if it is redundant
- NodeIntMap::iterator sel_i = d_selector_apps.find( n );
+ NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
Assert( sel_i != d_selector_apps.end() );
if( sel_i != d_selector_apps.end() ){
- int n_sel = (*sel_i).second;
- for( int j=0; j<n_sel; j++ ){
+ size_t n_sel = (*sel_i).second;
+ for (size_t j = 0; j < n_sel; j++)
+ {
Node ss = d_selector_apps_data[n][j];
if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
Trace("dt-collapse-sel") << "...redundant." << std::endl;
//add it to the vector
//sel->push_back( s );
d_selector_apps[n] = n_sel + 1;
- if( n_sel<(int)d_selector_apps_data[n].size() ){
+ if (n_sel < d_selector_apps_data[n].size())
+ {
d_selector_apps_data[n][n_sel] = s;
}else{
d_selector_apps_data[n].push_back( s );
Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
Assert( eqc->d_constructor.get().isNull() );
//check labels
- NodeIntMap::iterator lbl_i = d_labels.find( n );
+ NodeUIntMap::iterator lbl_i = d_labels.find(n);
if( lbl_i != d_labels.end() ){
size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
- int n_lbl = (*lbl_i).second;
- for( int i=0; i<n_lbl; i++ ){
+ size_t n_lbl = (*lbl_i).second;
+ for (size_t i = 0; i < n_lbl; i++)
+ {
Node t = d_labels_data[n][i];
- if( t.getKind()==NOT ){
- int tindex = DatatypesRewriter::isTester( t[0] );
- Assert( tindex!=-1 );
- if( tindex==(int)constructorIndex ){
+ if (d_labels_data[n][i].getKind() == NOT)
+ {
+ unsigned tindex = d_labels_tindex[n][i];
+ if (tindex == constructorIndex)
+ {
std::vector< TNode > assumptions;
explain( t, assumptions );
explainEquality( c, t[0][0], true, assumptions );
}
}
//check selectors
- NodeIntMap::iterator sel_i = d_selector_apps.find( n );
+ NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
if( sel_i != d_selector_apps.end() ){
- int n_sel = (*sel_i).second;
- for( int j=0; j<n_sel; j++ ){
+ size_t n_sel = (*sel_i).second;
+ for (size_t j = 0; j < n_sel; j++)
+ {
Node s = d_selector_apps_data[n][j];
//collapse the selector
collapseSelector( s, c );
if( hasLabel( ei, eqc ) ){
Trace( c ) << getLabel( eqc );
}else{
- NodeIntMap::iterator lbl_i = d_labels.find( eqc );
+ NodeUIntMap::iterator lbl_i = d_labels.find(eqc);
if( lbl_i != d_labels.end() ){
- for( int j=0; j<(*lbl_i).second; j++ ){
+ for (size_t j = 0; j < (*lbl_i).second; j++)
+ {
Trace( c ) << d_labels_data[eqc][j] << " ";
}
}
}
Trace( c ) << std::endl;
Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
- NodeIntMap::iterator sel_i = d_selector_apps.find( eqc );
+ NodeUIntMap::iterator sel_i = d_selector_apps.find(eqc);
if( sel_i != d_selector_apps.end() ){
- for( int j=0; j<(*sel_i).second; j++ ){
+ for (size_t j = 0; j < (*sel_i).second; j++)
+ {
Trace( c ) << d_selector_apps_data[eqc][j] << " ";
}
}
class TheoryDatatypes : public Theory {
private:
typedef context::CDList<Node> NodeList;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ /** maps nodes to an index in a vector */
+ typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap;
typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
std::map< Node, EqcInfo* > d_eqc_info;
/** map from nodes to their instantiated equivalent for each constructor type */
std::map< Node, std::map< int, Node > > d_inst_map;
- /** which instantiation lemmas we have sent */
- //std::map< Node, std::vector< Node > > d_inst_lemmas;
+ //---------------------------------labels
/** labels for each equivalence class
- * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either:
+ *
+ * For each eqc r, d_labels[r] is testers that hold for this equivalence
+ * class, either:
* a list of equations of the form
- * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers
- * and n is less than the number of possible constructors for t minus one,
+ * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of
+ * which are unique testers, n is less than the number of possible
+ * constructors for t minus one,
* or a list of equations of the form
- * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by
- * is_[constructor_(n+1)]( t ), each of which is a unique tester.
- */
- NodeIntMap d_labels;
+ * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by
+ * is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester.
+ * In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r.
+ *
+ * We store this list in a context-dependent way, using the four data
+ * structures below. The three vectors d_labels_data, d_labels_args, and
+ * d_labels_tindex store the tester applications, their arguments and the
+ * tester index of the application. The map d_labels stores the number of
+ * values in these vectors that is valid in the current context (this is an
+ * optimization that ensures we don't need to pop data when changing SAT
+ * contexts).
+ */
+ NodeUIntMap d_labels;
+ /** the tester applications */
std::map< Node, std::vector< Node > > d_labels_data;
+ /** the argument of each node in d_labels_data */
+ std::map<Node, std::vector<Node> > d_labels_args;
+ /** the tester index of each node in d_labels_data */
+ std::map<Node, std::vector<unsigned> > d_labels_tindex;
+ //---------------------------------end labels
/** selector apps for eqch equivalence class */
- NodeIntMap d_selector_apps;
+ NodeUIntMap d_selector_apps;
std::map< Node, std::vector< Node > > d_selector_apps_data;
/** Are we in conflict */
context::CDO<bool> d_conflict;
private:
/** add tester to equivalence class info */
- void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
+ void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg);
/** add selector to equivalence class info */
void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true );
/** add constructor */
projects / cvc5.git / commitdiff