mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

start work on string-integer integration

Browse source
This commit is contained in:
Murphy Berzish 2016-05-20 10:22:19 -04:00
parent 2f494a9611
commit 2522e35c5e
2 changed files with 35 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/smt/theory_str.cpp
View file

@ -2363,6 +2363,39 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
return n;
}
/*
* Look through the equivalence class of n to find an integer constant.
* Return that constant if it is found. Otherwise, return -1.
* Note that a return value of -1 should not normally be possible, as
* string length cannot be negative.
*/
rational theory_str::get_len_value(expr * n) {
ast_manager & m = get_manager();
context & ctx = get_context();
ctx.internalize(n, false);
TRACE("t_str_detail", tout << "checking eqc of " << mk_ismt2_pp(n, m) << " for an integer constant" << std::endl;);
enode * nNode = ctx.get_enode(n);
enode * eqcNode = nNode;
do {
app * ast = eqcNode->get_owner();
rational val;
bool is_int;
if (m_autil.is_numeral(n, val, is_int)) {
if (is_int) {
TRACE("t_str_detail", tout << "eqc contains integer constant " << val << std::endl;);
SASSERT(!val.is_neg());
return val;
}
}
} while (eqcNode != nNode);
// not found
TRACE("t_str_detail", tout << "eqc contains no integer constants" << std::endl;);
return rational(-1);
}
/*
* Decide whether n1 and n2 are already in the same equivalence class.
* This only checks whether the core considers them to be equal;

2
src/smt/theory_str.h
View file

@ -146,6 +146,8 @@ namespace smt {
expr * get_eqc_value(expr * n, bool & hasEqcValue);
bool in_same_eqc(expr * n1, expr * n2);
rational get_len_value(expr * n);
bool can_two_nodes_eq(expr * n1, expr * n2);
bool can_concat_eq_str(expr * concat, std::string str);
bool can_concat_eq_concat(expr * concat1, expr * concat2);