Skip to content

Commit

Permalink
Z3str3 Debug (#6000)
Browse files Browse the repository at this point in the history 
* z3str3 debug

* add comments of reference to bugs in the report

Co-authored-by: John Lu <[email protected]>
  • Loading branch information
@JohnLyu2
JohnLyu2 and JohnLyu2 authored Apr 27, 2022
1 parent 99e299b commit 5a9b0dd
Show file tree
Hide file tree
Showing 2 changed files with 101 additions and 51 deletions.
147 changes: 98 additions & 49 deletions src/smt/theory_str.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,7 @@ namespace smt {
}

void theory_str::assert_axiom(expr * _e) {
if (_e == nullptr)
if (_e == nullptr)
return;
if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = true;
Expand Down Expand Up @@ -1100,9 +1100,10 @@ namespace smt {

TRACE("str", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;);

expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
expr_ref ts2(mk_str_var("ts2"), m);
// change subvaribale names to solve some invalide model problems
expr_ref ts0(mk_str_var("ch_ts0"), m);
expr_ref ts1(mk_str_var("ch_ts1"), m);
expr_ref ts2(mk_str_var("ch_ts2"), m);

expr_ref cond(m.mk_and(
m_autil.mk_ge(arg1, mk_int(0)),
Expand Down Expand Up @@ -1134,8 +1135,9 @@ namespace smt {

TRACE("str", tout << "instantiate prefixof axiom for " << mk_pp(expr, m) << std::endl;);

expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
// change subvaribale names to solve some invalide model problems
expr_ref ts0(mk_str_var("p_ts0"), m);
expr_ref ts1(mk_str_var("p_ts1"), m);

expr_ref_vector innerItems(m);
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
Expand Down Expand Up @@ -1170,8 +1172,9 @@ namespace smt {

TRACE("str", tout << "instantiate suffixof axiom for " << mk_pp(expr, m) << std::endl;);

expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
// change subvaribale names to solve some invalide model problems
expr_ref ts0(mk_str_var("s_ts0"), m);
expr_ref ts1(mk_str_var("s_ts1"), m);

expr_ref_vector innerItems(m);
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
Expand Down Expand Up @@ -1235,8 +1238,9 @@ namespace smt {

TRACE("str", tout << "instantiate Contains axiom for " << mk_pp(ex, m) << std::endl;);

expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
// change subvaribale names to solve some invalide model problems
expr_ref ts0(mk_str_var("c_ts0"), m);
expr_ref ts1(mk_str_var("c_ts1"), m);

expr_ref breakdownAssert(ctx.mk_eq_atom(ex, ctx.mk_eq_atom(ex->get_arg(0), mk_concat(ts0, mk_concat(ex->get_arg(1), ts1)))), m);
SASSERT(breakdownAssert);
Expand Down Expand Up @@ -1287,8 +1291,9 @@ namespace smt {

TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);

expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x1(mk_str_var("i_x1"), m);
expr_ref x2(mk_str_var("i_x2"), m);

expr_ref condAst1(mk_contains(exHaystack, exNeedle), m);
expr_ref condAst2(m.mk_not(ctx.mk_eq_atom(exNeedle, mk_string(""))), m);
Expand All @@ -1305,8 +1310,9 @@ namespace smt {
// args[0] = x3 . x4
// /\ |x3| = |x1| + |args[1]| - 1
// /\ ! contains(x3, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x3(mk_str_var("i_x3"), m);
expr_ref x4(mk_str_var("i_x4"), m);
expr_ref tmpLen(m_autil.mk_add(ex, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
SASSERT(tmpLen);
thenItems.push_back(ctx.mk_eq_atom(exHaystack, mk_concat(x3, x4)));
Expand Down Expand Up @@ -1501,8 +1507,9 @@ namespace smt {

TRACE("str", tout << "instantiate LastIndexof axiom for " << mk_pp(expr, m) << std::endl;);

expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x1(mk_str_var("li_x1"), m);
expr_ref x2(mk_str_var("li_x2"), m);
expr_ref indexAst(mk_int_var("index"), m);
expr_ref_vector items(m);

Expand Down Expand Up @@ -1532,8 +1539,9 @@ namespace smt {

if (!canSkip) {
// args[0] = x3 . x4 /\ |x3| = |x1| + 1 /\ ! contains(x4, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x3(mk_str_var("li_x3"), m);
expr_ref x4(mk_str_var("li_x4"), m);
expr_ref tmpLen(m_autil.mk_add(indexAst, mk_int(1)), m);
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
Expand Down Expand Up @@ -1690,10 +1698,11 @@ namespace smt {

TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(ex, m) << std::endl;);

expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x1(mk_str_var("rp_x1"), m);
expr_ref x2(mk_str_var("rp_x2"), m);
expr_ref i1(mk_int_var("i1"), m);
expr_ref result(mk_str_var("result"), m);
expr_ref result(mk_str_var("rp_result"), m);

expr * replaceS = nullptr;
expr * replaceT = nullptr;
Expand All @@ -1714,8 +1723,9 @@ namespace smt {
// i1 = |x1|
thenItems.push_back(ctx.mk_eq_atom(i1, mk_strlen(x1)));
// args[0] = x3 . x4 /\ |x3| = |x1| + |args[1]| - 1 /\ ! contains(x3, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
// change subvaribale names to solve some invalide model problems
expr_ref x3(mk_str_var("rp_x3"), m);
expr_ref x4(mk_str_var("rp_x4"), m);
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
Expand Down Expand Up @@ -1812,7 +1822,7 @@ namespace smt {
expr_ref zero(mk_string("0"), m);
// let (the result starts with a "0") be p
expr_ref starts_with_zero(u.str.mk_prefix(zero, ex), m);
// let (the result is "0") be q
// let (the result is "0") be q
expr_ref is_zero(ctx.mk_eq_atom(ex, zero), m);
// encoding: the result does NOT start with a "0" (~p) xor the result is "0" (q)
// ~p xor q == (~p or q) and (p or ~q)
Expand Down Expand Up @@ -1847,7 +1857,7 @@ namespace smt {
expr_ref axiom(ctx.mk_eq_atom(ex, rhs), m);
assert_axiom_rw(axiom);
}

void theory_str::instantiate_axiom_str_from_code(enode * e) {
ast_manager & m = get_manager();

Expand Down Expand Up @@ -3245,7 +3255,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
assert_implication(ax_l, m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
assert_implication(ax_l, new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}
}
} else if (splitType == 1) {
Expand Down Expand Up @@ -3303,7 +3317,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
assert_implication(ax_l, m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
assert_implication(ax_l, new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}

}
Expand Down Expand Up @@ -3355,7 +3373,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
arrangement_disjunction.push_back(new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}

}
Expand Down Expand Up @@ -3400,7 +3422,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
arrangement_disjunction.push_back(new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}

}
Expand Down Expand Up @@ -3641,7 +3667,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
assert_implication(ax_l, m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
assert_implication(ax_l, new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}

}
Expand Down Expand Up @@ -3742,7 +3772,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
arrangement_disjunction.push_back(new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}
}
}
Expand Down Expand Up @@ -4037,7 +4071,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
assert_implication(ax_l, m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
assert_implication(ax_l, new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}
}
}
Expand Down Expand Up @@ -4116,7 +4154,11 @@ namespace smt {

if (!overlapAssumptionUsed) {
overlapAssumptionUsed = true;
arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
arrangement_disjunction.push_back(new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
}
}
}
Expand Down Expand Up @@ -4513,7 +4555,11 @@ namespace smt {

// only add the overlap assumption one time
if (!overlapAssumptionUsed) {
arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term);
// add context dependent formula overlap predicate and relate it to the global overlap predicate
sort * s = get_manager().mk_bool_sort();
expr_ref new_OverlapAssumption_term = expr_ref(mk_fresh_const(newOverlapStr, s), get_manager());
arrangement_disjunction.push_back(new_OverlapAssumption_term);
assert_implication(new_OverlapAssumption_term, m_theoryStrOverlapAssumption_term);
overlapAssumptionUsed = true;
}

Expand Down Expand Up @@ -4577,7 +4623,7 @@ namespace smt {
u.str.is_string(strExpr, stringVal);
return true;
}

/*
* Look through the equivalence class of n to find a string constant.
* Return that constant if it is found, and set hasEqcValue to true.
Expand All @@ -4604,7 +4650,7 @@ namespace smt {
return a;
}
curr = m_find.next(curr);
}
}
while (curr != first && curr != null_theory_var);
}
hasEqcValue = false;
Expand Down Expand Up @@ -4781,10 +4827,13 @@ namespace smt {
//} else if (getNodeType(t, node) == my_Z3_Func) {
} else if (is_app(node)) {
app * func_app = to_app(node);
unsigned int argCount = func_app->get_num_args();
for (unsigned int i = 0; i < argCount; i++) {
expr * argAst = func_app->get_arg(i);
get_const_str_asts_in_node(argAst, astList);
// the following check is only valid when the operator is string concatenate
if (u.str.is_concat(func_app)) {
unsigned int argCount = func_app->get_num_args();
for (unsigned int i = 0; i < argCount; i++) {
expr * argAst = func_app->get_arg(i);
get_const_str_asts_in_node(argAst, astList);
}
}
}
}
Expand Down Expand Up @@ -6885,7 +6934,7 @@ namespace smt {
}

// heuristics

if (u.str.is_prefix(e)) {
check_consistency_prefix(e, is_true);
} else if (u.str.is_suffix(e)) {
Expand All @@ -6905,7 +6954,7 @@ namespace smt {

VERIFY(u.str.is_prefix(e, needle, haystack));
TRACE("str", tout << "check consistency of prefix predicate: " << mk_pp(needle, m) << " prefixof " << mk_pp(haystack, m) << std::endl;);

zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
Expand All @@ -6932,7 +6981,7 @@ namespace smt {

VERIFY(u.str.is_suffix(e, needle, haystack));
TRACE("str", tout << "check consistency of suffix predicate: " << mk_pp(needle, m) << " suffixof " << mk_pp(haystack, m) << std::endl;);

zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
Expand All @@ -6959,7 +7008,7 @@ namespace smt {

VERIFY(u.str.is_contains(e, haystack, needle)); // first string contains second one
TRACE("str", tout << "check consistency of contains predicate: " << mk_pp(haystack, m) << " contains " << mk_pp(needle, m) << std::endl;);

zstring needleStringConstant;
if (get_string_constant_eqc(needle, needleStringConstant)) {
if (u.str.is_itos(haystack) && is_true) {
Expand Down Expand Up @@ -7052,7 +7101,7 @@ namespace smt {
m_concat_eval_todo.reset();
m_delayed_axiom_setup_terms.reset();
m_delayed_assertions_todo.reset();

TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });

// list of expr* to remove from cut_var_map
Expand Down Expand Up @@ -8386,7 +8435,7 @@ namespace smt {
}
}
}

if (!needToAssignFreeVars) {

// check string-int terms
Expand Down Expand Up @@ -8685,7 +8734,7 @@ namespace smt {
} else if (u.str.is_itos(ex)) {
expr* fromInt = nullptr;
u.str.is_itos(ex, fromInt);

arith_value v(m);
v.init(&ctx);
rational val;
Expand Down Expand Up @@ -8808,7 +8857,7 @@ namespace smt {
if (!u.str.is_string(to_app(Gamma.get(left_count)))) {
rational offsetLen = offset - left_length + 1;
extra_left_cond = m_autil.mk_ge(u.str.mk_length(Gamma.get(left_count)), mk_int(offsetLen));
}
}

// find len(Delta[:j])
unsigned right_count = 0;
Expand Down Expand Up @@ -8887,7 +8936,7 @@ namespace smt {

expr* theory_str::refine_dis(expr* lhs, expr* rhs) {
ast_manager & m = get_manager();

expr_ref lesson(m);
lesson = m.mk_not(m.mk_eq(lhs, rhs));
TRACE("str", tout << "learning not " << mk_pp(lesson, m) << std::endl;);
Expand Down
Loading

0 comments on commit 5a9b0dd

Please sign in to comment.