namespace theory {
namespace strings {
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+ switch (i)
+ {
+ case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
+ case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
+ case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;
+ case INFER_LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
+ case INFER_SSPLIT_CST_BINARY: out << "S-Split(CST-P)-binary"; break;
+ case INFER_SSPLIT_CST: out << "S-Split(CST-P)"; break;
+ case INFER_SSPLIT_VAR: out << "S-Split(VAR)"; break;
+ case INFER_FLOOP: out << "F-Loop"; break;
+ default: out << "?"; break;
+ }
+ return out;
+}
+
Node TheoryStrings::TermIndex::add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c ) {
if( index==n.getNumChildren() ){
if( d_data.isNull() ){
Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl;
unsigned min_id = 9;
unsigned max_index = 0;
- for( unsigned i=0; i<pinfer.size(); i++ ){
+ for (unsigned i = 0, size = pinfer.size(); i < size; i++)
+ {
Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : ";
- Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].getId() << std::endl;
+ Trace("strings-solve")
+ << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl;
if( use_index==-1 || pinfer[i].d_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_index ) ){
min_id = pinfer[i].d_id;
max_index = pinfer[i].d_index;
Assert( !pinfer[use_index].d_nf_pair[1].isNull() );
addNormalFormPair( pinfer[use_index].d_nf_pair[0], pinfer[use_index].d_nf_pair[1] );
}
- sendInference( pinfer[use_index].d_ant, pinfer[use_index].d_antn, pinfer[use_index].d_conc, pinfer[use_index].getId(), pinfer[use_index].sendAsLemma() );
+ std::stringstream ssi;
+ ssi << pinfer[use_index].d_id;
+ sendInference(pinfer[use_index].d_ant,
+ pinfer[use_index].d_antn,
+ pinfer[use_index].d_conc,
+ ssi.str().c_str(),
+ pinfer[use_index].sendAsLemma());
for( std::map< int, std::vector< Node > >::iterator it = pinfer[use_index].d_new_skolem.begin(); it != pinfer[use_index].d_new_skolem.end(); ++it ){
for( unsigned i=0; i<it->second.size(); i++ ){
if( it->first==0 ){
//set info
info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, length_eq, length_eq.negate() );
info.d_pending_phase[ length_eq ] = true;
- info.d_id = 3;
+ info.d_id = INFER_LEN_SPLIT;
info_valid = true;
}else{
Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
Node eq = other_str.eqNode( d_emptyString );
//set info
info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
- info.d_id = 4;
+ info.d_id = INFER_LEN_SPLIT_EMP;
info_valid = true;
}else{
if( !isRev ){ //FIXME
//set info
info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );
info.d_new_skolem[0].push_back( sk );
- info.d_id = 1;
+ info.d_id = INFER_SSPLIT_CST_PROP;
info_valid = true;
}
/* FIXME for isRev, speculative
sk.eqNode( d_emptyString ).negate(),
c_firstHalf.eqNode( isRev ? mkConcat( sk, other_str ) : mkConcat( other_str, sk ) ) ) );
info.d_new_skolem[0].push_back( sk );
- info.d_id = 5;
+ info.d_id = INFER_SSPLIT_CST_BINARY;
info_valid = true;
}else{
// normal v/c split
Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl;
info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, firstChar ) : mkConcat(firstChar, sk) );
info.d_new_skolem[0].push_back( sk );
- info.d_id = 6;
+ info.d_id = INFER_SSPLIT_CST;
info_valid = true;
}
}
if( lentTestSuccess!=-1 ){
info.d_antn.push_back( lentTestExp );
info.d_conc = lentTestSuccess==0 ? eq1 : eq2;
- info.d_id = 2;
+ info.d_id = INFER_SSPLIT_VAR_PROP;
info_valid = true;
}else{
Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate();
}
//set info
info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
- info.d_id = 7;
+ info.d_id = INFER_SSPLIT_VAR;
info_valid = true;
}
}
{
// try to make t equal to empty to avoid loop
info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
- info.d_id = 4;
+ info.d_id = INFER_LEN_SPLIT_EMP;
return true;
}
else
if (options::stringProcessLoop())
{
info.d_conc = conc;
- info.d_id = 8;
+ info.d_id = INFER_FLOOP;
info.d_nf_pair[0] = normal_form_src[i];
info.d_nf_pair[1] = normal_form_src[j];
return true;
*
*/
+/** Types of inferences used in the procedure
+ *
+ * These are variants of the inference rules in Figures 3-5 of Liang et al.
+ * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
+ */
+enum Inference
+{
+ INFER_NONE,
+ // string split constant propagation, for example:
+ // x = y, x = "abc", y = y1 ++ "b" ++ y2
+ // implies y1 = "a" ++ y1'
+ INFER_SSPLIT_CST_PROP,
+ // string split variable propagation, for example:
+ // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
+ // implies x1 = y1 ++ x1'
+ // This is inspired by Zheng et al CAV 2015.
+ INFER_SSPLIT_VAR_PROP,
+ // length split, for example:
+ // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
+ // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
+ INFER_LEN_SPLIT,
+ // length split empty, for example:
+ // z = "" V z != ""
+ // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
+ INFER_LEN_SPLIT_EMP,
+ // string split constant binary, for example:
+ // x1 = "aaaa" ++ x1' V "aaaa" = x1 ++ x1'
+ // This is inferred when, e.g. x = y, x = x1 ++ x2, y = "aaaaaaaa" ++ y2.
+ // This inference is disabled by default and is enabled by stringBinaryCsp().
+ INFER_SSPLIT_CST_BINARY,
+ // string split constant
+ // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
+ // implies y1 = "c" ++ y1'
+ // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
+ INFER_SSPLIT_CST,
+ // string split variable, for example:
+ // x = y, x = x1 ++ x2, y = y1 ++ y2
+ // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
+ // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
+ INFER_SSPLIT_VAR,
+ // flat form loop, for example:
+ // x = y, x = x1 ++ z, y = z ++ y2
+ // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
+ // for fresh u, u1, u2.
+ // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
+ INFER_FLOOP,
+};
+std::ostream& operator<<(std::ostream& out, Inference i);
+
struct StringsProxyVarAttributeId {};
typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
std::vector< Node > d_antn;
std::map< int, std::vector< Node > > d_new_skolem;
Node d_conc;
- unsigned d_id;
+ Inference d_id;
std::map< Node, bool > d_pending_phase;
unsigned d_index;
- const char * getId() {
- switch( d_id ){
- case 1:return "S-Split(CST-P)-prop";break;
- case 2:return "S-Split(VAR)-prop";break;
- case 3:return "Len-Split(Len)";break;
- case 4:return "Len-Split(Emp)";break;
- case 5:return "S-Split(CST-P)-binary";break;
- case 6:return "S-Split(CST-P)";break;
- case 7:return "S-Split(VAR)";break;
- case 8:return "F-Loop";break;
- default:break;
- }
- return "";
- }
Node d_nf_pair[2];
bool sendAsLemma();
};
projects / cvc5.git / commitdiff