mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
detect and process concat eq type 1 (WIP UNTESTED)
This commit is contained in:
Murphy Berzish
parent
a62d15403e
commit
ed7b343822
2 changed files with 495 additions and 4 deletions
|
|
@ -28,7 +28,10 @@ theory_str::theory_str(ast_manager & m):
|
|||
search_started(false),
|
||||
m_autil(m),
|
||||
m_strutil(m),
|
||||
tmpXorVarCount(0)
|
||||
tmpStringVarCount(0),
|
||||
tmpXorVarCount(0),
|
||||
avoidLoopCut(true),
|
||||
loopDetected(false)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -101,6 +104,122 @@ bool theory_str::internalize_term(app * term) {
|
|||
return true;
|
||||
}
|
||||
|
||||
static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
|
||||
std::map<expr*, int>::iterator itor = src.begin();
|
||||
for (; itor != src.end(); itor++) {
|
||||
dest[itor->first] = 1;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
bool hasSelfCut(Z3_ast n1, Z3_ast n2) {
|
||||
if (cut_VARMap.find(n1) == cut_VARMap.end())
|
||||
return false;
|
||||
|
||||
if (cut_VARMap.find(n2) == cut_VARMap.end())
|
||||
return false;
|
||||
|
||||
if (cut_VARMap[n1].empty() || cut_VARMap[n2].empty())
|
||||
return false;
|
||||
|
||||
std::map<Z3_ast, int>::iterator itor = cut_VARMap[n1].top()->vars.begin();
|
||||
for (; itor != cut_VARMap[n1].top()->vars.end(); itor++) {
|
||||
if (cut_VARMap[n2].top()->vars.find(itor->first) != cut_VARMap[n2].top()->vars.end())
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
*/
|
||||
|
||||
bool theory_str::has_self_cut(expr * n1, expr * n2) {
|
||||
if (cut_var_map.find(n1) == cut_var_map.end()) {
|
||||
return false;
|
||||
}
|
||||
if (cut_var_map.find(n2) == cut_var_map.end()) {
|
||||
return false;
|
||||
}
|
||||
if (cut_var_map[n1].empty() || cut_var_map[n2].empty()) {
|
||||
return false;
|
||||
}
|
||||
|
||||
std::map<expr*, int>::iterator itor = cut_var_map[n1].top()->vars.begin();
|
||||
for (; itor != cut_var_map[n1].top()->vars.end(); ++itor) {
|
||||
if (cut_var_map[n2].top()->vars.find(itor->first) != cut_var_map[n2].top()->vars.end()) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::add_cut_info_one_node(expr * baseNode, int slevel, expr * node) {
|
||||
if (cut_var_map.find(baseNode) == cut_var_map.end()) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
} else {
|
||||
if (cut_var_map[baseNode].empty()) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
} else {
|
||||
if (cut_var_map[baseNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
} else if (cut_var_map[baseNode].top()->level == slevel) {
|
||||
cut_var_map[baseNode].top()->vars[node] = 1;
|
||||
} else {
|
||||
get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode) {
|
||||
if (cut_var_map.find(srcNode) == cut_var_map.end()) {
|
||||
get_manager().raise_exception("illegal state in add_cut_info_merge(): cut_var_map doesn't contain srcNode");
|
||||
}
|
||||
|
||||
if (cut_var_map[srcNode].empty()) {
|
||||
get_manager().raise_exception("illegal state in add_cut_info_merge(): cut_var_map[srcNode] is empty");
|
||||
}
|
||||
|
||||
if (cut_var_map.find(destNode) == cut_var_map.end()) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
cut_var_map[destNode].push(varInfo);
|
||||
} else {
|
||||
if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
cut_var_map[destNode].push(varInfo);
|
||||
} else if (cut_var_map[destNode].top()->level == slevel) {
|
||||
cut_vars_map_copy(cut_var_map[destNode].top()->vars, cut_var_map[srcNode].top()->vars);
|
||||
} else {
|
||||
get_manager().raise_exception("illegal state in add_cut_info_merge(): inconsistent slevels");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_str::check_and_init_cut_var(expr * node) {
|
||||
if (cut_var_map.find(node) != cut_var_map.end()) {
|
||||
return;
|
||||
} else if (!m_strutil.is_string(node)) {
|
||||
add_cut_info_one_node(node, -1, node);
|
||||
}
|
||||
}
|
||||
|
||||
app * theory_str::mk_int(int n) {
|
||||
return m_autil.mk_numeral(rational(n), true);
|
||||
}
|
||||
|
||||
app * theory_str::mk_internal_xor_var() {
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
|
@ -119,6 +238,49 @@ app * theory_str::mk_internal_xor_var() {
|
|||
return a;
|
||||
}
|
||||
|
||||
/*
|
||||
Z3_context ctx = Z3_theory_get_context(t);
|
||||
PATheoryData * td = (PATheoryData *) Z3_theory_get_ext_data(t);
|
||||
std::stringstream ss;
|
||||
ss << tmpStringVarCount;
|
||||
tmpStringVarCount++;
|
||||
std::string name = "$$_str" + ss.str();
|
||||
Z3_ast varAst = mk_var(ctx, name.c_str(), td->String);
|
||||
nonEmptyStrVarAxiom(t, varAst, __LINE__);
|
||||
return varAst;
|
||||
*/
|
||||
|
||||
app * theory_str::mk_nonempty_str_var() {
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
std::stringstream ss;
|
||||
ss << tmpStringVarCount;
|
||||
tmpStringVarCount++;
|
||||
std::string name = "$$_str" + ss.str();
|
||||
sort * string_sort = m.mk_sort(m_strutil.get_family_id(), STRING_SORT);
|
||||
char * new_buffer = alloc_svect(char, name.length() + 1);
|
||||
strcpy(new_buffer, name.c_str());
|
||||
symbol sym(new_buffer);
|
||||
|
||||
app* a = m.mk_const(m.mk_const_decl(sym, string_sort));
|
||||
// assert a variation of the basic string axioms that ensures this string is nonempty
|
||||
{
|
||||
// build LHS
|
||||
expr_ref len_str(m);
|
||||
len_str = mk_strlen(a);
|
||||
SASSERT(len_str);
|
||||
// build RHS
|
||||
expr_ref zero(m);
|
||||
zero = m_autil.mk_numeral(rational(0), true);
|
||||
SASSERT(zero);
|
||||
// build LHS > RHS and assert
|
||||
app * lhs_gt_rhs = m_autil.mk_gt(len_str, zero);
|
||||
SASSERT(lhs_gt_rhs);
|
||||
assert_axiom(lhs_gt_rhs);
|
||||
}
|
||||
return a;
|
||||
}
|
||||
|
||||
app * theory_str::mk_strlen(expr * e) {
|
||||
/*if (m_strutil.is_string(e)) {*/ if (false) {
|
||||
const char * strval = 0;
|
||||
|
|
@ -372,7 +534,7 @@ void theory_str::reset_eh() {
|
|||
m_basicstr_axiom_todo.reset();
|
||||
m_str_eq_todo.reset();
|
||||
m_concat_axiom_todo.reset();
|
||||
pop_scope_eh(0);
|
||||
pop_scope_eh(get_context().get_scope_level());
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
@ -670,9 +832,289 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) {
|
|||
}
|
||||
|
||||
// start to split both concats
|
||||
check_and_init_cut_var(v1_arg0);
|
||||
check_and_init_cut_var(v1_arg1);
|
||||
check_and_init_cut_var(v2_arg0);
|
||||
check_and_init_cut_var(v2_arg1);
|
||||
|
||||
//*************************************************************
|
||||
// case 1: concat(x, y) = concat(m, n)
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type1(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type1(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
|
||||
//*************************************************************
|
||||
// case 2: concat(x, y) = concat(m, "str")
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type2(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type2(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
|
||||
//*************************************************************
|
||||
// case 3: concat(x, y) = concat("str", n)
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type3(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type3(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
|
||||
//*************************************************************
|
||||
// case 4: concat("str1", y) = concat("str2", n)
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type4(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type4(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
|
||||
//*************************************************************
|
||||
// case 5: concat(x, "str1") = concat(m, "str2")
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type5(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type5(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
//*************************************************************
|
||||
// case 6: concat("str1", y) = concat(m, "str2")
|
||||
//*************************************************************
|
||||
if (is_concat_eq_type6(new_nn1, new_nn2)) {
|
||||
process_concat_eq_type6(new_nn1, new_nn2);
|
||||
return;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
expr * x = to_app(concatAst1)->get_arg(0);
|
||||
expr * y = to_app(concatAst1)->get_arg(1);
|
||||
expr * m = to_app(concatAst2)->get_arg(0);
|
||||
expr * n = to_app(concatAst2)->get_arg(1);
|
||||
|
||||
if (!m_strutil.is_string(x) && !m_strutil.is_string(y) && !m_strutil.is_string(m) && !m_strutil.is_string(n)) {
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
ast_manager & mgr = get_manager();
|
||||
context & ctx = get_context();
|
||||
TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl
|
||||
<< "concatAst1 = " << mk_ismt2_pp(concatAst1, m) << std::endl
|
||||
<< "concatAst2 = " << mk_ismt2_pp(concatAst2, m) << std::endl;
|
||||
);
|
||||
|
||||
if (!is_concat(to_app(concatAst1))) {
|
||||
TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;);
|
||||
return;
|
||||
}
|
||||
if (!is_concat(to_app(concatAst2))) {
|
||||
TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;);
|
||||
return;
|
||||
}
|
||||
expr * x = to_app(concatAst1)->get_arg(0);
|
||||
expr * y = to_app(concatAst1)->get_arg(1);
|
||||
expr * m = to_app(concatAst2)->get_arg(0);
|
||||
expr * n = to_app(concatAst2)->get_arg(1);
|
||||
|
||||
/* TODO query the integer theory:
|
||||
int x_len = getLenValue(t, x);
|
||||
int y_len = getLenValue(t, y);
|
||||
int m_len = getLenValue(t, m);
|
||||
int n_len = getLenValue(t, n);
|
||||
*/
|
||||
int x_len = -1;
|
||||
int y_len = -1;
|
||||
int m_len = -1;
|
||||
int n_len = -1;
|
||||
|
||||
int splitType = -1;
|
||||
if (x_len != -1 && m_len != -1) {
|
||||
if (x_len < m_len)
|
||||
splitType = 0;
|
||||
else if (x_len == m_len)
|
||||
splitType = 1;
|
||||
else
|
||||
splitType = 2;
|
||||
}
|
||||
|
||||
if (splitType == -1 && y_len != -1 && n_len != -1) {
|
||||
if (y_len > n_len)
|
||||
splitType = 0;
|
||||
else if (y_len == n_len)
|
||||
splitType = 1;
|
||||
else
|
||||
splitType = 2;
|
||||
}
|
||||
|
||||
TRACE("t_str_detail", tout << "split type " << splitType << std::endl;);
|
||||
|
||||
expr * t1 = NULL;
|
||||
expr * t2 = NULL;
|
||||
expr * xorFlag = NULL;
|
||||
|
||||
std::pair<expr*, expr*> key1(concatAst1, concatAst2);
|
||||
std::pair<expr*, expr*> key2(concatAst2, concatAst1);
|
||||
|
||||
if (varForBreakConcat.find(key1) == varForBreakConcat.end() && varForBreakConcat.find(key2) == varForBreakConcat.end()) {
|
||||
t1 = mk_nonempty_str_var();
|
||||
t2 = mk_nonempty_str_var();
|
||||
xorFlag = mk_internal_xor_var();
|
||||
check_and_init_cut_var(t1);
|
||||
check_and_init_cut_var(t2);
|
||||
varForBreakConcat[key1][0] = t1;
|
||||
varForBreakConcat[key1][1] = t2;
|
||||
varForBreakConcat[key1][2] = xorFlag;
|
||||
} else {
|
||||
// match found
|
||||
if (varForBreakConcat.find(key1) != varForBreakConcat.end()) {
|
||||
t1 = varForBreakConcat[key1][0];
|
||||
t2 = varForBreakConcat[key1][1];
|
||||
xorFlag = varForBreakConcat[key1][2];
|
||||
} else {
|
||||
t1 = varForBreakConcat[key2][0];
|
||||
t2 = varForBreakConcat[key2][1];
|
||||
xorFlag = varForBreakConcat[key2][2];
|
||||
}
|
||||
}
|
||||
|
||||
// For split types 0 through 2, we can get away with providing
|
||||
// fewer split options since more length information is available.
|
||||
if (splitType == 0) {
|
||||
NOT_IMPLEMENTED_YET(); // TODO
|
||||
} else if (splitType == 1) {
|
||||
NOT_IMPLEMENTED_YET(); // TODO
|
||||
} else if (splitType == 2) {
|
||||
NOT_IMPLEMENTED_YET(); // TODO
|
||||
} else if (splitType == -1) {
|
||||
// Here we don't really have a choice. We have no length information at all...
|
||||
expr ** or_item = alloc_svect(expr*, 3);
|
||||
expr ** and_item = alloc_svect(expr*, 20);
|
||||
int option = 0;
|
||||
int pos = 1;
|
||||
|
||||
// break option 1: m cuts y
|
||||
// len(x) < len(m) || len(y) > len(n)
|
||||
if (!avoidLoopCut || !has_self_cut(m, y)) {
|
||||
// break down option 1-1
|
||||
expr * x_t1 = mk_concat(x, t1);
|
||||
expr * t1_n = mk_concat(t1, n);
|
||||
or_item[option] = ctx.mk_eq_atom(xorFlag, mk_int(option));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(m, x_t1));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(y, t1_n));
|
||||
|
||||
expr_ref x_plus_t1(m_autil.mk_add(mk_strlen(x), mk_strlen(t1)), mgr);
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(m), x_plus_t1));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], m_autil.mk_gt(mk_strlen(m), mk_strlen(x)));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], m_autil.mk_gt(mk_strlen(y), mk_strlen(n)));
|
||||
|
||||
option++;
|
||||
|
||||
add_cut_info_merge(t1, ctx.get_scope_level(), m);
|
||||
add_cut_info_merge(t1, ctx.get_scope_level(), y);
|
||||
} else {
|
||||
loopDetected = true;
|
||||
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
|
||||
// TODO printCutVar(m, y);
|
||||
}
|
||||
|
||||
// break option 2:
|
||||
// x = m || y = n
|
||||
if (!avoidLoopCut || !has_self_cut(x, n)) {
|
||||
// break down option 1-2
|
||||
expr * m_t2 = mk_concat(m, t2);
|
||||
expr * t2_y = mk_concat(t2, y);
|
||||
or_item[option] = ctx.mk_eq_atom(xorFlag, mk_int(option));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(x, m_t2));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(n, t2_y));
|
||||
|
||||
|
||||
expr_ref m_plus_t2(m_autil.mk_add(mk_strlen(m), mk_strlen(t2)), mgr);
|
||||
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), m_plus_t2));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), mk_strlen(m)));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(n), mk_strlen(y)));
|
||||
|
||||
|
||||
option++;
|
||||
|
||||
add_cut_info_merge(t2, sLevel, x);
|
||||
add_cut_info_merge(t2, sLevel, n);
|
||||
} else {
|
||||
loopDetected = true;
|
||||
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
|
||||
// TODO printCutVar(x, n);
|
||||
}
|
||||
|
||||
if (can_two_nodes_eq(x, m) && can_two_nodes_eq(y, n)) {
|
||||
or_item[option] = ctx.mk_eq_atom(xorFlag, mk_int(option));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(x, m));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(y, n));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), mk_strlen(m)));
|
||||
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(y), mk_strlen(n)));
|
||||
++option;
|
||||
}
|
||||
|
||||
if (option > 0) {
|
||||
if (option == 1) {
|
||||
and_item[0] = or_item[0];
|
||||
} else {
|
||||
and_item[0] = mgr.mk_or(option, or_item);
|
||||
}
|
||||
expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), m);
|
||||
expr_ref conclusion(mgr.mk_and(pos, and_item), m);
|
||||
assert_implication(premise, conclusion);
|
||||
} else {
|
||||
TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;);
|
||||
}
|
||||
} // (splitType == -1)
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
|
||||
// TODO
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
|
||||
// TODO
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
|
||||
// TODO
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
|
||||
// TODO
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
|
||||
}
|
||||
|
||||
bool theory_str::is_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
|
||||
// TODO
|
||||
return false;
|
||||
}
|
||||
|
||||
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -1327,6 +1769,20 @@ void theory_str::push_scope_eh() {
|
|||
|
||||
void theory_str::pop_scope_eh(unsigned num_scopes) {
|
||||
TRACE("t_str", tout << "pop " << num_scopes << std::endl;);
|
||||
context & ctx = get_context();
|
||||
unsigned sLevel = ctx.get_scope_level();
|
||||
std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
|
||||
while (varItor != cut_var_map.end()) {
|
||||
while ((varItor->second.size() > 0) && (varItor->second.top()->level != 0) && (varItor->second.top()->level >= sLevel)) {
|
||||
T_cut * aCut = varItor->second.top();
|
||||
varItor->second.pop();
|
||||
dealloc(aCut);
|
||||
}
|
||||
if (varItor->second.size() == 0) {
|
||||
cut_var_map.erase(varItor);
|
||||
}
|
||||
++varItor;
|
||||
}
|
||||
}
|
||||
|
||||
final_check_status theory_str::final_check_eh() {
|
||||
|
|
|
|||
|
|
@ -47,7 +47,15 @@ namespace smt {
|
|||
};
|
||||
|
||||
class theory_str : public theory {
|
||||
// TODO
|
||||
struct T_cut
|
||||
{
|
||||
int level;
|
||||
std::map<expr*, int> vars;
|
||||
|
||||
T_cut() {
|
||||
level = -100;
|
||||
}
|
||||
};
|
||||
protected:
|
||||
bool search_started;
|
||||
arith_util m_autil;
|
||||
|
|
@ -59,8 +67,13 @@ namespace smt {
|
|||
svector<std::pair<enode*,enode*> > m_str_eq_todo;
|
||||
ptr_vector<enode> m_concat_axiom_todo;
|
||||
|
||||
int tmpStringVarCount;
|
||||
int tmpXorVarCount;
|
||||
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
|
||||
|
||||
bool avoidLoopCut = true;
|
||||
bool loopDetected = false;
|
||||
std::map<expr*, std::stack<T_cut *> > cut_var_map;
|
||||
protected:
|
||||
void assert_axiom(expr * e);
|
||||
void assert_implication(expr * premise, expr * conclusion);
|
||||
|
|
@ -69,6 +82,14 @@ namespace smt {
|
|||
expr * mk_concat(expr * n1, expr * n2);
|
||||
expr * mk_concat_const_str(expr * n1, expr * n2);
|
||||
|
||||
app * mk_int(int n);
|
||||
|
||||
void check_and_init_cut_var(expr * node);
|
||||
void add_cut_info_one_node(expr * baseNode, int slevel, expr * node);
|
||||
void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode);
|
||||
bool has_self_cut(expr * n1, expr * n2);
|
||||
|
||||
app * mk_nonempty_str_var();
|
||||
app * mk_internal_xor_var();
|
||||
|
||||
bool is_concat(app const * a) const { return a->is_app_of(get_id(), OP_STRCAT); }
|
||||
|
|
@ -98,6 +119,20 @@ namespace smt {
|
|||
void simplify_concat_equality(expr * lhs, expr * rhs);
|
||||
void solve_concat_eq_str(expr * concat, expr * str);
|
||||
|
||||
bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
|
||||
bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
|
||||
bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);
|
||||
bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2);
|
||||
bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2);
|
||||
bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2);
|
||||
|
||||
void process_concat_eq_type1(expr * concatAst1, expr * concatAst2);
|
||||
void process_concat_eq_type2(expr * concatAst1, expr * concatAst2);
|
||||
void process_concat_eq_type3(expr * concatAst1, expr * concatAst2);
|
||||
void process_concat_eq_type4(expr * concatAst1, expr * concatAst2);
|
||||
void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
|
||||
void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
|
||||
|
||||
bool new_eq_check(expr * lhs, expr * rhs);
|
||||
void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
|
||||
public:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue