From 5a9b0dd747a2fc26513fcb15181678781e6667a7 Mon Sep 17 00:00:00 2001 From: JohnLyu2 <65240623+JohnLyu2@users.noreply.github.com> Date: Wed, 27 Apr 2022 06:37:07 -0400 Subject: [PATCH] Z3str3 Debug (#6000) * z3str3 debug * add comments of reference to bugs in the report Co-authored-by: John Lu --- src/smt/theory_str.cpp | 147 +++++++++++++++++++++++++++-------------- src/smt/theory_str.h | 5 +- 2 files changed, 101 insertions(+), 51 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0b772f17d..8bd6c49aa 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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; @@ -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)), @@ -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))); @@ -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))); @@ -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); @@ -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); @@ -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))); @@ -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); @@ -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)); @@ -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; @@ -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)); @@ -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) @@ -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(); @@ -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) { @@ -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); } } @@ -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); } } @@ -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); } } @@ -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); } } @@ -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); } } } @@ -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); } } } @@ -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); } } } @@ -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; } @@ -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. @@ -4604,7 +4650,7 @@ namespace smt { return a; } curr = m_find.next(curr); - } + } while (curr != first && curr != null_theory_var); } hasEqcValue = false; @@ -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); + } } } } @@ -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)) { @@ -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) { @@ -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) { @@ -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) { @@ -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 @@ -8386,7 +8435,7 @@ namespace smt { } } } - + if (!needToAssignFreeVars) { // check string-int terms @@ -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; @@ -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; @@ -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;); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index d96a4e4af..090a5fe36 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -393,6 +393,8 @@ protected: // does not introduce equalities when they weren't enforced. unsigned m_unused_id; + const char* newOverlapStr = "!!NewOverlapAssumption!!"; + // terms we couldn't go through set_up_axioms() with because they weren't internalized expr_ref_vector m_delayed_axiom_setup_terms; @@ -492,7 +494,7 @@ protected: obj_map> fixed_length_lesson; //keep track of information for the lesson unsigned preprocessing_iteration_count; // number of attempts we've made to solve by preprocessing length information obj_map candidate_model; - + stats m_stats; protected: @@ -777,4 +779,3 @@ protected: }; }; -