From fd82daca2d14aeb0cc40dc77c78a9ec924c4abbd Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 5 May 2020 12:22:54 -0500 Subject: [PATCH 1/4] z3str3: remove legacy fixed-length overlap testing parameter smt.str.fixed_length_overlap_models has been deprecated --- src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_str_params.cpp | 1 - src/smt/params/theory_str_params.h | 8 - src/smt/theory_str.cpp | 328 +++++---------------------- src/smt/theory_str.h | 7 - 5 files changed, 54 insertions(+), 291 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 86db50e3ccc..7cad1a7fcbf 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -103,7 +103,6 @@ def_module_params(module_name='smt', ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'), ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), - ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'), ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'), ('str.regex_automata', BOOL, True, 'use automata-based reasoning for regular expressions (Z3str3 only)'), ('str.regex_automata_difficulty_threshold', UINT, 1000, 'difficulty threshold for regex automata heuristics'), diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index 1746f110965..41eda3c512b 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -27,7 +27,6 @@ void theory_str_params::updt_params(params_ref const & _p) { m_UseFastLengthTesterCache = p.str_fast_length_tester_cache(); m_UseFastValueTesterCache = p.str_fast_value_tester_cache(); m_StringConstantCache = p.str_string_constant_cache(); - m_FiniteOverlapModels = p.str_finite_overlap_models(); m_UseBinarySearch = p.str_use_binary_search(); m_BinarySearchInitialUpperBound = p.str_binary_search_start(); m_OverlapTheoryAwarePriority = p.str_overlap_priority(); diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 187f763401c..4b6c9bc81e7 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -68,13 +68,6 @@ struct theory_str_params { */ bool m_StringConstantCache; - /* - * If FiniteOverlapModels is set to true, - * arrangements that result in overlapping variables will generate a small number of models - * to test instead of completely giving up on the case. - */ - bool m_FiniteOverlapModels; - bool m_UseBinarySearch; unsigned m_BinarySearchInitialUpperBound; @@ -145,7 +138,6 @@ struct theory_str_params { m_UseFastLengthTesterCache(false), m_UseFastValueTesterCache(true), m_StringConstantCache(true), - m_FiniteOverlapModels(false), m_UseBinarySearch(false), m_BinarySearchInitialUpperBound(64), m_OverlapTheoryAwarePriority(-0.1), diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c203916c407..a539af8d98d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -168,8 +168,6 @@ namespace smt { binary_search_next_var_low.reset(); binary_search_next_var_high.reset(); - finite_model_test_varlists.reset(); - fixed_length_subterm_trail.reset(); fixed_length_assumptions.reset(); fixed_length_used_len_terms.reset(); @@ -3535,18 +3533,12 @@ namespace smt { } } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - assert_implication(ax_l, tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - assert_implication(ax_l, m_theoryStrOverlapAssumption_term); - } + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, m_theoryStrOverlapAssumption_term); } } } else if (splitType == 1) { @@ -3598,19 +3590,15 @@ namespace smt { } } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - assert_implication(ax_l, tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - assert_implication(ax_l, m_theoryStrOverlapAssumption_term); - } + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, m_theoryStrOverlapAssumption_term); } + } } else if (splitType == -1) { // Here we don't really have a choice. We have no length information at all... @@ -3654,19 +3642,15 @@ namespace smt { add_cut_info_merge(t1, ctx.get_scope_level(), y); } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - arrangement_disjunction.push_back(tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); - } + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); } + } // break option 2: @@ -3703,19 +3687,15 @@ namespace smt { add_cut_info_merge(t2, ctx.get_scope_level(), n); } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - arrangement_disjunction.push_back(tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); - } + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); + + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); } + } // option 3: @@ -3950,19 +3930,14 @@ namespace smt { } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - assert_implication(ax_l, tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIP" << std::endl;); - TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIP" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - assert_implication(ax_l, m_theoryStrOverlapAssumption_term); - } + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, m_theoryStrOverlapAssumption_term); } + } } } else if (splitType == 1) { @@ -4056,18 +4031,12 @@ namespace smt { add_cut_info_merge(temp1, ctx.get_scope_level(), m); } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - arrangement_disjunction.push_back(tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); - } + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); } } } @@ -4358,18 +4327,12 @@ namespace smt { } } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - assert_implication(ax_l, tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - assert_implication(ax_l, m_theoryStrOverlapAssumption_term); - } + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + assert_implication(ax_l, m_theoryStrOverlapAssumption_term); } } } @@ -4443,18 +4406,12 @@ namespace smt { add_cut_info_merge(temp1, sLevel, n); } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - arrangement_disjunction.push_back(tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); - TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); - if (!overlapAssumptionUsed) { - overlapAssumptionUsed = true; - arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); - } + if (!overlapAssumptionUsed) { + overlapAssumptionUsed = true; + arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); } } } @@ -4849,20 +4806,15 @@ namespace smt { } else { loopDetected = true; - if (m_params.m_FiniteOverlapModels) { - expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2); - arrangement_disjunction.push_back(tester); - add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); - } else { - TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); - TRACE("str", print_cut_var(m, tout); print_cut_var(y, tout);); + TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); + TRACE("str", print_cut_var(m, tout); print_cut_var(y, tout);); - // only add the overlap assumption one time - if (!overlapAssumptionUsed) { - arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); - overlapAssumptionUsed = true; - } + // only add the overlap assumption one time + if (!overlapAssumptionUsed) { + arrangement_disjunction.push_back(m_theoryStrOverlapAssumption_term); + overlapAssumptionUsed = true; } + } for (unsigned int overLen : overlapLen) { @@ -7155,168 +7107,6 @@ namespace smt { } } - expr_ref theory_str::set_up_finite_model_test(expr * lhs, expr * rhs) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - TRACE("str", tout << "activating finite model testing for overlapping concats " - << mk_pp(lhs, m) << " and " << mk_pp(rhs, m) << std::endl;); - std::map concatMap; - std::map unrollMap; - std::map varMap; - classify_ast_by_type(lhs, varMap, concatMap, unrollMap); - classify_ast_by_type(rhs, varMap, concatMap, unrollMap); - TRACE("str", tout << "found vars:"; - for (std::map::iterator it = varMap.begin(); it != varMap.end(); ++it) { - tout << " " << mk_pp(it->first, m); - } - tout << std::endl; - ); - - expr_ref testvar(mk_str_var("finiteModelTest"), m); - m_trail.push_back(testvar); - ptr_vector varlist; - - for (std::map::iterator it = varMap.begin(); it != varMap.end(); ++it) { - expr * v = it->first; - varlist.push_back(v); - } - - // make things easy for the core wrt. testvar - expr_ref t1(ctx.mk_eq_atom(testvar, mk_string("")), m); - expr_ref t_yes(ctx.mk_eq_atom(testvar, mk_string("yes")), m); - expr_ref testvaraxiom(m.mk_or(t1, t_yes), m); - assert_axiom(testvaraxiom); - - finite_model_test_varlists.insert(testvar, varlist); - m_trail_stack.push(insert_obj_map >(finite_model_test_varlists, testvar) ); - return t_yes; - } - - void theory_str::finite_model_test(expr * testvar, expr * str) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - zstring s; - if (!u.str.is_string(str, s)) return; - if (s == "yes") { - TRACE("str", tout << "start finite model test for " << mk_pp(testvar, m) << std::endl;); - ptr_vector & vars = finite_model_test_varlists[testvar]; - for (ptr_vector::iterator it = vars.begin(); it != vars.end(); ++it) { - expr * v = *it; - bool v_has_eqc = false; - get_eqc_value(v, v_has_eqc); - if (v_has_eqc) { - TRACE("str", tout << "variable " << mk_pp(v,m) << " already equivalent to a string constant" << std::endl;); - continue; - } - // check for any sort of existing length tester we might interfere with - if (m_params.m_UseBinarySearch) { - if (binary_search_len_tester_stack.contains(v) && !binary_search_len_tester_stack[v].empty()) { - TRACE("str", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); - continue; - } else { - // start binary search as normal - expr_ref implLhs(ctx.mk_eq_atom(testvar, str), m); - expr_ref implRhs(binary_search_length_test(v, nullptr, ""), m); - assert_implication(implLhs, implRhs); - } - } else { - bool map_effectively_empty = false; - if (!fvar_len_count_map.contains(v)) { - map_effectively_empty = true; - } - - if (!map_effectively_empty) { - map_effectively_empty = true; - if (fvar_lenTester_map.contains(v)) { - for (expr * indicator : fvar_lenTester_map[v]) { - if (internal_variable_set.contains(indicator)) { - map_effectively_empty = false; - break; - } - } - } - } - - if (map_effectively_empty) { - TRACE("str", tout << "no existing length testers for " << mk_pp(v, m) << std::endl;); - rational v_len; - rational v_lower_bound; - rational v_upper_bound; - expr_ref vLengthExpr(mk_strlen(v), m); - if (get_len_value(v, v_len)) { - TRACE("str", tout << "length = " << v_len.to_string() << std::endl;); - v_lower_bound = v_len; - v_upper_bound = v_len; - } else { - bool lower_bound_exists = lower_bound(vLengthExpr, v_lower_bound); - bool upper_bound_exists = upper_bound(vLengthExpr, v_upper_bound); - TRACE("str", tout << "bounds = [" << (lower_bound_exists?v_lower_bound.to_string():"?") - << ".." << (upper_bound_exists?v_upper_bound.to_string():"?") << "]" << std::endl;); - - // make sure the bounds are non-negative - if (lower_bound_exists && v_lower_bound.is_neg()) { - v_lower_bound = rational::zero(); - } - if (upper_bound_exists && v_upper_bound.is_neg()) { - v_upper_bound = rational::zero(); - } - - if (lower_bound_exists && upper_bound_exists) { - // easiest case. we will search within these bounds - } else if (upper_bound_exists && !lower_bound_exists) { - // search between 0 and the upper bound - v_lower_bound = rational::zero(); - } else if (lower_bound_exists && !upper_bound_exists) { - // check some finite portion of the search space - v_upper_bound = v_lower_bound + rational(10); - } else { - // no bounds information - v_lower_bound = rational::zero(); - v_upper_bound = v_lower_bound + rational(10); - } - } - // now create a fake length tester over this finite disjunction of lengths - - fvar_len_count_map.insert(v, 1); - unsigned int testNum = fvar_len_count_map[v]; - - expr_ref indicator(mk_internal_lenTest_var(v, testNum), m); - SASSERT(indicator); - m_trail.push_back(indicator); - - if (!fvar_lenTester_map.contains(v)) { - fvar_lenTester_map.insert(v, ptr_vector()); - } - fvar_lenTester_map[v].shrink(0); - fvar_lenTester_map[v].push_back(indicator); - lenTester_fvar_map.insert(indicator, v); - - expr_ref_vector orList(m); - expr_ref_vector andList(m); - - for (rational l = v_lower_bound; l <= v_upper_bound; l += rational::one()) { - zstring lStr = zstring(l.to_string().c_str()); - expr_ref str_indicator(mk_string(lStr), m); - expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); - orList.push_back(or_expr); - expr_ref and_expr(ctx.mk_eq_atom(or_expr, ctx.mk_eq_atom(vLengthExpr, m_autil.mk_numeral(l, true))), m); - andList.push_back(and_expr); - } - andList.push_back(mk_or(orList)); - expr_ref implLhs(ctx.mk_eq_atom(testvar, str), m); - expr_ref implRhs(mk_and(andList), m); - assert_implication(implLhs, implRhs); - } else { - TRACE("str", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); - continue; - } - } - } // foreach (v in vars) - } // (s == "yes") - } - void theory_str::handle_equality(expr * lhs, expr * rhs) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -7342,16 +7132,6 @@ namespace smt { return; } - /* // temporarily disabled, we are borrowing these testers for something else - if (m_params.m_FiniteOverlapModels && !finite_model_test_varlists.empty()) { - if (finite_model_test_varlists.contains(lhs)) { - finite_model_test(lhs, rhs); return; - } else if (finite_model_test_varlists.contains(rhs)) { - finite_model_test(rhs, lhs); return; - } - } - */ - if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) { return; } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 4b0eee5182b..24855ee7eeb 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -603,10 +603,6 @@ class theory_str : public theory { // maps a length tester to the next length tester to be (re)used if the split is "high" obj_map binary_search_next_var_high; - // finite model finding data - // maps a finite model tester var to a list of variables that will be tested - obj_map > finite_model_test_varlists; - // fixed length model construction expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver* expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these @@ -884,9 +880,6 @@ class theory_str : public theory { // TESTING void refresh_theory_var(expr * e); - expr_ref set_up_finite_model_test(expr * lhs, expr * rhs); - void finite_model_test(expr * v, expr * c); - public: theory_str(ast_manager & m, theory_str_params const & params); ~theory_str() override; From 1c817889bd0761753c5620429f9e3a7b5735247e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 5 May 2020 12:46:17 -0500 Subject: [PATCH 2/4] z3str3: remove legacy length/value testing algorithm and binary search heuristic the following parameters are deprecated: smt.str.use_binary_search smt.str.binary_search_start smt.str.fixed_length_models (the fixed-length model construction is now always used) --- src/smt/params/smt_params_helper.pyg | 3 - src/smt/params/theory_str_params.cpp | 6 - src/smt/params/theory_str_params.h | 13 - src/smt/theory_str.cpp | 82 +-- src/smt/theory_str.h | 21 - src/smt/theory_str_mc.cpp | 1025 -------------------------- 6 files changed, 4 insertions(+), 1146 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 7cad1a7fcbf..362de64843a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -100,8 +100,6 @@ def_module_params(module_name='smt', ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'), ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'), ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'), - ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'), - ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'), ('str.regex_automata', BOOL, True, 'use automata-based reasoning for regular expressions (Z3str3 only)'), @@ -110,7 +108,6 @@ def_module_params(module_name='smt', ('str.regex_automata_failed_automaton_threshold', UINT, 10, 'number of failed automaton construction attempts after which a full automaton is automatically built'), ('str.regex_automata_failed_intersection_threshold', UINT, 10, 'number of failed automaton intersection attempts after which intersection is always computed'), ('str.regex_automata_length_attempt_threshold', UINT, 10, 'number of length/path constraint attempts before checking unsatisfiability of regex terms'), - ('str.fixed_length_models', BOOL, True, 'use fixed-length equation solver to construct models (Z3str3 only)'), ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'), ('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index 41eda3c512b..1a13c60494d 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -27,8 +27,6 @@ void theory_str_params::updt_params(params_ref const & _p) { m_UseFastLengthTesterCache = p.str_fast_length_tester_cache(); m_UseFastValueTesterCache = p.str_fast_value_tester_cache(); m_StringConstantCache = p.str_string_constant_cache(); - m_UseBinarySearch = p.str_use_binary_search(); - m_BinarySearchInitialUpperBound = p.str_binary_search_start(); m_OverlapTheoryAwarePriority = p.str_overlap_priority(); m_RegexAutomata = p.str_regex_automata(); m_RegexAutomata_DifficultyThreshold = p.str_regex_automata_difficulty_threshold(); @@ -36,7 +34,6 @@ void theory_str_params::updt_params(params_ref const & _p) { m_RegexAutomata_FailedAutomatonThreshold = p.str_regex_automata_failed_automaton_threshold(); m_RegexAutomata_FailedIntersectionThreshold = p.str_regex_automata_failed_intersection_threshold(); m_RegexAutomata_LengthAttemptThreshold = p.str_regex_automata_length_attempt_threshold(); - m_FixedLengthModels = p.str_fixed_length_models(); m_FixedLengthRefinement = p.str_fixed_length_refinement(); m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex(); } @@ -51,8 +48,6 @@ void theory_str_params::display(std::ostream & out) const { DISPLAY_PARAM(m_UseFastLengthTesterCache); DISPLAY_PARAM(m_UseFastValueTesterCache); DISPLAY_PARAM(m_StringConstantCache); - DISPLAY_PARAM(m_UseBinarySearch); - DISPLAY_PARAM(m_BinarySearchInitialUpperBound); DISPLAY_PARAM(m_OverlapTheoryAwarePriority); DISPLAY_PARAM(m_RegexAutomata); DISPLAY_PARAM(m_RegexAutomata_DifficultyThreshold); @@ -60,6 +55,5 @@ void theory_str_params::display(std::ostream & out) const { DISPLAY_PARAM(m_RegexAutomata_FailedAutomatonThreshold); DISPLAY_PARAM(m_RegexAutomata_FailedIntersectionThreshold); DISPLAY_PARAM(m_RegexAutomata_LengthAttemptThreshold); - DISPLAY_PARAM(m_FixedLengthModels); DISPLAY_PARAM(m_FixedLengthNaiveCounterexamples); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 4b6c9bc81e7..f293d3f0a40 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -68,9 +68,6 @@ struct theory_str_params { */ bool m_StringConstantCache; - bool m_UseBinarySearch; - unsigned m_BinarySearchInitialUpperBound; - double m_OverlapTheoryAwarePriority; /* @@ -109,13 +106,6 @@ struct theory_str_params { * before which we begin checking unsatisfiability of a regex term. */ unsigned m_RegexAutomata_LengthAttemptThreshold; - - /* - * If FixedLengthModels is true, Z3str3 will use a fixed-length equation solver to construct models in final_check. - * If false, Z3str3 will use the legacy length tester and value tester procedure. - */ - bool m_FixedLengthModels; - /* * If FixedLengthRefinement is true and the fixed-length equation solver is enabled, * Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive @@ -138,8 +128,6 @@ struct theory_str_params { m_UseFastLengthTesterCache(false), m_UseFastValueTesterCache(true), m_StringConstantCache(true), - m_UseBinarySearch(false), - m_BinarySearchInitialUpperBound(64), m_OverlapTheoryAwarePriority(-0.1), m_RegexAutomata(true), m_RegexAutomata_DifficultyThreshold(1000), @@ -147,7 +135,6 @@ struct theory_str_params { m_RegexAutomata_FailedAutomatonThreshold(10), m_RegexAutomata_FailedIntersectionThreshold(10), m_RegexAutomata_LengthAttemptThreshold(10), - m_FixedLengthModels(true), m_FixedLengthRefinement(false), m_FixedLengthNaiveCounterexamples(true) { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a539af8d98d..0bc5d8eb136 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -562,31 +562,6 @@ namespace smt { return m_autil.mk_numeral(q, true); } - expr * theory_str::mk_internal_lenTest_var(expr * node, int lTries) { - ast_manager & m = get_manager(); - - std::stringstream ss; - ss << "$$_len_" << mk_ismt2_pp(node, m) << "_" << lTries << "_" << tmpLenTestVarCount; - tmpLenTestVarCount += 1; - std::string name = ss.str(); - app * var = mk_str_var(name); - internal_lenTest_vars.insert(var); - m_trail.push_back(var); - return var; - } - - expr * theory_str::mk_internal_valTest_var(expr * node, int len, int vTries) { - ast_manager & m = get_manager(); - std::stringstream ss; - ss << "$$_val_" << mk_ismt2_pp(node, m) << "_" << len << "_" << vTries << "_" << tmpValTestVarCount; - tmpValTestVarCount += 1; - std::string name = ss.str(); - app * var = mk_str_var(name); - internal_valTest_vars.insert(var); - m_trail.push_back(var); - return var; - } - void theory_str::track_variable_scope(expr * var) { if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) { internal_variable_scope_levels[sLevel] = obj_hashtable(); @@ -7132,10 +7107,6 @@ namespace smt { return; } - if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) { - return; - } - if (u.str.is_concat(to_app(lhs)) && u.str.is_concat(to_app(rhs))) { bool nn1HasEqcValue = false; bool nn2HasEqcValue = false; @@ -9301,7 +9272,7 @@ namespace smt { } } - if (m_params.m_FixedLengthModels) { + { // TODO if we're using fixed-length testing, do we care about finding free variables any more? // that work might be useless TRACE("str", tout << "using fixed-length model construction" << std::endl;); @@ -9336,49 +9307,6 @@ namespace smt { TRACE("str", tout << "fixed-length model construction found missing side conditions; continuing search" << std::endl;); return FC_CONTINUE; } - } else { - // Legacy (Z3str2) length+value testing - - // -------- - // experimental free variable assignment - begin - // * special handling for variables that are not used in concat - // -------- - bool testAssign = true; - if (!testAssign) { - for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { - expr * freeVar = fvIt->first; - /* - std::string vName = std::string(Z3_ast_to_string(ctx, freeVar)); - if (vName.length() >= 9 && vName.substr(0, 9) == "$$_regVar") { - continue; - } - */ - expr * toAssert = gen_len_val_options_for_free_var(freeVar, nullptr, ""); - if (toAssert != nullptr) { - assert_axiom(toAssert); - } - } - } else { - process_free_var(freeVar_map); - } - // experimental free variable assignment - end - - // now deal with removed free variables that are bounded by an unroll - TRACE("str", tout << "fv_unrolls_map (#" << fv_unrolls_map.size() << "):" << std::endl;); - for (std::map >::iterator fvIt1 = fv_unrolls_map.begin(); - fvIt1 != fv_unrolls_map.end(); fvIt1++) { - expr * var = fvIt1->first; - fSimpUnroll.clear(); - get_eqc_simpleUnroll(var, constValue, fSimpUnroll); - if (fSimpUnroll.size() == 0) { - gen_assign_unroll_reg(fv_unrolls_map[var]); - } else { - expr * toAssert = gen_assign_unroll_Str2Reg(var, fSimpUnroll); - if (toAssert != nullptr) { - assert_axiom(toAssert); - } - } - } } if (opt_VerifyFinalCheckProgress && !finalCheckProgressIndicator) { @@ -9508,11 +9436,9 @@ namespace smt { } } - if (m_params.m_FixedLengthModels) { - zstring assignedValue; - if (candidate_model.find(n, assignedValue)) { - return to_app(mk_string(assignedValue)); - } + zstring assignedValue; + if (candidate_model.find(n, assignedValue)) { + return to_app(mk_string(assignedValue)); } // fallback path diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 24855ee7eeb..d41de45bfb8 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -653,7 +653,6 @@ class theory_str : public theory { app * mk_int_var(std::string name); app_ref mk_nonempty_str_var(); app * mk_internal_xor_var(); - expr * mk_internal_valTest_var(expr * node, int len, int vTries); app * mk_regex_rep_var(); app * mk_unroll_bound_var(); app * mk_unroll_test_var(); @@ -808,26 +807,6 @@ class theory_str : public theory { void classify_ast_by_type_in_positive_context(std::map & varMap, std::map & concatMap, std::map & unrollMap); - expr * mk_internal_lenTest_var(expr * node, int lTries); - expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue); - void process_free_var(std::map & freeVar_map); - expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); - expr * gen_free_var_options(expr * freeVar, expr * len_indicator, - zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr); - expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, - zstring lenStr, int tries); - void print_value_tester_list(svector > & testerList); - bool get_next_val_encode(int_vector & base, int_vector & next); - zstring gen_val_string(int len, int_vector & encoding); - - // binary search heuristic - expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue); - expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits); - - bool free_var_attempt(expr * nn1, expr * nn2); - void more_len_tests(expr * lenTester, zstring lenTesterValue); - void more_value_tests(expr * valTester, zstring valTesterValue); - expr * get_alias_index_ast(std::map & aliasIndexMap, expr * node); expr * getMostLeftNodeInConcat(expr * node); expr * getMostRightNodeInConcat(expr * node); diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 5f1c48c212b..ffe55a4d00c 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -1214,1003 +1214,6 @@ namespace smt { } } - expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tries) { - ast_manager & m = get_manager(); - context & ctx = get_context(); - - expr_ref freeVarLen(mk_strlen(freeVar), m); - SASSERT(freeVarLen); - - { - rational freeVar_len_value; - if (get_len_value(freeVar, freeVar_len_value)) { - TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); - expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m); - expr_ref concreteValue(ctx.mk_eq_atom( - ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), - ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m); - expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m); - SASSERT(finalAxiom); - m_trail.push_back(finalAxiom); - return finalAxiom; - } - } - - expr_ref_vector orList(m); - expr_ref_vector andList(m); - - int distance = 3; - int l = (tries - 1) * distance; - int h = tries * distance; - - TRACE("str", - tout << "building andList and orList" << std::endl; - if (m_params.m_AggressiveLengthTesting) { - tout << "note: aggressive length testing is active" << std::endl; - } - ); - - // experimental theory-aware case split support - literal_vector case_split_literals; - - for (int i = l; i < h; ++i) { - expr_ref str_indicator(m); - if (m_params.m_UseFastLengthTesterCache) { - rational ri(i); - expr * lookup_val; - if(lengthTesterCache.find(ri, lookup_val)) { - str_indicator = expr_ref(lookup_val, m); - } else { - // no match; create and insert - zstring i_str = int_to_string(i); - expr_ref new_val(mk_string(i_str), m); - lengthTesterCache.insert(ri, new_val); - m_trail.push_back(new_val); - str_indicator = expr_ref(new_val, m); - } - } else { - zstring i_str = int_to_string(i); - str_indicator = expr_ref(mk_string(i_str), m); - } - expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); - orList.push_back(or_expr); - - double priority; - // give high priority to small lengths if this is available - if (i <= 5) { - priority = 0.3; - } else { - // prioritize over "more" - priority = 0.2; - } - add_theory_aware_branching_info(or_expr, priority, l_true); - - if (m_params.m_AggressiveLengthTesting) { - literal l = mk_eq(indicator, str_indicator, false); - ctx.mark_as_relevant(l); - ctx.force_phase(l); - } - - case_split_literals.insert(mk_eq(freeVarLen, mk_int(i), false)); - - expr_ref and_expr(ctx.mk_eq_atom(orList.get(orList.size() - 1), m.mk_eq(freeVarLen, mk_int(i))), m); - andList.push_back(and_expr); - } - - expr_ref more_option(ctx.mk_eq_atom(indicator, mk_string("more")), m); - orList.push_back(more_option); - // decrease priority of this option - add_theory_aware_branching_info(more_option, -0.1, l_true); - if (m_params.m_AggressiveLengthTesting) { - literal l = mk_eq(indicator, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - - andList.push_back(ctx.mk_eq_atom(orList.get(orList.size() - 1), m_autil.mk_ge(freeVarLen, mk_int(h)))); - - /* - { // more experimental theory case split support - expr_ref tmp(m_autil.mk_ge(freeVarLen, mk_int(h)), m); - ctx.internalize(m_autil.mk_ge(freeVarLen, mk_int(h)), false); - case_split_literals.push_back(ctx.get_literal(tmp)); - ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - } - */ - - expr_ref_vector or_items(m); - expr_ref_vector and_items(m); - - for (unsigned i = 0; i < orList.size(); ++i) { - or_items.push_back(orList.get(i)); - } - - and_items.push_back(mk_or(or_items)); - for(unsigned i = 0; i < andList.size(); ++i) { - and_items.push_back(andList.get(i)); - } - - TRACE("str", tout << "check: " << mk_pp(mk_and(and_items), m) << std::endl;); - - expr_ref lenTestAssert = mk_and(and_items); - SASSERT(lenTestAssert); - TRACE("str", tout << "crash avoidance lenTestAssert: " << mk_pp(lenTestAssert, m) << std::endl;); - - int testerCount = tries - 1; - if (testerCount > 0) { - expr_ref_vector and_items_LHS(m); - expr_ref moreAst(mk_string("more"), m); - for (int i = 0; i < testerCount; ++i) { - expr * indicator = fvar_lenTester_map[freeVar][i]; - if (internal_variable_set.find(indicator) == internal_variable_set.end()) { - TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " out of scope; continuing" << std::endl;); - continue; - } else { - TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " in scope" << std::endl;); - and_items_LHS.push_back(ctx.mk_eq_atom(indicator, moreAst)); - } - } - expr_ref assertL(mk_and(and_items_LHS), m); - SASSERT(assertL); - expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get()); - SASSERT(finalAxiom != nullptr); - TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;); - return finalAxiom; - } else { - TRACE("str", tout << "crash avoidance lenTestAssert.get(): " << mk_pp(lenTestAssert.get(), m) << std::endl;); - m_trail.push_back(lenTestAssert.get()); - return lenTestAssert.get(); - } - } - - /* - * The return value indicates whether we covered the search space. - * - If the next encoding is valid, return false - * - Otherwise, return true - */ - bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { - SASSERT(charSetSize > 0); - - TRACE("str", tout << "base vector: [ "; - for (unsigned i = 0; i < base.size(); ++i) { - tout << base[i] << " "; - } - tout << "]" << std::endl; - ); - - int s = 0; - int carry = 0; - next.reset(); - - for (int i = 0; i < (int) base.size(); i++) { - if (i == 0) { - s = base[i] + 1; - carry = s / charSetSize; - s = s % charSetSize; - next.push_back(s); - } else { - s = base[i] + carry; - carry = s / charSetSize; - s = s % charSetSize; - next.push_back(s); - } - } - if (next[next.size() - 1] > 0) { - next.reset(); - return true; - } else { - return false; - } - } - - expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, - zstring lenStr, int tries) { - ast_manager & m = get_manager(); - context & ctx = get_context(); - - int distance = 32; - - // ---------------------------------------------------------------------------------------- - // generate value options encoding - // encoding is a vector of size (len + 1) - // e.g, len = 2, - // encoding {1, 2, 0} means the value option is "charSet[2]"."charSet[1]" - // the last item in the encoding indicates whether the whole space is covered - // for example, if the charSet = {a, b}. All valid encodings are - // {0, 0, 0}, {1, 0, 0}, {0, 1, 0}, {1, 1, 0} - // if add 1 to the last one, we get - // {0, 0, 1} - // the last item "1" shows this is not a valid encoding, and we have covered all space - // ---------------------------------------------------------------------------------------- - int len = atoi(lenStr.encode().c_str()); - bool coverAll = false; - vector options; - int_vector base; - - TRACE("str", tout - << "freeVar = " << mk_ismt2_pp(freeVar, m) << std::endl - << "len_indicator = " << mk_ismt2_pp(len_indicator, m) << std::endl - << "val_indicator = " << mk_ismt2_pp(val_indicator, m) << std::endl - << "lenstr = " << lenStr << "\n" - << "tries = " << tries << "\n"; - if (m_params.m_AggressiveValueTesting) { - tout << "note: aggressive value testing is enabled" << std::endl; - } - ); - - if (tries == 0) { - base = int_vector(len + 1, 0); - coverAll = false; - } else { - expr * lastestValIndi = fvar_valueTester_map[freeVar][len][tries - 1].second; - TRACE("str", tout << "last value tester = " << mk_ismt2_pp(lastestValIndi, m) << std::endl;); - coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); - } - - size_t l = (tries) * distance; - size_t h = l; - for (int i = 0; i < distance; i++) { - if (coverAll) - break; - options.push_back(base); - h++; - coverAll = get_next_val_encode(options[options.size() - 1], base); - } - val_range_map.insert(val_indicator, options[options.size() - 1]); - - TRACE("str", - tout << "value tester encoding " << "{" << std::endl; - int_vector vec = val_range_map[val_indicator]; - - for (int_vector::iterator it = vec.begin(); it != vec.end(); ++it) { - tout << *it << std::endl; - } - tout << "}" << std::endl; - ); - - // ---------------------------------------------------------------------------------------- - - expr_ref_vector orList(m), andList(m); - - for (size_t i = l; i < h; i++) { - orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); - if (m_params.m_AggressiveValueTesting) { - literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); - ctx.mark_as_relevant(lit); - ctx.force_phase(lit); - } - - zstring aStr = gen_val_string(len, options[i - l]); - expr * strAst; - if (m_params.m_UseFastValueTesterCache) { - if (!valueTesterCache.find(aStr, strAst)) { - strAst = mk_string(aStr); - valueTesterCache.insert(aStr, strAst); - m_trail.push_back(strAst); - } - } else { - strAst = mk_string(aStr); - } - andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); - } - if (!coverAll) { - orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); - if (m_params.m_AggressiveValueTesting) { - literal l = mk_eq(val_indicator, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - } - - andList.push_back(mk_or(orList)); - expr_ref valTestAssert = mk_and(andList); - - // --------------------------------------- - // If the new value tester is $$_val_x_16_i - // Should add ($$_len_x_j = 16) /\ ($$_val_x_16_i = "more") - // --------------------------------------- - andList.reset(); - andList.push_back(m.mk_eq(len_indicator, mk_string(lenStr))); - for (int i = 0; i < tries; i++) { - expr * vTester = fvar_valueTester_map[freeVar][len][i].second; - if (vTester != val_indicator) - andList.push_back(m.mk_eq(vTester, mk_string("more"))); - } - expr_ref assertL = mk_and(andList); - // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) - return m.mk_or(m.mk_not(assertL), valTestAssert); - } - - // ----------------------------------------------------------------------------------------------------- - // True branch will be taken in final_check: - // - When we discover a variable is "free" for the first time - // lenTesterInCbEq = NULL - // lenTesterValue = "" - // False branch will be taken when invoked by new_eq_eh(). - // - After we set up length tester for a "free" var in final_check, - // when the tester is assigned to some value (e.g. "more" or "4"), - // lenTesterInCbEq != NULL, and its value will be passed by lenTesterValue - // The difference is that in new_eq_eh(), lenTesterInCbEq and its value have NOT been put into a same eqc - // ----------------------------------------------------------------------------------------------------- - expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { - - ast_manager & m = get_manager(); - - TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); - - if (m_params.m_UseBinarySearch) { - TRACE("str", tout << "using binary search heuristic" << std::endl;); - return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); - } else { - bool map_effectively_empty = false; - if (!fvar_len_count_map.contains(freeVar)) { - TRACE("str", tout << "fvar_len_count_map is empty" << std::endl;); - map_effectively_empty = true; - } - - if (!map_effectively_empty) { - // check whether any entries correspond to variables that went out of scope; - // if every entry is out of scope then the map counts as being empty - - // assume empty and find a counterexample - map_effectively_empty = true; - if (fvar_lenTester_map.contains(freeVar)) { - for (expr * indicator : fvar_lenTester_map[freeVar]) { - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { - TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) - << " in fvar_lenTester_map[freeVar]" << std::endl;); - map_effectively_empty = false; - break; - } - } - } - CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); - } - - if (map_effectively_empty) { - // no length assertions for this free variable have ever been added. - TRACE("str", tout << "no length assertions yet" << std::endl;); - - fvar_len_count_map.insert(freeVar, 1); - unsigned int testNum = fvar_len_count_map[freeVar]; - - expr_ref indicator(mk_internal_lenTest_var(freeVar, testNum), m); - SASSERT(indicator); - - // since the map is "effectively empty", we can remove those variables that have left scope... - if (!fvar_lenTester_map.contains(freeVar)) { - fvar_lenTester_map.insert(freeVar, ptr_vector()); - } - fvar_lenTester_map[freeVar].shrink(0); - fvar_lenTester_map[freeVar].push_back(indicator); - lenTester_fvar_map.insert(indicator, freeVar); - - expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); - SASSERT(lenTestAssert != nullptr); - return lenTestAssert; - } else { - TRACE("str", tout << "found previous in-scope length assertions" << std::endl;); - - expr * effectiveLenInd = nullptr; - zstring effectiveLenIndiStr(""); - int lenTesterCount; - if (fvar_lenTester_map.contains(freeVar)) { - lenTesterCount = fvar_lenTester_map[freeVar].size(); - } else { - lenTesterCount = 0; - } - - TRACE("str", - tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl; - for (int i = 0; i < lenTesterCount; ++i) { - expr * len_indicator = fvar_lenTester_map[freeVar][i]; - tout << mk_pp(len_indicator, m) << ": "; - bool effectiveInScope = (internal_variable_set.find(len_indicator) != internal_variable_set.end()); - tout << (effectiveInScope ? "in scope" : "NOT in scope"); - tout << std::endl; - } - ); - - int i = 0; - for (; i < lenTesterCount; ++i) { - expr * len_indicator_pre = fvar_lenTester_map[freeVar][i]; - // check whether this is in scope as well - if (internal_variable_set.find(len_indicator_pre) == internal_variable_set.end()) { - TRACE("str", tout << "length indicator " << mk_pp(len_indicator_pre, m) << " not in scope" << std::endl;); - continue; - } - - bool indicatorHasEqcValue = false; - expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); - TRACE("str", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << - " = " << mk_ismt2_pp(len_indicator_value, m) << std::endl;); - if (indicatorHasEqcValue) { - zstring len_pIndiStr; - u.str.is_string(len_indicator_value, len_pIndiStr); - // NSB: is len_indicator_value always a string? Then use VERIFY, or otherwise test return value - if (len_pIndiStr != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = len_pIndiStr; - break; - } - } else { - if (lenTesterInCbEq != len_indicator_pre) { - TRACE("str", tout << "WARNING: length indicator " << mk_ismt2_pp(len_indicator_pre, m) - << " does not have an equivalence class value." - << " i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); - if (i > 0) { - effectiveLenInd = fvar_lenTester_map[freeVar][i - 1]; - bool effectiveHasEqcValue; - expr * effective_eqc_value = get_eqc_value(effectiveLenInd, effectiveHasEqcValue); - bool effectiveInScope = (internal_variable_set.find(effectiveLenInd) != internal_variable_set.end()); - TRACE("str", tout << "checking effective length indicator " << mk_pp(effectiveLenInd, m) << ": " - << (effectiveInScope ? "in scope" : "NOT in scope") << ", "; - if (effectiveHasEqcValue) { - tout << "~= " << mk_pp(effective_eqc_value, m); - } else { - tout << "no eqc string constant"; - } - tout << std::endl;); (void)effectiveInScope; - if (effectiveLenInd == lenTesterInCbEq) { - effectiveLenIndiStr = lenTesterValue; - } else { - if (effectiveHasEqcValue) { - u.str.is_string(effective_eqc_value, effectiveLenIndiStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - } else { - NOT_IMPLEMENTED_YET(); - } - } - } - break; - } - // lenTesterInCbEq == len_indicator_pre - else { - if (lenTesterValue != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = lenTesterValue; - break; - } - } - } // !indicatorHasEqcValue - } // for (i : [0..lenTesterCount-1]) - if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "") { - TRACE("str", tout << "length is not fixed; generating length tester options for free var" << std::endl;); - expr_ref indicator(m); - unsigned int testNum = 0; - - TRACE("str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr - << ", i = " << i << ", lenTesterCount = " << lenTesterCount << "\n";); - - if (i == lenTesterCount) { - fvar_len_count_map[freeVar] = fvar_len_count_map[freeVar] + 1; - testNum = fvar_len_count_map[freeVar]; - indicator = mk_internal_lenTest_var(freeVar, testNum); - fvar_lenTester_map[freeVar].push_back(indicator); - lenTester_fvar_map.insert(indicator, freeVar); - } else { - indicator = fvar_lenTester_map[freeVar][i]; - refresh_theory_var(indicator); - testNum = i + 1; - } - expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum); - SASSERT(lenTestAssert != nullptr); - return lenTestAssert; - } else { - // if we are performing automata-based reasoning and the term associated with - // this length tester is in any way constrained by regex terms, - // do not perform value testing -- this term is not a free variable. - if (m_params.m_RegexAutomata) { - std::map, expr*>::iterator it = regex_in_bool_map.begin(); - for (; it != regex_in_bool_map.end(); ++it) { - expr * re = it->second; - expr * re_str = to_app(re)->get_arg(0); - // recursive descent through all subterms of re_str to see if any of them are - // - the same as freeVar - // - in the same EQC as freeVar - if (term_appears_as_subterm(freeVar, re_str)) { - TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;); - return nullptr; - } - } - } - - TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); - // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, nullptr, zstring("")); - return valueAssert; - } - } // fVarLenCountMap.find(...) - - } // !UseBinarySearch - } - - expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, - zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr) { - ast_manager & m = get_manager(); - - int len = atoi(len_valueStr.encode().c_str()); - - // check whether any value tester is actually in scope - TRACE("str", tout << "checking scope of previous value testers" << std::endl;); - bool map_effectively_empty = true; - if (fvar_valueTester_map.contains(freeVar) && - fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { - // there's *something* in the map, but check its scope - for (auto const& entry : fvar_valueTester_map[freeVar][len]) { - expr * aTester = entry.second; - if (!internal_variable_set.contains(aTester)) { - TRACE("str", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); - } else { - TRACE("str", tout << mk_pp(aTester, m) << " in scope" << std::endl;); - map_effectively_empty = false; - break; - } - } - } - - if (map_effectively_empty) { - TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;); - int tries = 0; - expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); - valueTester_fvar_map.insert(val_indicator, freeVar); - if (!fvar_valueTester_map.contains(freeVar)) { - fvar_valueTester_map.insert(freeVar, std::map > >()); - } - fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator)); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); - } else { - TRACE("str", tout << "checking previous value testers" << std::endl;); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - - // go through all previous value testers - // If some doesn't have an eqc value, add its assertion again. - int testerTotal = fvar_valueTester_map[freeVar][len].size(); - int i = 0; - for (; i < testerTotal; i++) { - expr * aTester = fvar_valueTester_map[freeVar][len][i].second; - - // it's probably worth checking scope here, actually - if (!internal_variable_set.contains(aTester)) { - TRACE("str", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); - continue; - } - - if (aTester == valTesterInCbEq) { - break; - } - - bool anEqcHasValue = false; - get_eqc_value(aTester, anEqcHasValue); - if (!anEqcHasValue) { - TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - << " doesn't have an equivalence class value." << std::endl;); - refresh_theory_var(aTester); - - expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); - - TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl - << mk_ismt2_pp(makeupAssert, m) << std::endl;); - assert_axiom(makeupAssert); - } else { - // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); - } - } - - if (valTesterValueStr == "more") { - expr * valTester = nullptr; - if (i + 1 < testerTotal) { - valTester = fvar_valueTester_map[freeVar][len][i + 1].second; - refresh_theory_var(valTester); - } else { - valTester = mk_internal_valTest_var(freeVar, len, i + 1); - valueTester_fvar_map.insert(valTester, freeVar); - fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); - print_value_tester_list(fvar_valueTester_map[freeVar][len]); - } - return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); - } - - return nullptr; - } - } - - void theory_str::process_free_var(std::map & freeVar_map) { - context & ctx = get_context(); - - obj_hashtable eqcRepSet; - obj_hashtable leafVarSet; - std::map > aloneVars; - - for (auto const& kv : freeVar_map) { - expr * freeVar = kv.first; - // skip all regular expression vars - if (regex_variable_set.contains(freeVar)) { - continue; - } - - // Iterate the EQC of freeVar, its eqc variable should not be in the eqcRepSet. - // If found, have to filter it out - std::set eqVarSet; - get_var_in_eqc(freeVar, eqVarSet); - bool duplicated = false; - expr * dupVar = nullptr; - for (expr* eq : eqVarSet) { - if (eqcRepSet.contains(eq)) { - duplicated = true; - dupVar = eq; - break; - } - } - if (duplicated && dupVar != nullptr) { - TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) - << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;); - continue; - } else { - eqcRepSet.insert(freeVar); - } - } - - for (expr * freeVar : eqcRepSet) { - // has length constraint initially - bool standAlone = !input_var_in_len.contains(freeVar); - // iterate parents - if (standAlone) { - // I hope this works! - if (!ctx.e_internalized(freeVar)) { - ctx.internalize(freeVar, false); - } - enode * e_freeVar = ctx.get_enode(freeVar); - enode_vector::iterator it = e_freeVar->begin_parents(); - for (; it != e_freeVar->end_parents(); ++it) { - expr * parentAst = (*it)->get_owner(); - if (u.str.is_concat(to_app(parentAst))) { - standAlone = false; - break; - } - } - } - - if (standAlone) { - rational len_value; - bool len_value_exists = get_len_value(freeVar, len_value); - if (len_value_exists) { - leafVarSet.insert(freeVar); - } else { - aloneVars[-1].insert(freeVar); - } - } else { - leafVarSet.insert(freeVar); - } - } - - for (expr* lv : leafVarSet) { - expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, ""); - // gen_len_val_options_for_free_var() can legally return NULL, - // as methods that it calls may assert their own axioms instead. - if (toAssert) assert_axiom(toAssert); - - } - - for (auto const& kv : aloneVars) { - for (expr* av : kv.second) { - expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, ""); - // same deal with returning a NULL axiom here - if (toAssert) assert_axiom(toAssert); - } - } - } - - bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { - zstring nn2_str; - if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager()) - << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); - more_len_tests(nn1, nn2_str); - return true; - } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - if (nn2_str == "more") { - TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager()) - << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); - more_value_tests(nn1, nn2_str); - } - return true; - } else if (internal_unrollTest_vars.contains(nn1)) { - return true; - } else { - return false; - } - } - - void theory_str::more_len_tests(expr * lenTester, zstring lenTesterValue) { - ast_manager & m = get_manager(); - if (lenTester_fvar_map.contains(lenTester)) { - expr * fVar = lenTester_fvar_map[lenTester]; - expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); - TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (toAssert) { - assert_axiom(toAssert); - } - } - } - - void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { - ast_manager & m = get_manager(); (void)m; - - expr * fVar = valueTester_fvar_map[valTester]; - if (m_params.m_UseBinarySearch) { - if (!binary_search_len_tester_stack.contains(fVar) || binary_search_len_tester_stack[fVar].empty()) { - TRACE("str", tout << "WARNING: no active length testers for " << mk_pp(fVar, m) << std::endl;); - NOT_IMPLEMENTED_YET(); - } - expr * effectiveLenInd = binary_search_len_tester_stack[fVar].back(); - bool hasEqcValue; - expr * len_indicator_value = get_eqc_value(effectiveLenInd, hasEqcValue); - if (!hasEqcValue) { - TRACE("str", tout << "WARNING: length tester " << mk_pp(effectiveLenInd, m) << " at top of stack for " << mk_pp(fVar, m) << " has no EQC value" << std::endl;); - } else { - // safety check - zstring effectiveLenIndiStr; - u.str.is_string(len_indicator_value, effectiveLenIndiStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { - TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); - UNREACHABLE(); - } - expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (valueAssert != nullptr) { - assert_axiom(valueAssert); - } - } - } else { - int lenTesterCount; - if (fvar_lenTester_map.contains(fVar)) { - lenTesterCount = fvar_lenTester_map[fVar].size(); - } else { - lenTesterCount = 0; - } - - expr * effectiveLenInd = nullptr; - zstring effectiveLenIndiStr = ""; - for (int i = 0; i < lenTesterCount; ++i) { - expr * len_indicator_pre = fvar_lenTester_map[fVar][i]; - bool indicatorHasEqcValue = false; - expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); - if (indicatorHasEqcValue) { - zstring len_pIndiStr; - u.str.is_string(len_indicator_value, len_pIndiStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - if (len_pIndiStr != "more") { - effectiveLenInd = len_indicator_pre; - effectiveLenIndiStr = len_pIndiStr; - break; - } - } - } - expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (valueAssert != nullptr) { - assert_axiom(valueAssert); - } - } - } - - - // Return an expression of the form - // (tester = "less" | tester = "N" | tester = "more") & - // (tester = "less" iff len(freeVar) < N) & (tester = "more" iff len(freeVar) > N) & (tester = "N" iff len(freeVar) = N)) - expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - rational N = bounds.midPoint; - rational N_minus_one = N - rational::one(); - rational N_plus_one = N + rational::one(); - expr_ref lenFreeVar(mk_strlen(freeVar), m); - - TRACE("str", tout << "create case split for free var " << mk_pp(freeVar, m) - << " over " << mk_pp(tester, m) << " with midpoint " << N << std::endl;); - - expr_ref_vector combinedCaseSplit(m); - expr_ref_vector testerCases(m); - - expr_ref caseLess(ctx.mk_eq_atom(tester, mk_string("less")), m); - testerCases.push_back(caseLess); - combinedCaseSplit.push_back(ctx.mk_eq_atom(caseLess, m_autil.mk_le(lenFreeVar, m_autil.mk_numeral(N_minus_one, true) ))); - - expr_ref caseMore(ctx.mk_eq_atom(tester, mk_string("more")), m); - testerCases.push_back(caseMore); - combinedCaseSplit.push_back(ctx.mk_eq_atom(caseMore, m_autil.mk_ge(lenFreeVar, m_autil.mk_numeral(N_plus_one, true) ))); - - expr_ref caseEq(ctx.mk_eq_atom(tester, mk_string(N.to_string().c_str())), m); - testerCases.push_back(caseEq); - combinedCaseSplit.push_back(ctx.mk_eq_atom(caseEq, ctx.mk_eq_atom(lenFreeVar, m_autil.mk_numeral(N, true)))); - - combinedCaseSplit.push_back(mk_or(testerCases)); - - // force internalization on all terms in testerCases so we can extract literals - for (unsigned i = 0; i < testerCases.size(); ++i) { - expr * testerCase = testerCases.get(i); - if (!ctx.b_internalized(testerCase)) { - ctx.internalize(testerCase, false); - } - literal l = ctx.get_literal(testerCase); - case_split.push_back(l); - } - - expr_ref final_term(mk_and(combinedCaseSplit), m); - SASSERT(final_term); - TRACE("str", tout << "final term: " << mk_pp(final_term, m) << std::endl;); - return final_term; - } - - expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue) { - ast_manager & m = get_manager(); - - if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) { - TRACE("str", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; - for (ptr_vector::const_iterator it = binary_search_len_tester_stack[freeVar].begin(); - it != binary_search_len_tester_stack[freeVar].end(); ++it) { - expr * tester = *it; - tout << mk_pp(tester, m) << ": "; - if (binary_search_len_tester_info.contains(tester)) { - binary_search_info & bounds = binary_search_len_tester_info[tester]; - tout << "[" << bounds.lowerBound << " | " << bounds.midPoint << " | " << bounds.upperBound << "]!" << bounds.windowSize; - } else { - tout << "[WARNING: no bounds info available]"; - } - bool hasEqcValue; - expr * testerEqcValue = get_eqc_value(tester, hasEqcValue); - if (hasEqcValue) { - tout << " = " << mk_pp(testerEqcValue, m); - } else { - tout << " [no eqc value]"; - } - tout << std::endl; - } - ); - expr * lastTester = binary_search_len_tester_stack[freeVar].back(); - bool lastTesterHasEqcValue; - expr * lastTesterValue = get_eqc_value(lastTester, lastTesterHasEqcValue); - zstring lastTesterConstant; - if (!lastTesterHasEqcValue) { - TRACE("str", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); - // check previousLenTester - if (previousLenTester == lastTester) { - lastTesterConstant = previousLenTesterValue; - TRACE("str", tout << "invoked with previousLenTester info matching top of stack" << std::endl;); - } else { - TRACE("str", tout << "WARNING: unexpected reordering of length testers!" << std::endl;); - UNREACHABLE(); return nullptr; - } - } else { - u.str.is_string(lastTesterValue, lastTesterConstant); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - } - TRACE("str", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";); - if (lastTesterConstant == "more" || lastTesterConstant == "less") { - // use the previous bounds info to generate a new midpoint - binary_search_info lastBounds; - if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { - // unexpected - TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); - UNREACHABLE(); - } - TRACE("str", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;); - binary_search_info newBounds; - expr * newTester = nullptr; - if (lastTesterConstant == "more") { - // special case: if the midpoint, upper bound, and window size are all equal, - // we double the window size and adjust the bounds - if (lastBounds.midPoint == lastBounds.upperBound && lastBounds.upperBound == lastBounds.windowSize) { - TRACE("str", tout << "search hit window size; expanding" << std::endl;); - newBounds.lowerBound = lastBounds.windowSize + rational::one(); - newBounds.windowSize = lastBounds.windowSize * rational(2); - newBounds.upperBound = newBounds.windowSize; - newBounds.calculate_midpoint(); - } else if (false) { - // handle the case where the midpoint can't be increased further - // (e.g. a window like [50 | 50 | 50]!64 and we don't answer "50") - } else { - // general case - newBounds.lowerBound = lastBounds.midPoint + rational::one(); - newBounds.windowSize = lastBounds.windowSize; - newBounds.upperBound = lastBounds.upperBound; - newBounds.calculate_midpoint(); - } - if (!binary_search_next_var_high.find(lastTester, newTester)) { - newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); - binary_search_next_var_high.insert(lastTester, newTester); - } - refresh_theory_var(newTester); - } else if (lastTesterConstant == "less") { - if (false) { - // handle the case where the midpoint can't be decreased further - // (e.g. a window like [0 | 0 | 0]!64 and we don't answer "0" - } else { - // general case - newBounds.upperBound = lastBounds.midPoint - rational::one(); - newBounds.windowSize = lastBounds.windowSize; - newBounds.lowerBound = lastBounds.lowerBound; - newBounds.calculate_midpoint(); - } - if (!binary_search_next_var_low.find(lastTester, newTester)) { - newTester = mk_internal_lenTest_var(freeVar, newBounds.midPoint.get_int32()); - binary_search_next_var_low.insert(lastTester, newTester); - } - refresh_theory_var(newTester); - } - TRACE("str", tout << "new bounds are [" << newBounds.lowerBound << " | " << newBounds.midPoint << " | " << newBounds.upperBound << "]!" << newBounds.windowSize << std::endl;); - binary_search_len_tester_stack[freeVar].push_back(newTester); - m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); - binary_search_len_tester_info.insert(newTester, newBounds); - m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, newTester)); - - literal_vector case_split_literals; - expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals)); - m_trail.push_back(next_case_split); - // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - return next_case_split; - } else { // lastTesterConstant is a concrete value - TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); - // defensive check that this length did not converge on a negative value. - binary_search_info lastBounds; - if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { - // unexpected - TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); - UNREACHABLE(); - } - if (lastBounds.midPoint.is_neg()) { - TRACE("str", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;); - expr_ref axiom(m_autil.mk_ge(mk_strlen(freeVar), m_autil.mk_numeral(rational::zero(), true)), m); - return axiom; - } - // length is fixed - expr * valueAssert = gen_free_var_options(freeVar, lastTester, lastTesterConstant, nullptr, zstring("")); - return valueAssert; - } - } else { - // no length testers yet - TRACE("str", tout << "no length testers for " << mk_pp(freeVar, m) << std::endl;); - binary_search_len_tester_stack.insert(freeVar, ptr_vector()); - - expr * firstTester; - rational lowerBound(0); - rational upperBound(m_params.m_BinarySearchInitialUpperBound); - rational windowSize(upperBound); - rational midPoint(floor(upperBound / rational(2))); - if (!binary_search_starting_len_tester.find(freeVar, firstTester)) { - firstTester = mk_internal_lenTest_var(freeVar, midPoint.get_int32()); - binary_search_starting_len_tester.insert(freeVar, firstTester); - } - refresh_theory_var(firstTester); - - { - rational freeVar_len_value; - if (get_len_value(freeVar, freeVar_len_value)) { - TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); - midPoint = freeVar_len_value; - upperBound = midPoint * 2; - windowSize = upperBound; - } - } - - binary_search_len_tester_stack[freeVar].push_back(firstTester); - m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); - binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize); - binary_search_len_tester_info.insert(firstTester, new_info); - m_trail_stack.push(insert_obj_map(binary_search_len_tester_info, firstTester)); - - literal_vector case_split_literals; - expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals)); - m_trail.push_back(initial_case_split); - // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); - return initial_case_split; - } - } - static int computeGCD(int x, int y) { if (x == 0) { return y; @@ -2443,34 +1446,6 @@ namespace smt { return finalAND; } - void theory_str::print_value_tester_list(svector > & testerList) { - TRACE("str", - int ss = testerList.size(); - tout << "valueTesterList = {"; - for (int i = 0; i < ss; ++i) { - if (i % 4 == 0) { - tout << std::endl; - } - tout << "(" << testerList[i].first << ", "; - tout << mk_pp(testerList[i].second, get_manager()); - tout << "), "; - } - tout << std::endl << "}" << std::endl; - ); - } - - zstring theory_str::gen_val_string(int len, int_vector & encoding) { - SASSERT(charSetSize > 0); - SASSERT(!char_set.empty()); - - std::string re(len, char_set[0]); - for (int i = 0; i < (int) encoding.size() - 1; i++) { - int idx = encoding[i]; - re[len - 1 - i] = char_set[idx]; - } - return zstring(re.c_str()); - } - void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items) { context & ctx = get_context(); ast_manager & mgr = get_manager(); From 25e2b2251e82c608c430535eeb11a2e8f627431e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 5 May 2020 13:15:49 -0500 Subject: [PATCH 3/4] z3str3: remove legacy regex unroll methods --- src/ast/seq_decl_plugin.cpp | 7 - src/ast/seq_decl_plugin.h | 2 - src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_str_params.cpp | 2 - src/smt/params/theory_str_params.h | 8 - src/smt/theory_str.cpp | 487 +-------------------------- src/smt/theory_str.h | 25 -- src/smt/theory_str_mc.cpp | 430 ----------------------- 8 files changed, 7 insertions(+), 955 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 26e0ec25ef5..7d1061570ec 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -553,7 +553,6 @@ void seq_decl_plugin::init() { sort* str2TintT[3] = { strT, strT, intT }; sort* seqAintT[2] = { seqA, intT }; sort* seq3A[3] = { seqA, seqA, seqA }; - sort* reTintT[2] = { reT, intT }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); @@ -604,7 +603,6 @@ void seq_decl_plugin::init() { m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, nullptr, reT); m_sigs[_OP_REGEXP_FULL_CHAR] = alloc(psig, m, "re.allchar", 0, 0, nullptr, reT); m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); - m_sigs[_OP_RE_UNROLL] = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT); } void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { @@ -772,11 +770,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, default: m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); } - - case _OP_RE_UNROLL: - m_has_re = true; - match(*m_sigs[k], arity, domain, range, rng); - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 56bffa19502..e6d1d753abb 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -86,7 +86,6 @@ enum seq_op_kind { _OP_REGEXP_EMPTY, _OP_REGEXP_FULL_CHAR, _OP_SEQ_SKOLEM, - _OP_RE_UNROLL, LAST_SEQ_OP }; @@ -415,7 +414,6 @@ class seq_util { bool is_loop(expr const* n, expr*& body, unsigned& lo); bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi); bool is_loop(expr const* n, expr*& body, expr*& lo); - bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); } }; str str; re re; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 362de64843a..5c1ac5d9d92 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -102,7 +102,6 @@ def_module_params(module_name='smt', ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'), - ('str.regex_automata', BOOL, True, 'use automata-based reasoning for regular expressions (Z3str3 only)'), ('str.regex_automata_difficulty_threshold', UINT, 1000, 'difficulty threshold for regex automata heuristics'), ('str.regex_automata_intersection_difficulty_threshold', UINT, 1000, 'difficulty threshold for regex intersection heuristics'), ('str.regex_automata_failed_automaton_threshold', UINT, 10, 'number of failed automaton construction attempts after which a full automaton is automatically built'), diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index 1a13c60494d..e0802b5d77f 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -28,7 +28,6 @@ void theory_str_params::updt_params(params_ref const & _p) { m_UseFastValueTesterCache = p.str_fast_value_tester_cache(); m_StringConstantCache = p.str_string_constant_cache(); m_OverlapTheoryAwarePriority = p.str_overlap_priority(); - m_RegexAutomata = p.str_regex_automata(); m_RegexAutomata_DifficultyThreshold = p.str_regex_automata_difficulty_threshold(); m_RegexAutomata_IntersectionDifficultyThreshold = p.str_regex_automata_intersection_difficulty_threshold(); m_RegexAutomata_FailedAutomatonThreshold = p.str_regex_automata_failed_automaton_threshold(); @@ -49,7 +48,6 @@ void theory_str_params::display(std::ostream & out) const { DISPLAY_PARAM(m_UseFastValueTesterCache); DISPLAY_PARAM(m_StringConstantCache); DISPLAY_PARAM(m_OverlapTheoryAwarePriority); - DISPLAY_PARAM(m_RegexAutomata); DISPLAY_PARAM(m_RegexAutomata_DifficultyThreshold); DISPLAY_PARAM(m_RegexAutomata_IntersectionDifficultyThreshold); DISPLAY_PARAM(m_RegexAutomata_FailedAutomatonThreshold); diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index f293d3f0a40..6ee9d75e9f6 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -70,13 +70,6 @@ struct theory_str_params { double m_OverlapTheoryAwarePriority; - /* - * If RegexAutomata is set to true, - * Z3str3 will use automata-based methods to reason about - * regular expression constraints. - */ - bool m_RegexAutomata; - /* * RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3 * will not eagerly construct an automaton for a regular expression term. @@ -129,7 +122,6 @@ struct theory_str_params { m_UseFastValueTesterCache(true), m_StringConstantCache(true), m_OverlapTheoryAwarePriority(-0.1), - m_RegexAutomata(true), m_RegexAutomata_DifficultyThreshold(1000), m_RegexAutomata_IntersectionDifficultyThreshold(1000), m_RegexAutomata_FailedAutomatonThreshold(10), diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0bc5d8eb136..1893b4eba7b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -125,14 +125,9 @@ namespace smt { fvar_valueTester_map.reset(); valueTester_fvar_map.reset(); val_range_map.reset(); - unroll_tries_map.reset(); - unroll_var_map.reset(); - concat_eq_unroll_ast_map.reset(); contains_map.reset(); contain_pair_bool_map.reset(); contain_pair_idx_map.reset(); - regex_in_bool_map.clear(); - regex_in_var_reg_str_map.reset(); m_automata.reset(); regex_automata.reset(); @@ -607,17 +602,6 @@ namespace smt { return a; } - app * theory_str::mk_unroll_bound_var() { - return mk_int_var("unroll"); - } - - app * theory_str::mk_unroll_test_var() { - app * v = mk_str_var("unrollTest"); // was uRt - internal_unrollTest_vars.insert(v); - track_variable_scope(v); - return v; - } - app * theory_str::mk_str_var(std::string name) { context & ctx = get_context(); @@ -646,28 +630,6 @@ namespace smt { return a; } - app * theory_str::mk_regex_rep_var() { - context & ctx = get_context(); - - sort * string_sort = u.str.mk_string_sort(); - app * a = mk_fresh_const("regex", string_sort); - m_trail.push_back(a); - - ctx.internalize(a, false); - SASSERT(ctx.get_enode(a) != nullptr); - SASSERT(ctx.e_internalized(a)); - mk_var(ctx.get_enode(a)); - m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;); - - variable_set.insert(a); - //internal_variable_set.insert(a); - regex_variable_set.insert(a); - track_variable_scope(a); - - return a; - } - void theory_str::add_nonempty_constraint(expr * s) { context & ctx = get_context(); ast_manager & m = get_manager(); @@ -733,25 +695,6 @@ namespace smt { return a; } - app * theory_str::mk_unroll(expr * n, expr * bound) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - expr * args[2] = {n, bound}; - app * unrollFunc = get_manager().mk_app(get_id(), _OP_RE_UNROLL, 0, nullptr, 2, args); - m_trail.push_back(unrollFunc); - - expr_ref_vector items(m); - items.push_back(ctx.mk_eq_atom(ctx.mk_eq_atom(bound, mk_int(0)), ctx.mk_eq_atom(unrollFunc, mk_string("")))); - items.push_back(m_autil.mk_ge(bound, mk_int(0))); - items.push_back(m_autil.mk_ge(mk_strlen(unrollFunc), mk_int(0))); - - expr_ref finalAxiom(mk_and(items), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - return unrollFunc; - } - app * theory_str::mk_contains(expr * haystack, expr * needle) { app * contains = u.str.mk_contains(haystack, needle); // TODO double-check semantics/argument order m_trail.push_back(contains); @@ -2062,7 +2005,6 @@ namespace smt { } void theory_str::instantiate_axiom_RegexIn(enode * e) { - context & ctx = get_context(); ast_manager & m = get_manager(); app * ex = e->get_owner(); @@ -2074,128 +2016,13 @@ namespace smt { TRACE("str", tout << "instantiate RegexIn axiom for " << mk_pp(ex, m) << std::endl;); - { - zstring regexStr = get_std_regex_str(ex->get_arg(1)); - std::pair key1(ex->get_arg(0), regexStr); - // skip Z3str's map check, because we already check if we set up axioms on this term - regex_in_bool_map[key1] = ex; - if (!regex_in_var_reg_str_map.contains(ex->get_arg(0))) { - regex_in_var_reg_str_map.insert(ex->get_arg(0), std::set()); - } - regex_in_var_reg_str_map[ex->get_arg(0)].insert(regexStr); - } - expr_ref str(ex->get_arg(0), m); - app * regex = to_app(ex->get_arg(1)); - - if (m_params.m_RegexAutomata) { - regex_terms.insert(ex); - if (!regex_terms_by_string.contains(str)) { - regex_terms_by_string.insert(str, ptr_vector()); - } - regex_terms_by_string[str].push_back(ex); - // stop setting up axioms here, we do this differently - return; - } - - // quick reference for the following code: - // - ex: top-level regex membership term - // - str: string term appearing in ex - // - regex: regex term appearing in ex - // ex ::= (str.in.re str regex) - - if (u.re.is_to_re(regex)) { - expr_ref rxStr(regex->get_arg(0), m); - // want to assert 'expr IFF (str == rxStr)' - expr_ref rhs(ctx.mk_eq_atom(str, rxStr), m); - expr_ref finalAxiom(m.mk_iff(ex, rhs), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - TRACE("str", tout << "set up Str2Reg: (RegexIn " << mk_pp(str, m) << " " << mk_pp(regex, m) << ")" << std::endl;); - } else if (u.re.is_concat(regex)) { - expr_ref var1(mk_regex_rep_var(), m); - expr_ref var2(mk_regex_rep_var(), m); - expr_ref rhs(mk_concat(var1, var2), m); - expr_ref rx1(regex->get_arg(0), m); - expr_ref rx2(regex->get_arg(1), m); - expr_ref var1InRegex1(mk_RegexIn(var1, rx1), m); - expr_ref var2InRegex2(mk_RegexIn(var2, rx2), m); - - expr_ref_vector items(m); - items.push_back(var1InRegex1); - items.push_back(var2InRegex2); - items.push_back(ctx.mk_eq_atom(ex, ctx.mk_eq_atom(str, rhs))); - expr_ref finalAxiom(mk_and(items), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - } else if (u.re.is_union(regex)) { - expr_ref var1(mk_regex_rep_var(), m); - expr_ref var2(mk_regex_rep_var(), m); - expr_ref orVar(m.mk_or(ctx.mk_eq_atom(str, var1), ctx.mk_eq_atom(str, var2)), m); - expr_ref regex1(regex->get_arg(0), m); - expr_ref regex2(regex->get_arg(1), m); - expr_ref var1InRegex1(mk_RegexIn(var1, regex1), m); - expr_ref var2InRegex2(mk_RegexIn(var2, regex2), m); - expr_ref_vector items(m); - items.push_back(var1InRegex1); - items.push_back(var2InRegex2); - items.push_back(ctx.mk_eq_atom(ex, orVar)); - assert_axiom(mk_and(items)); - } else if (u.re.is_star(regex)) { - // slightly more complex due to the unrolling step. - expr_ref regex1(regex->get_arg(0), m); - expr_ref unrollCount(mk_unroll_bound_var(), m); - expr_ref unrollFunc(mk_unroll(regex1, unrollCount), m); - expr_ref_vector items(m); - items.push_back(ctx.mk_eq_atom(ex, ctx.mk_eq_atom(str, unrollFunc))); - items.push_back(ctx.mk_eq_atom(ctx.mk_eq_atom(unrollCount, mk_int(0)), ctx.mk_eq_atom(unrollFunc, mk_string("")))); - expr_ref finalAxiom(mk_and(items), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - } else if (u.re.is_range(regex)) { - // (re.range "A" "Z") unfolds to (re.union "A" "B" ... "Z"); - // we rewrite to expr IFF (str = "A" or str = "B" or ... or str = "Z") - expr_ref lo(regex->get_arg(0), m); - expr_ref hi(regex->get_arg(1), m); - zstring str_lo, str_hi; - SASSERT(u.str.is_string(lo)); - SASSERT(u.str.is_string(hi)); - u.str.is_string(lo, str_lo); - u.str.is_string(hi, str_hi); - SASSERT(str_lo.length() == 1); - SASSERT(str_hi.length() == 1); - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange - unsigned int tmp = c1; - c1 = c2; - c2 = tmp; - } - expr_ref_vector range_cases(m); - for (unsigned int ch = c1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref rhs(ctx.mk_eq_atom(str, u.str.mk_string(s_ch)), m); - range_cases.push_back(rhs); - } - expr_ref rhs(mk_or(range_cases), m); - expr_ref finalAxiom(m.mk_iff(ex, rhs), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - } else if (u.re.is_full_seq(regex)) { - // trivially true for any string! - assert_axiom(ex); - } else if (u.re.is_full_char(regex)) { - // any char = any string of length 1 - expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), mk_int(1)), m); - expr_ref finalAxiom(m.mk_iff(ex, rhs), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - } else { - TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); - NOT_IMPLEMENTED_YET(); + regex_terms.insert(ex); + if (!regex_terms_by_string.contains(str)) { + regex_terms_by_string.insert(str, ptr_vector()); } + regex_terms_by_string[str].push_back(ex); } void theory_str::attach_new_th_var(enode * n) { @@ -2270,11 +2097,6 @@ namespace smt { check_contain_in_new_eq(lhs, rhs); } - if (!regex_in_bool_map.empty() && !m_params.m_RegexAutomata) { - TRACE("str", tout << "checking regex consistency" << std::endl;); - check_regex_in(lhs, rhs); - } - // okay, all checks here passed return true; } @@ -4842,125 +4664,6 @@ namespace smt { generate_mutual_exclusion(arrangement_disjunction); } - void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) { - if (!u.re.is_unroll(to_app(unrollFunc))) { - return; - } - if (!u.str.is_string(constStr)) { - return; - } - - expr * funcInUnroll = to_app(unrollFunc)->get_arg(0); - zstring strValue; - u.str.is_string(constStr, strValue); - - TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, get_manager()) << std::endl - << "constStr: " << mk_pp(constStr, get_manager()) << std::endl;); - - if (strValue == "") { - return; - } - - if (u.re.is_to_re(to_app(funcInUnroll))) { - unroll_str2reg_constStr(unrollFunc, constStr); - return; - } - } - - void theory_str::process_concat_eq_unroll(expr * concat, expr * unroll) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - TRACE("str", tout << "concat = " << mk_pp(concat, mgr) << ", unroll = " << mk_pp(unroll, mgr) << std::endl;); - - expr_ref toAssert(mgr); - expr * _toAssert; - - if (!concat_eq_unroll_ast_map.find(concat, unroll, _toAssert)) { - expr_ref arg1(to_app(concat)->get_arg(0), mgr); - expr_ref arg2(to_app(concat)->get_arg(1), mgr); - expr_ref r1(to_app(unroll)->get_arg(0), mgr); - expr_ref t1(to_app(unroll)->get_arg(1), mgr); - - expr_ref v1(mk_regex_rep_var(), mgr); - expr_ref v2(mk_regex_rep_var(), mgr); - expr_ref v3(mk_regex_rep_var(), mgr); - expr_ref v4(mk_regex_rep_var(), mgr); - expr_ref v5(mk_regex_rep_var(), mgr); - - expr_ref t2(mk_unroll_bound_var(), mgr); - expr_ref t3(mk_unroll_bound_var(), mgr); - expr_ref emptyStr(mk_string(""), mgr); - - expr_ref unroll1(mk_unroll(r1, t2), mgr); - expr_ref unroll2(mk_unroll(r1, t3), mgr); - - expr_ref op0(ctx.mk_eq_atom(t1, mk_int(0)), mgr); - expr_ref op1(m_autil.mk_ge(t1, mk_int(1)), mgr); - - expr_ref_vector op1Items(mgr); - expr_ref_vector op2Items(mgr); - - op1Items.push_back(ctx.mk_eq_atom(arg1, emptyStr)); - op1Items.push_back(ctx.mk_eq_atom(arg2, emptyStr)); - op1Items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(0))); - op1Items.push_back(ctx.mk_eq_atom(mk_strlen(arg2), mk_int(0))); - expr_ref opAnd1(ctx.mk_eq_atom(op0, mk_and(op1Items)), mgr); - - expr_ref v1v2(mk_concat(v1, v2), mgr); - op2Items.push_back(ctx.mk_eq_atom(arg1, v1v2)); - op2Items.push_back(ctx.mk_eq_atom(mk_strlen(arg1), m_autil.mk_add(mk_strlen(v1), mk_strlen(v2)))); - expr_ref v3v4(mk_concat(v3, v4), mgr); - op2Items.push_back(ctx.mk_eq_atom(arg2, v3v4)); - op2Items.push_back(ctx.mk_eq_atom(mk_strlen(arg2), m_autil.mk_add(mk_strlen(v3), mk_strlen(v4)))); - - op2Items.push_back(ctx.mk_eq_atom(v1, unroll1)); - op2Items.push_back(ctx.mk_eq_atom(mk_strlen(v1), mk_strlen(unroll1))); - op2Items.push_back(ctx.mk_eq_atom(v4, unroll2)); - op2Items.push_back(ctx.mk_eq_atom(mk_strlen(v4), mk_strlen(unroll2))); - expr_ref v2v3(mk_concat(v2, v3), mgr); - op2Items.push_back(ctx.mk_eq_atom(v5, v2v3)); - reduce_virtual_regex_in(v5, r1, op2Items); - op2Items.push_back(ctx.mk_eq_atom(mk_strlen(v5), m_autil.mk_add(mk_strlen(v2), mk_strlen(v3)))); - op2Items.push_back(ctx.mk_eq_atom(m_autil.mk_add(t2, t3), m_autil.mk_add(t1, mk_int(-1)))); - expr_ref opAnd2(ctx.mk_eq_atom(op1, mk_and(op2Items)), mgr); - - toAssert = mgr.mk_and(opAnd1, opAnd2); - m_trail.push_back(toAssert); - concat_eq_unroll_ast_map.insert(concat, unroll, toAssert); - } else { - toAssert = _toAssert; - } - - assert_axiom(toAssert); - } - - void theory_str::unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - expr * str2RegFunc = to_app(unrollFunc)->get_arg(0); - expr * strInStr2RegFunc = to_app(str2RegFunc)->get_arg(0); - expr * oriCnt = to_app(unrollFunc)->get_arg(1); - - zstring strValue; - u.str.is_string(eqConstStr, strValue); - zstring regStrValue; - u.str.is_string(strInStr2RegFunc, regStrValue); - unsigned int strLen = strValue.length(); - unsigned int regStrLen = regStrValue.length(); - SASSERT(regStrLen != 0); // this should never occur -- the case for empty string is handled elsewhere - unsigned int cnt = strLen / regStrLen; - - expr_ref implyL(ctx.mk_eq_atom(unrollFunc, eqConstStr), m); - expr_ref implyR1(ctx.mk_eq_atom(oriCnt, mk_int(cnt)), m); - expr_ref implyR2(ctx.mk_eq_atom(mk_strlen(unrollFunc), mk_int(strLen)), m); - expr_ref axiomRHS(m.mk_and(implyR1, implyR2), m); - SASSERT(implyL); - SASSERT(axiomRHS); - assert_implication(implyL, axiomRHS); - } - /* * Look through the equivalence class of n to find a string constant. * Return that constant if it is found, and set hasEqcValue to true. @@ -5801,9 +5504,6 @@ namespace smt { std::map & concatAliasMap, std::map & varConstMap, std::map & concatConstMap, std::map > & varEqConcatMap, std::map, std::set > > & groundedMap) { - if (u.re.is_unroll(to_app(node))) { - return; - } // ************************************************** // first deAlias the node if it is a var or concat // ************************************************** @@ -6685,60 +6385,6 @@ namespace smt { } } - void theory_str::check_regex_in(expr * nn1, expr * nn2) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - expr_ref_vector eqNodeSet(m); - - expr * constStr_1 = collect_eq_nodes(nn1, eqNodeSet); - expr * constStr_2 = collect_eq_nodes(nn2, eqNodeSet); - expr * constStr = (constStr_1 != nullptr) ? constStr_1 : constStr_2; - - if (constStr == nullptr) { - return; - } else { - expr_ref_vector::iterator itor = eqNodeSet.begin(); - for (; itor != eqNodeSet.end(); itor++) { - if (regex_in_var_reg_str_map.contains(*itor)) { - std::set::iterator strItor = regex_in_var_reg_str_map[*itor].begin(); - for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) { - zstring regStr = *strItor; - zstring constStrValue; - u.str.is_string(constStr, constStrValue); - std::pair key1 = std::make_pair(*itor, regStr); - if (regex_in_bool_map.find(key1) != regex_in_bool_map.end()) { - expr * boolVar = regex_in_bool_map[key1]; // actually the RegexIn term - app * a_regexIn = to_app(boolVar); - expr * regexTerm = a_regexIn->get_arg(1); - - // TODO figure out regex NFA stuff - if (!regex_nfa_cache.contains(regexTerm)) { - TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;); - regex_nfa_cache.insert(regexTerm, nfa(u, regexTerm)); - } else { - TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;); - } - - nfa regexNFA = regex_nfa_cache[regexTerm]; - ENSURE(regexNFA.is_valid()); - bool matchRes = regexNFA.matches(constStrValue); - - TRACE("str", tout << mk_pp(*itor, m) << " in " << regStr << " : " << (matchRes ? "yes" : "no") << std::endl;); - - expr_ref implyL(ctx.mk_eq_atom(*itor, constStr), m); - if (matchRes) { - assert_implication(implyL, boolVar); - } else { - assert_implication(implyL, mk_not(m, boolVar)); - } - } - } - } - } - } - } - /* * strArgmt::solve_concat_eq_str() * Solve concatenations of the form: @@ -7228,26 +6874,6 @@ namespace smt { if (!nn1HasEqcValue && nn2HasEqcValue) { simplify_parent(lhs, nn2_value); } - - expr * nn1EqConst = nullptr; - std::set nn1EqUnrollFuncs; - get_eqc_allUnroll(lhs, nn1EqConst, nn1EqUnrollFuncs); - expr * nn2EqConst = nullptr; - std::set nn2EqUnrollFuncs; - get_eqc_allUnroll(rhs, nn2EqConst, nn2EqUnrollFuncs); - - if (nn2EqConst != nullptr) { - for (std::set::iterator itor1 = nn1EqUnrollFuncs.begin(); itor1 != nn1EqUnrollFuncs.end(); itor1++) { - process_unroll_eq_const_str(*itor1, nn2EqConst); - } - } - - if (nn1EqConst != nullptr) { - for (std::set::iterator itor2 = nn2EqUnrollFuncs.begin(); itor2 != nn2EqUnrollFuncs.end(); itor2++) { - process_unroll_eq_const_str(*itor2, nn1EqConst); - } - } - } // Check that a string's length can be 0 iff it is the empty string. @@ -7775,11 +7401,6 @@ namespace smt { if (canskip == 0 && concatMap.find(node) == concatMap.end()) { concatMap[node] = 1; } - } else if (u.re.is_unroll(aNode)) { - // Unroll - if (unrollMap.find(node) == unrollMap.end()) { - unrollMap[node] = 1; - } } // recursively visit all arguments for (unsigned i = 0; i < aNode->get_num_args(); ++i) { @@ -8038,33 +7659,6 @@ namespace smt { } classify_ast_by_type_in_positive_context(strVarMap, concatMap, unrollMap); - std::map aliasUnrollSet; - std::map::iterator unrollItor = unrollMap.begin(); - for (; unrollItor != unrollMap.end(); ++unrollItor) { - if (aliasUnrollSet.find(unrollItor->first) != aliasUnrollSet.end()) { - continue; - } - expr * aRoot = nullptr; - enode * e_currEqc = ctx.get_enode(unrollItor->first); - enode * e_curr = e_currEqc; - do { - app * curr = e_currEqc->get_owner(); - if (u.re.is_unroll(curr)) { - if (aRoot == nullptr) { - aRoot = curr; - } - aliasUnrollSet[curr] = aRoot; - } - e_currEqc = e_currEqc->get_next(); - } while (e_currEqc != e_curr); - } - - for (unrollItor = unrollMap.begin(); unrollItor != unrollMap.end(); unrollItor++) { - expr * unrFunc = unrollItor->first; - expr * urKey = aliasUnrollSet[unrFunc]; - unrollGroupMap[urKey].insert(unrFunc); - } - // Step 2: collect alias relation // e.g. suppose we have the equivalence class {x, y, z}; // then we set aliasIndexMap[y] = x @@ -8144,8 +7738,6 @@ namespace smt { if (!is_arg0_emptyStr && !is_arg1_emptyStr) { var_eq_concat_map[deAliasNode][curr] = 1; } - } else if (u.re.is_unroll(to_app(curr))) { - var_eq_unroll_map[deAliasNode][curr] = 1; } curr = get_eqc_next(curr); @@ -9047,10 +8639,7 @@ namespace smt { } } - // regex automata - if (m_params.m_RegexAutomata) { - solve_regex_automata(); - } // RegexAutomata + solve_regex_automata(); bool needToAssignFreeVars = false; expr_ref_vector free_variables(m); @@ -9112,7 +8701,7 @@ namespace smt { // the string assignment for each variable is consistent with the automaton. // The (probably) easiest way to do this is to ensure // that we have path constraints set up for every assigned regex term. - if (m_params.m_RegexAutomata && !regex_terms.empty()) { + if (!regex_terms.empty()) { for (obj_hashtable::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) { expr * str_in_re = *it; expr * str; @@ -9163,16 +8752,7 @@ namespace smt { // (2) vars are not bounded by either concat or unroll // ----------------------------------------------------------- std::map > fv_unrolls_map; - std::set tmpSet; - expr * constValue = nullptr; - for (std::map::iterator fvIt2 = freeVar_map.begin(); fvIt2 != freeVar_map.end(); fvIt2++) { - expr * var = fvIt2->first; - tmpSet.clear(); - get_eqc_allUnroll(var, constValue, tmpSet); - if (!tmpSet.empty()) { - fv_unrolls_map[var] = tmpSet; - } - } + // erase var bounded by an unroll function from freeVar_map for (std::map >::iterator fvIt3 = fv_unrolls_map.begin(); fvIt3 != fv_unrolls_map.end(); fvIt3++) { @@ -9248,8 +8828,6 @@ namespace smt { // Assign free variables std::set fSimpUnroll; - constValue = nullptr; - { TRACE("str", tout << "free var map (#" << freeVar_map.size() << "):" << std::endl; for (std::map::iterator freeVarItor1 = freeVar_map.begin(); freeVarItor1 != freeVar_map.end(); freeVarItor1++) { @@ -9263,15 +8841,6 @@ namespace smt { ); } - for (std::map >::iterator fvIt2 = concatFreeArgsEqUnrollsMap.begin(); - fvIt2 != concatFreeArgsEqUnrollsMap.end(); fvIt2++) { - expr * concat = fvIt2->first; - for (std::set::iterator urItor = fvIt2->second.begin(); urItor != fvIt2->second.end(); urItor++) { - expr * unroll = *urItor; - process_concat_eq_unroll(concat, unroll); - } - } - { // TODO if we're using fixed-length testing, do we care about finding free variables any more? // that work might be useless @@ -9357,48 +8926,6 @@ namespace smt { return lhs_name.str() < rhs_name.str(); } - /* - * Collect all unroll functions - * and constant string in eqc of node n - */ - void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set & unrollFuncSet) { - constStr = nullptr; - unrollFuncSet.clear(); - - expr * curr = n; - do { - if (u.str.is_string(to_app(curr))) { - constStr = curr; - } else if (u.re.is_unroll(to_app(curr))) { - if (unrollFuncSet.find(curr) == unrollFuncSet.end()) { - unrollFuncSet.insert(curr); - } - } - curr = get_eqc_next(curr); - } while (curr != n); - } - - // Collect simple Unroll functions (whose core is Str2Reg) and constant strings in the EQC of n. - void theory_str::get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set & unrollFuncSet) { - constStr = nullptr; - unrollFuncSet.clear(); - - expr * curr = n; - do { - if (u.str.is_string(to_app(curr))) { - constStr = curr; - } else if (u.re.is_unroll(to_app(curr))) { - expr * core = to_app(curr)->get_arg(0); - if (u.re.is_to_re(to_app(core))) { - if (unrollFuncSet.find(curr) == unrollFuncSet.end()) { - unrollFuncSet.insert(curr); - } - } - } - curr = get_eqc_next(curr); - } while (curr != n); - } - void theory_str::init_model(model_generator & mg) { //TRACE("str", tout << "initializing model" << std::endl; display(tout);); m_factory = alloc(str_value_factory, get_manager(), get_family_id()); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index d41de45bfb8..9ce86361a3b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -504,21 +504,12 @@ class theory_str : public theory { obj_map val_range_map; - // This can't be an expr_ref_vector because the constructor is wrong, - // we would need to modify the allocator so we pass in ast_manager - obj_map, ptr_vector > > unroll_tries_map; - obj_map unroll_var_map; - obj_pair_map concat_eq_unroll_ast_map; expr_ref_vector contains_map; theory_str_contain_pair_bool_map_t contain_pair_bool_map; obj_map > > contain_pair_idx_map; - // TBD: do a curried map for determinism. - std::map, expr*> regex_in_bool_map; - obj_map > regex_in_var_reg_str_map; - // regex automata scoped_ptr_vector m_automata; ptr_vector regex_automata; @@ -653,9 +644,6 @@ class theory_str : public theory { app * mk_int_var(std::string name); app_ref mk_nonempty_str_var(); app * mk_internal_xor_var(); - app * mk_regex_rep_var(); - app * mk_unroll_bound_var(); - app * mk_unroll_test_var(); void add_nonempty_constraint(expr * s); void instantiate_concat_axiom(enode * cat); @@ -687,10 +675,6 @@ class theory_str : public theory { expr * mk_RegexIn(expr * str, expr * regexp); void instantiate_axiom_RegexIn(enode * e); - app * mk_unroll(expr * n, expr * bound); - void process_unroll_eq_const_str(expr * unrollFunc, expr * constStr); - void unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr); - void process_concat_eq_unroll(expr * concat, expr * unroll); // regex automata and length-aware regex void solve_regex_automata(); @@ -834,15 +818,6 @@ class theory_str : public theory { bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity); // strRegex - - void get_eqc_allUnroll(expr * n, expr * &constStr, std::set & unrollFuncSet); - void get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set & unrollFuncSet); - void gen_assign_unroll_reg(std::set & unrolls); - expr * gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls); - expr * gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr); - expr * gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h); - void reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items); - void check_regex_in(expr * nn1, expr * nn2); zstring get_std_regex_str(expr * r); void dump_assignments(); diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index ffe55a4d00c..2ca1482d7f2 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -1214,434 +1214,4 @@ namespace smt { } } - static int computeGCD(int x, int y) { - if (x == 0) { - return y; - } - while (y != 0) { - if (x > y) { - x = x - y; - } else { - y = y - x; - } - } - return x; - } - - static int computeLCM(int a, int b) { - int temp = computeGCD(a, b); - return temp ? (a / temp * b) : 0; - } - - static zstring get_unrolled_string(zstring core, int count) { - zstring res(""); - for (int i = 0; i < count; i++) { - res = res + core; - } - return res; - } - - expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - int lcm = 1; - int coreValueCount = 0; - expr * oneUnroll = nullptr; - zstring oneCoreStr(""); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr * str2RegFunc = to_app(*itor)->get_arg(0); - expr * coreVal = to_app(str2RegFunc)->get_arg(0); - zstring coreStr; - u.str.is_string(coreVal, coreStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - if (oneUnroll == nullptr) { - oneUnroll = *itor; - oneCoreStr = coreStr; - } - coreValueCount++; - int core1Len = coreStr.length(); - lcm = computeLCM(lcm, core1Len); - } - // - bool canHaveNonEmptyAssign = true; - expr_ref_vector litems(mgr); - zstring lcmStr = get_unrolled_string(oneCoreStr, (lcm / oneCoreStr.length())); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr * str2RegFunc = to_app(*itor)->get_arg(0); - expr * coreVal = to_app(str2RegFunc)->get_arg(0); - zstring coreStr; - u.str.is_string(coreVal, coreStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - unsigned int core1Len = coreStr.length(); - zstring uStr = get_unrolled_string(coreStr, (lcm / core1Len)); - if (uStr != lcmStr) { - canHaveNonEmptyAssign = false; - } - litems.push_back(ctx.mk_eq_atom(n, *itor)); - } - - if (canHaveNonEmptyAssign) { - return gen_unroll_conditional_options(n, unrolls, lcmStr); - } else { - expr_ref implyL(mk_and(litems), mgr); - expr_ref implyR(ctx.mk_eq_atom(n, mk_string("")), mgr); - // want to return (implyL -> implyR) - expr * final_axiom = rewrite_implication(implyL, implyR); - return final_axiom; - } - } - - expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & unrolls, zstring lcmStr) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - int dist = opt_LCMUnrollStep; - expr_ref_vector litems(mgr); - expr_ref moreAst(mk_string("more"), mgr); - for (expr * e : unrolls) { - expr_ref item(ctx.mk_eq_atom(var, e), mgr); - TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); - litems.push_back(item); - } - - // handle out-of-scope entries in unroll_tries_map - - ptr_vector outOfScopeTesters; - - for (expr * tester : unroll_tries_map[var][unrolls]) { - bool inScope = internal_unrollTest_vars.contains(tester); - TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) - << (inScope ? " in scope" : " out of scope") - << std::endl;); - if (!inScope) { - outOfScopeTesters.push_back(tester); - } - } - - for (expr* e : outOfScopeTesters) { - unroll_tries_map[var][unrolls].erase(e); - } - - if (unroll_tries_map[var][unrolls].empty()) { - unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); - } - - int tries = unroll_tries_map[var][unrolls].size(); - for (int i = 0; i < tries; i++) { - expr * tester = unroll_tries_map[var][unrolls][i]; - // TESTING - refresh_theory_var(tester); - bool testerHasValue = false; - expr * testerVal = get_eqc_value(tester, testerHasValue); - if (!testerHasValue) { - // generate make-up assertion - int l = i * dist; - int h = (i + 1) * dist; - expr_ref lImp(mk_and(litems), mgr); - expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); - - SASSERT(lImp); - TRACE("str", tout << "lImp = " << mk_pp(lImp, mgr) << std::endl;); - SASSERT(rImp); - TRACE("str", tout << "rImp = " << mk_pp(rImp, mgr) << std::endl;); - - expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); - SASSERT(toAssert); - TRACE("str", tout << "Making up assignments for variable which is equal to unbounded Unroll" << std::endl;); - m_trail.push_back(toAssert); - return toAssert; - - // note: this is how the code looks in Z3str2's strRegex.cpp:genUnrollConditionalOptions. - // the return is in the same place - - // insert [tester = "more"] to litems so that the implyL for next tester is correct - litems.push_back(ctx.mk_eq_atom(tester, moreAst)); - } else { - zstring testerStr; - u.str.is_string(testerVal, testerStr); - // NSB: is argument always a string? Then use VERIFY, or otherwise test return value - TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); - if (testerStr == "more") { - litems.push_back(ctx.mk_eq_atom(tester, moreAst)); - } - } - } - expr * tester = mk_unroll_test_var(); - unroll_tries_map[var][unrolls].push_back(tester); - int l = tries * dist; - int h = (tries + 1) * dist; - expr_ref lImp(mk_and(litems), mgr); - expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); - SASSERT(lImp); - SASSERT(rImp); - expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); - SASSERT(toAssert); - TRACE("str", tout << "Generating assignment for variable which is equal to unbounded Unroll" << std::endl;); - m_trail.push_back(toAssert); - return toAssert; - } - - expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - TRACE("str", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr - << ", l = " << l << ", h = " << h << "\n";); - - if (m_params.m_AggressiveUnrollTesting) { - TRACE("str", tout << "note: aggressive unroll testing is active" << std::endl;); - } - - expr_ref_vector orItems(mgr); - expr_ref_vector andItems(mgr); - - for (int i = l; i < h; i++) { - zstring iStr = int_to_string(i); - expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, mk_string(iStr)), mgr); - TRACE("str", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); - if (m_params.m_AggressiveUnrollTesting) { - literal l = mk_eq(testerVar, mk_string(iStr), false); - ctx.mark_as_relevant(l); - ctx.force_phase(l); - } - - orItems.push_back(testerEqAst); - zstring unrollStrInstance = get_unrolled_string(lcmStr, i); - - expr_ref x1(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(var, mk_string(unrollStrInstance))), mgr); - TRACE("str", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); - andItems.push_back(x1); - - expr_ref x2(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(mk_strlen(var), mk_int(i * lcmStr.length()))), mgr); - TRACE("str", tout << "x2 = " << mk_pp(x2, mgr) << std::endl;); - andItems.push_back(x2); - } - expr_ref testerEqMore(ctx.mk_eq_atom(testerVar, mk_string("more")), mgr); - TRACE("str", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;); - if (m_params.m_AggressiveUnrollTesting) { - literal l = mk_eq(testerVar, mk_string("more"), false); - ctx.mark_as_relevant(l); - ctx.force_phase(~l); - } - - orItems.push_back(testerEqMore); - int nextLowerLenBound = h * lcmStr.length(); - expr_ref more2(ctx.mk_eq_atom(testerEqMore, - //Z3_mk_ge(mk_length(t, var), mk_int(ctx, nextLowerLenBound)) - m_autil.mk_ge(m_autil.mk_add(mk_strlen(var), mk_int(-1 * nextLowerLenBound)), mk_int(0)) - ), mgr); - TRACE("str", tout << "more2 = " << mk_pp(more2, mgr) << std::endl;); - andItems.push_back(more2); - - expr_ref finalOR(mgr.mk_or(orItems.size(), orItems.c_ptr()), mgr); - TRACE("str", tout << "finalOR = " << mk_pp(finalOR, mgr) << std::endl;); - andItems.push_back(mk_or(orItems)); - - expr_ref finalAND(mgr.mk_and(andItems.size(), andItems.c_ptr()), mgr); - TRACE("str", tout << "finalAND = " << mk_pp(finalAND, mgr) << std::endl;); - - // doing the following avoids a segmentation fault - m_trail.push_back(finalAND); - return finalAND; - } - - void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - TRACE("str", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); - - app * regexFuncDecl = to_app(regex); - if (u.re.is_to_re(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in Str2Reg(s1) - // ==> - // var = s1 /\ length(var) = length(s1) - // --------------------------------------------------------- - expr * strInside = to_app(regex)->get_arg(0); - items.push_back(ctx.mk_eq_atom(var, strInside)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(strInside))); - return; - } - // RegexUnion - else if (u.re.is_union(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in RegexUnion(r1, r2) - // ==> - // (var = newVar1 \/ var = newVar2) - // (var = newVar1 --> length(var) = length(newVar1)) /\ (var = newVar2 --> length(var) = length(newVar2)) - // /\ (newVar1 \in r1) /\ (newVar2 \in r2) - // --------------------------------------------------------- - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - items.push_back(mgr.mk_or(ctx.mk_eq_atom(var, newVar1), ctx.mk_eq_atom(var, newVar2))); - items.push_back(mgr.mk_or( - mgr.mk_not(ctx.mk_eq_atom(var, newVar1)), - ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar1)))); - items.push_back(mgr.mk_or( - mgr.mk_not(ctx.mk_eq_atom(var, newVar2)), - ctx.mk_eq_atom(mk_strlen(var), mk_strlen(newVar2)))); - - expr * regArg1 = to_app(regex)->get_arg(0); - reduce_virtual_regex_in(newVar1, regArg1, items); - - expr * regArg2 = to_app(regex)->get_arg(1); - reduce_virtual_regex_in(newVar2, regArg2, items); - - return; - } - // RegexConcat - else if (u.re.is_concat(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in RegexConcat(r1, r2) - // ==> - // (var = newVar1 . newVar2) /\ (length(var) = length(vewVar1 . newVar2) ) - // /\ (newVar1 \in r1) /\ (newVar2 \in r2) - // --------------------------------------------------------- - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); - items.push_back(ctx.mk_eq_atom(var, concatAst)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), - m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); - - expr * regArg1 = to_app(regex)->get_arg(0); - reduce_virtual_regex_in(newVar1, regArg1, items); - expr * regArg2 = to_app(regex)->get_arg(1); - reduce_virtual_regex_in(newVar2, regArg2, items); - return; - } - // Unroll - else if (u.re.is_star(regexFuncDecl)) { - // --------------------------------------------------------- - // var \in Star(r1) - // ==> - // var = unroll(r1, t1) /\ |var| = |unroll(r1, t1)| - // --------------------------------------------------------- - expr * regArg = to_app(regex)->get_arg(0); - expr_ref unrollCnt(mk_unroll_bound_var(), mgr); - expr_ref unrollFunc(mk_unroll(regArg, unrollCnt), mgr); - items.push_back(ctx.mk_eq_atom(var, unrollFunc)); - items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_strlen(unrollFunc))); - return; - } - // re.range - else if (u.re.is_range(regexFuncDecl)) { - // var in range("a", "z") - // ==> - // (var = "a" or var = "b" or ... or var = "z") - expr_ref lo(regexFuncDecl->get_arg(0), mgr); - expr_ref hi(regexFuncDecl->get_arg(1), mgr); - zstring str_lo, str_hi; - SASSERT(u.str.is_string(lo)); - SASSERT(u.str.is_string(hi)); - VERIFY(u.str.is_string(lo, str_lo)); - VERIFY(u.str.is_string(hi, str_hi)); - SASSERT(str_lo.length() == 1); - SASSERT(str_hi.length() == 1); - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange - unsigned int tmp = c1; - c1 = c2; - c2 = tmp; - } - expr_ref_vector range_cases(mgr); - for (unsigned int ch = c1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref rhs(ctx.mk_eq_atom(var, u.str.mk_string(s_ch)), mgr); - range_cases.push_back(rhs); - } - expr_ref rhs(mk_or(range_cases), mgr); - SASSERT(rhs); - assert_axiom(rhs); - return; - } else { - get_manager().raise_exception("unrecognized regex operator"); - UNREACHABLE(); - } - } - - void theory_str::gen_assign_unroll_reg(std::set & unrolls) { - context & ctx = get_context(); - ast_manager & mgr = get_manager(); - - expr_ref_vector items(mgr); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr * unrFunc = *itor; - TRACE("str", tout << "generating assignment for unroll " << mk_pp(unrFunc, mgr) << std::endl;); - - expr * regexInUnr = to_app(unrFunc)->get_arg(0); - expr * cntInUnr = to_app(unrFunc)->get_arg(1); - items.reset(); - - rational low, high; - bool low_exists = lower_bound(cntInUnr, low); (void)low_exists; - bool high_exists = upper_bound(cntInUnr, high); (void)high_exists; - - TRACE("str", - tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; - rational unrLenValue; - bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); - tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl; - rational cntInUnrValue; - bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue); - tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?") - << " low = " - << (low_exists ? low.to_string() : "?") - << " high = " - << (high_exists ? high.to_string() : "?") - << std::endl; - ); - - expr_ref toAssert(mgr); - if (low.is_neg()) { - toAssert = m_autil.mk_ge(cntInUnr, mk_int(0)); - } else { - if (!unroll_var_map.contains(unrFunc)) { - - expr_ref newVar1(mk_regex_rep_var(), mgr); - expr_ref newVar2(mk_regex_rep_var(), mgr); - expr_ref concatAst(mk_concat(newVar1, newVar2), mgr); - expr_ref newCnt(mk_unroll_bound_var(), mgr); - expr_ref newUnrollFunc(mk_unroll(regexInUnr, newCnt), mgr); - - // unroll(r1, t1) = newVar1 . newVar2 - items.push_back(ctx.mk_eq_atom(unrFunc, concatAst)); - items.push_back(ctx.mk_eq_atom(mk_strlen(unrFunc), m_autil.mk_add(mk_strlen(newVar1), mk_strlen(newVar2)))); - // mk_strlen(unrFunc) >= mk_strlen(newVar{1,2}) - items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar1))), mk_int(0))); - items.push_back(m_autil.mk_ge(m_autil.mk_add(mk_strlen(unrFunc), m_autil.mk_mul(mk_int(-1), mk_strlen(newVar2))), mk_int(0))); - // newVar1 \in r1 - reduce_virtual_regex_in(newVar1, regexInUnr, items); - items.push_back(ctx.mk_eq_atom(cntInUnr, m_autil.mk_add(newCnt, mk_int(1)))); - items.push_back(ctx.mk_eq_atom(newVar2, newUnrollFunc)); - items.push_back(ctx.mk_eq_atom(mk_strlen(newVar2), mk_strlen(newUnrollFunc))); - toAssert = ctx.mk_eq_atom( - m_autil.mk_ge(cntInUnr, mk_int(1)), - mk_and(items)); - - // option 0 - expr_ref op0(ctx.mk_eq_atom(cntInUnr, mk_int(0)), mgr); - expr_ref ast1(ctx.mk_eq_atom(unrFunc, mk_string("")), mgr); - expr_ref ast2(ctx.mk_eq_atom(mk_strlen(unrFunc), mk_int(0)), mgr); - expr_ref and1(mgr.mk_and(ast1, ast2), mgr); - - // put together - toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert); - - unroll_var_map.insert(unrFunc, toAssert); - } - else { - toAssert = unroll_var_map[unrFunc]; - } - } - m_trail.push_back(toAssert); - assert_axiom(toAssert); - } - } - - }; // namespace smt From 0343377d8229317acceff3d5daa8f5c2876311da Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 5 May 2020 14:55:30 -0400 Subject: [PATCH 4/4] z3str3: remove unused methods and member variables --- src/smt/theory_str.cpp | 130 +---------------------------------------- src/smt/theory_str.h | 57 ------------------ 2 files changed, 3 insertions(+), 184 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1893b4eba7b..41cd97f9842 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -61,8 +61,6 @@ namespace smt { m_persisted_axiom_todo(m), tmpStringVarCount(0), tmpXorVarCount(0), - tmpLenTestVarCount(0), - tmpValTestVarCount(0), avoidLoopCut(true), loopDetected(false), m_theoryStrOverlapAssumption_term(m), @@ -110,21 +108,8 @@ namespace smt { //variable_set.reset(); //internal_variable_set.reset(); - //regex_variable_set.reset(); //internal_variable_scope_levels.clear(); - internal_lenTest_vars.reset(); - internal_valTest_vars.reset(); - internal_unrollTest_vars.reset(); - - input_var_in_len.reset(); - - fvar_len_count_map.reset(); - fvar_lenTester_map.reset(); - lenTester_fvar_map.reset(); - fvar_valueTester_map.reset(); - valueTester_fvar_map.reset(); - val_range_map.reset(); contains_map.reset(); contain_pair_bool_map.reset(); contain_pair_idx_map.reset(); @@ -150,18 +135,11 @@ namespace smt { concat_astNode_map.reset(); string_int_conversion_terms.reset(); string_int_axioms.reset(); - lengthTesterCache.reset(); - valueTesterCache.reset(); stringConstantCache.reset(); length_ast_map.reset(); //m_trail_stack.reset(); // m_find.reset(); - binary_search_len_tester_stack.reset(); - binary_search_len_tester_info.reset(); - binary_search_starting_len_tester.reset(); - binary_search_next_var_low.reset(); - binary_search_next_var_high.reset(); fixed_length_subterm_trail.reset(); fixed_length_assumptions.reset(); @@ -1916,94 +1894,6 @@ namespace smt { return regexIn; } - static zstring str2RegexStr(zstring str) { - zstring res(""); - int len = str.length(); - for (int i = 0; i < len; i++) { - char nc = str[i]; - // 12 special chars - if (nc == '\\' || nc == '^' || nc == '$' || nc == '.' || nc == '|' || nc == '?' - || nc == '*' || nc == '+' || nc == '(' || nc == ')' || nc == '[' || nc == '{') { - res = res + zstring("\\"); - } - char tmp[2] = {(char)str[i], '\0'}; - res = res + zstring(tmp); - } - return res; - } - - zstring theory_str::get_std_regex_str(expr * regex) { - app * a_regex = to_app(regex); - if (u.re.is_to_re(a_regex)) { - expr * regAst = a_regex->get_arg(0); - zstring regAstVal; - u.str.is_string(regAst, regAstVal); - zstring regStr = str2RegexStr(regAstVal); - return regStr; - } else if (u.re.is_concat(a_regex)) { - expr * reg1Ast = a_regex->get_arg(0); - expr * reg2Ast = a_regex->get_arg(1); - zstring reg1Str = get_std_regex_str(reg1Ast); - zstring reg2Str = get_std_regex_str(reg2Ast); - return zstring("(") + reg1Str + zstring(")(") + reg2Str + zstring(")"); - } else if (u.re.is_union(a_regex)) { - expr * reg1Ast = a_regex->get_arg(0); - expr * reg2Ast = a_regex->get_arg(1); - zstring reg1Str = get_std_regex_str(reg1Ast); - zstring reg2Str = get_std_regex_str(reg2Ast); - return zstring("(") + reg1Str + zstring(")|(") + reg2Str + zstring(")"); - } else if (u.re.is_star(a_regex)) { - expr * reg1Ast = a_regex->get_arg(0); - zstring reg1Str = get_std_regex_str(reg1Ast); - return zstring("(") + reg1Str + zstring(")*"); - } else if (u.re.is_range(a_regex)) { - expr * range1 = a_regex->get_arg(0); - expr * range2 = a_regex->get_arg(1); - zstring range1val, range2val; - u.str.is_string(range1, range1val); - u.str.is_string(range2, range2val); - return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); - } else if (u.re.is_loop(a_regex)) { - expr * body; - unsigned lo, hi; - // There are two variants of loop: a 2-argument version and a 3-argument version. - if (u.re.is_loop(a_regex, body, lo, hi)) { - rational rLo(lo); - rational rHi(hi); - zstring bodyStr = get_std_regex_str(body); - return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})"); - } else if (u.re.is_loop(a_regex, body, lo)) { - rational rLo(lo); - zstring bodyStr = get_std_regex_str(body); - return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring("+") + zstring("})"); - } - else { - TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); - UNREACHABLE(); return zstring(""); - } - } else if (u.re.is_full_seq(a_regex)) { - return zstring("(.*)"); - } else if (u.re.is_full_char(a_regex)) { - return zstring("str.allchar"); - } else if (u.re.is_intersection(a_regex)) { - expr * a0; - expr * a1; - u.re.is_intersection(a_regex, a0, a1); - zstring a0str = get_std_regex_str(a0); - zstring a1str = get_std_regex_str(a1); - return zstring("(") + a0str + zstring("&&") + a1str + zstring(")"); - } else if (u.re.is_complement(a_regex)) { - expr * body; - u.re.is_complement(a_regex, body); - zstring bodyStr = get_std_regex_str(body); - return zstring("(^") + bodyStr + zstring(")"); - } else { - TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); - UNREACHABLE(); return zstring(""); - } - - } - void theory_str::instantiate_axiom_RegexIn(enode * e) { ast_manager & m = get_manager(); @@ -7007,14 +6897,6 @@ namespace smt { // we also want to check whether we can eval this concat, // in case the rewriter did not totally finish with this term m_concat_eval_todo.push_back(n); - } else if (u.str.is_length(ap)) { - // if the argument is a variable, - // keep track of this for later, we'll need it during model gen - expr * var = ap->get_arg(0); - app * aVar = to_app(var); - if (aVar->get_num_args() == 0 && !u.str.is_string(aVar)) { - input_var_in_len.insert(var); - } } else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) { m_library_aware_axiom_todo.push_back(n); } else if (u.str.is_itos(ap)) { @@ -7365,10 +7247,7 @@ namespace smt { // check whether the node is a string variable; // testing set membership here bypasses several expensive checks. // note that internal variables don't count if they're only length tester / value tester vars. - if (variable_set.find(node) != variable_set.end() - && internal_lenTest_vars.find(node) == internal_lenTest_vars.end() - && internal_valTest_vars.find(node) == internal_valTest_vars.end() - && internal_unrollTest_vars.find(node) == internal_unrollTest_vars.end()) { + if (variable_set.find(node) != variable_set.end()) { if (varMap[node] != 1) { TRACE("str", tout << "new variable: " << mk_pp(node, get_manager()) << std::endl;); } @@ -8344,9 +8223,7 @@ namespace smt { void theory_str::collect_var_concat(expr * node, std::set & varSet, std::set & concatSet) { if (variable_set.find(node) != variable_set.end()) { - if (internal_lenTest_vars.find(node) == internal_lenTest_vars.end()) { - varSet.insert(node); - } + varSet.insert(node); } else if (is_app(node)) { app * aNode = to_app(node); @@ -8652,8 +8529,7 @@ namespace smt { if (vName.length() >= 3 && vName.substr(0, 3) == "$$_") continue; */ - if (internal_variable_set.find(itor->first) != internal_variable_set.end() - || regex_variable_set.find(itor->first) != regex_variable_set.end()) { + if (internal_variable_set.find(itor->first) != internal_variable_set.end()) { // this can be ignored, I think TRACE("str", tout << "free internal variable " << mk_pp(itor->first, m) << " ignored" << std::endl;); continue; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 9ce86361a3b..3d3208ca5a7 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -472,8 +472,6 @@ class theory_str : public theory { int tmpStringVarCount; int tmpXorVarCount; - int tmpLenTestVarCount; - int tmpValTestVarCount; // obj_pair_map > varForBreakConcat; std::map, std::map > varForBreakConcat; bool avoidLoopCut; @@ -484,27 +482,8 @@ class theory_str : public theory { obj_hashtable variable_set; obj_hashtable internal_variable_set; - obj_hashtable regex_variable_set; std::map > internal_variable_scope_levels; - obj_hashtable internal_lenTest_vars; - obj_hashtable internal_valTest_vars; - obj_hashtable internal_unrollTest_vars; - - obj_hashtable input_var_in_len; - - obj_map fvar_len_count_map; - obj_map > fvar_lenTester_map; - obj_map lenTester_fvar_map; - - - obj_map > > > fvar_valueTester_map; - - obj_map valueTester_fvar_map; - - obj_map val_range_map; - - expr_ref_vector contains_map; theory_str_contain_pair_bool_map_t contain_pair_bool_map; @@ -545,11 +524,6 @@ class theory_str : public theory { expr_ref_vector string_int_conversion_terms; obj_hashtable string_int_axioms; - // used when opt_FastLengthTesterCache is true - rational_map lengthTesterCache; - // used when opt_FastValueTesterCache is true - string_map valueTesterCache; - string_map stringConstantCache; unsigned long totalCacheAccessCount; unsigned long cacheHitCount; @@ -566,34 +540,6 @@ class theory_str : public theory { expr * get_eqc_next(expr * n); app * get_ast(theory_var i); - // binary search heuristic data - struct binary_search_info { - rational lowerBound; - rational midPoint; - rational upperBound; - rational windowSize; - - binary_search_info() : lowerBound(rational::zero()), midPoint(rational::zero()), - upperBound(rational::zero()), windowSize(rational::zero()) {} - binary_search_info(rational lower, rational mid, rational upper, rational windowSize) : - lowerBound(lower), midPoint(mid), upperBound(upper), windowSize(windowSize) {} - - void calculate_midpoint() { - midPoint = floor(lowerBound + ((upperBound - lowerBound) / rational(2)) ); - } - }; - // maps a free string var to a stack of active length testers. - // can use binary_search_trail to record changes to this object - obj_map > binary_search_len_tester_stack; - // maps a length tester var to the *active* search window - obj_map binary_search_len_tester_info; - // maps a free string var to the first length tester to be (re)used - obj_map binary_search_starting_len_tester; - // maps a length tester to the next length tester to be (re)used if the split is "low" - obj_map binary_search_next_var_low; - // maps a length tester to the next length tester to be (re)used if the split is "high" - obj_map binary_search_next_var_high; - // fixed length model construction expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver* expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these @@ -817,9 +763,6 @@ class theory_str : public theory { bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex); bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity); - // strRegex - zstring get_std_regex_str(expr * r); - void dump_assignments(); void initialize_charset();