mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 05:00:51 +00:00
Code Activity

add theory_str::check_length_consistency, WIP

Browse source
This commit is contained in:
Murphy Berzish 2016-07-27 16:18:05 -04:00
parent a31a948a5b
commit 95f1cfa5a6
2 changed files with 31 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/smt/theory_str.cpp
View file

@ -4141,9 +4141,36 @@ bool theory_str::can_two_nodes_eq(expr * n1, expr * n2) {
return true; return true;
} }
// was checkLength2ConstStr() in Z3str2
// returns true if everything is OK, or false if inconsistency detected
// - note that these are different from the semantics in Z3str2
bool theory_str::check_length_const_string(expr * n1, expr * constStr) {
// TODO NEXT
NOT_IMPLEMENTED_YET(); return true;
}
// returns true if everything is OK, or false if inconsistency detected
// - note that these are different from the semantics in Z3str2
bool theory_str::check_length_eq_var_concat(expr * n1, expr * n2) {
// TODO NEXT
NOT_IMPLEMENTED_YET(); return true;
}
// returns false if an inconsistency is detected, or true if no inconsistencies were found
// - note that these are different from the semantics of checkLengConsistency() in Z3str2
bool theory_str::check_length_consistency(expr * n1, expr * n2) { bool theory_str::check_length_consistency(expr * n1, expr * n2) {
// TODO NEXT if (m_strutil.is_string(n1) && m_strutil.is_string(n2)) {
NOT_IMPLEMENTED_YET(); return true; // consistency has already been checked in can_two_nodes_eq().
return true;
} else if (m_strutil.is_string(n1) && (!m_strutil.is_string(n2))) {
return check_length_const_string(n2, n1);
} else if (m_strutil.is_string(n2) && (!m_strutil.is_string(n1))) {
return check_length_const_string(n1, n2);
} else {
// n1 and n2 are vars or concats
return check_length_eq_var_concat(n1, n2);
}
return 0;
} }
void theory_str::check_concat_len_in_eqc(expr * concat) { void theory_str::check_concat_len_in_eqc(expr * concat) {

2
src/smt/theory_str.h
View file

@ -300,6 +300,8 @@ namespace smt {
bool can_concat_eq_concat(expr * concat1, expr * concat2); bool can_concat_eq_concat(expr * concat1, expr * concat2);
void check_concat_len_in_eqc(expr * concat); void check_concat_len_in_eqc(expr * concat);
bool check_length_consistency(expr * n1, expr * n2); bool check_length_consistency(expr * n1, expr * n2);
bool check_length_const_string(expr * n1, expr * constStr);
bool check_length_eq_var_concat(expr * n1, expr * n2);
void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList); void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
expr * simplify_concat(expr * node); expr * simplify_concat(expr * node);