return true;
}
Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){
+ //return mkSkolemS( c, isLenSplit );
std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit );
if( it==d_skolem_cache[a][b].end() ){
Node sk = mkSkolemS( c, isLenSplit );
}else{
return it->second;
}
+
}
bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms,
}
}else{
if( !areEqual( n, nrc ) ){
- expl = mkExplain( exp );
if( n.getType().isBoolean() ){
exp.push_back( nrc==d_true ? n.negate() : n );
+ //exp.push_back( n );
conc = d_false;
}else{
conc = n.eqNode( nrc );
}
+ expl = mkExplain( exp );
}
}
if( !conc.isNull() ){