diff --git a/README.md b/README.md index 959ea3aabf9..2b2ee6fec8a 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ For a brief overview of the architecture, see [SMT-COMP'24 Z3-Noodler descriptio ### Dependencies -1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.3`. +1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.6`. ```shell git clone 'https://github.com/VeriFIT/mata.git' cd mata @@ -47,16 +47,16 @@ make test-noodler ``` ### Running Z3-Noodler -To run Z3-Noodler, select Z3-Noodler as Z3's string solver when executing Z3. +To run Z3-Noodler, use: ```shell cd build/ -./z3 smt.string_solver=noodler +./z3 ``` -If you want to get a model for sat instances, you need to enable producing models (otherwise the resulting models are not usable). +If you want to get a model for sat instances (using `get-model` or `get-value`), you need to enable model generation: ```shell cd build/ -./z3 smt.string_solver=noodler smt.str.produce_models=true +./z3 model=true ``` However, model generation is highly experimental, the models might be invalid or they cannot be computed (yet). diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index a2757d955ba..0635eedf981 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -114,7 +114,7 @@ class get_model_cmd : public cmd { if (ctx.ignore_check()) return; if (!ctx.is_model_available(m) || !ctx.get_check_sat_result()) - throw cmd_exception("model is not available"); + throw cmd_exception("model is not available, did you forget to enable model generation with ''model=true'?"); if (m_index > 0 && ctx.get_opt()) { ctx.get_opt()->get_box_model(m, m_index); } @@ -129,7 +129,7 @@ class get_model_cmd : public cmd { ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { model_ref m; if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); + throw cmd_exception("model is not available, did you forget to enable model generation with 'model=true'?"); ctx.regular_stream() << "("; dictionary const & macros = ctx.get_macros(); bool first = true; diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 1d5d10b399c..98981d42034 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -175,7 +175,7 @@ void context_params::collect_param_descrs(param_descrs & d) { void context_params::collect_solver_param_descrs(param_descrs & d) { d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); - d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); + d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "false"); d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); } diff --git a/src/params/context_params.h b/src/params/context_params.h index 1f169a5bdda..4e20f3d9828 100644 --- a/src/params/context_params.h +++ b/src/params/context_params.h @@ -37,7 +37,7 @@ class context_params { bool m_debug_ref_count { false }; bool m_trace { false }; bool m_well_sorted_check { false }; - bool m_model { true }; + bool m_model { false }; bool m_model_validate { false }; bool m_dump_models { false }; bool m_unsat_core { false }; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 98323816ace..3fadcec7adb 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2685,7 +2685,7 @@ namespace smt2 { return; } if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == nullptr) - throw cmd_exception("model is not available"); + throw cmd_exception("model is not available, did you forget to enable model generation with 'model=true'?"); if (index != 0) { m_ctx.get_opt()->get_box_model(md, index); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4723d5e9c80..0f5d26219fe 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -113,7 +113,7 @@ def_module_params(module_name='smt', ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), - ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver), \'empty\' (a no-op solver that forces an answer unknown if strings were used), \'none\' (no solver)'), + ('string_solver', SYMBOL, 'noodler', 'solver for string/sequence theories. options are: \'noodler\' (Z3-Noodler string solver), \'z3str3\', \'seq\' (Z3 default solver), \'auto\' (use static features to choose best solver), \'empty\' (a no-op solver that forces an answer unknown if strings were used), \'none\' (no solver)'), ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), @@ -138,7 +138,6 @@ def_module_params(module_name='smt', ('str.preprocess_red', BOOL, False, 'use automata reduction eagerly in the preprocessing (Z3-Noodler only)'), ('str.try_nielsen', BOOL, True, 'use Nielsen reduction for quadratic formulas (Z3-Noodler only)'), ('str.underapprox_length', UINT, 5, 'maximum length of digit words used in underapproximating from_int/to_int conversions (Z3-Noodler only)'), - ('str.produce_models', BOOL, False, 'generate models (Z3-Noodler only)'), ('str.ca_constr', BOOL, False, 'use counter automata for solving extended string constraints (Z3-Noodler only)'), ('str.try_length_proc', BOOL, False, 'use length-based decision procedure (Z3-Noodler only)'), ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'), diff --git a/src/smt/params/theory_str_noodler_params.cpp b/src/smt/params/theory_str_noodler_params.cpp index e8d86bfa17c..9d1cdf25779 100644 --- a/src/smt/params/theory_str_noodler_params.cpp +++ b/src/smt/params/theory_str_noodler_params.cpp @@ -1,6 +1,7 @@ #include "smt/params/theory_str_noodler_params.h" #include "smt/params/smt_params_helper.hpp" +#include "util/gparams.h" void theory_str_noodler_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); @@ -10,8 +11,8 @@ void theory_str_noodler_params::updt_params(params_ref const & _p) { m_try_nielsen = p.str_try_nielsen(); m_try_length_proc = p.str_try_length_proc(); m_underapprox_length = p.str_underapprox_length(); - m_produce_models = p.str_produce_models(); m_ca_constr = p.str_ca_constr(); + m_produce_models = gparams::get_ref().get_bool("model", false); } #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; diff --git a/src/smt/theory_str_noodler/aut_assignment.cpp b/src/smt/theory_str_noodler/aut_assignment.cpp index c82930e9b3e..ca8f8f2eaa6 100644 --- a/src/smt/theory_str_noodler/aut_assignment.cpp +++ b/src/smt/theory_str_noodler/aut_assignment.cpp @@ -1,5 +1,6 @@ #include "aut_assignment.h" #include "util.h" +#include "regex.h" namespace smt::noodler { LenNode AutAssignment::get_lengths(const BasicTerm& var) const { @@ -188,4 +189,42 @@ namespace smt::noodler { aut.tarjan_scc_discover(callback); return flat; } + + void AutAssignment::add_symbol_from_dummy(mata::Symbol sym) { + if(alphabet.contains(sym)) { return; } + bool is_there_some_dummy = false; + for (auto& [var, nfa] : *this) { + for (mata::nfa::State state = 0; state < nfa->num_of_states(); ++state) { + const mata::nfa::StatePost& delta_from_state = nfa->delta[state]; + if (!delta_from_state.empty() && delta_from_state.back().symbol == util::get_dummy_symbol()) { // dummy symbol should be largest (we do not have epsilons), so should be at the back + is_there_some_dummy = true; + nfa->delta.add(state, sym, nfa->delta[state].back().targets); + } + } + } + if (is_there_some_dummy) { + alphabet.insert(sym); + } + } + + void AutAssignment::replace_dummy_with_new_symbol() { + mata::Symbol new_symbol = regex::Alphabet(alphabet).get_unused_symbol(); + bool is_there_some_dummy = false; + for (auto& [var, nfa] : *this) { + for (mata::nfa::State state = 0; state < nfa->num_of_states(); ++state) { + if (!nfa->delta[state].empty()) { // if there is some transition from state + mata::nfa::StatePost& delta_from_state = nfa->delta.mutable_state_post(state); // then we can for sure get mutable transitions from state without side effect + if (delta_from_state.back().symbol == util::get_dummy_symbol()) { // dummy symbol should be largest (we do not have epsilons), so should be at the back + is_there_some_dummy = true; + mata::nfa::StateSet targets = delta_from_state.back().targets; + delta_from_state.pop_back(); + nfa->delta.add(state, new_symbol, targets); + } + } + } + } + if (is_there_some_dummy) { + alphabet.insert(new_symbol); + } + } } diff --git a/src/smt/theory_str_noodler/aut_assignment.h b/src/smt/theory_str_noodler/aut_assignment.h index ca25ea28965..2cdeefcc9eb 100644 --- a/src/smt/theory_str_noodler/aut_assignment.h +++ b/src/smt/theory_str_noodler/aut_assignment.h @@ -194,6 +194,12 @@ namespace smt::noodler { } } + /// @brief Add symbol @p s to alphabet and removes it from dummy symbol (i.e. adds transitions trough @p s in all automata if there is transition trough dummy symbol) + void add_symbol_from_dummy(mata::Symbol s); + + /// @brief Replace dummy symbol in all automata by a new symbol + void replace_dummy_with_new_symbol(); + /** * @brief Is language complement of a finite language? * diff --git a/src/smt/theory_str_noodler/decision_procedure.cpp b/src/smt/theory_str_noodler/decision_procedure.cpp index 41ba970ebf0..7c9b279384b 100644 --- a/src/smt/theory_str_noodler/decision_procedure.cpp +++ b/src/smt/theory_str_noodler/decision_procedure.cpp @@ -1393,9 +1393,10 @@ namespace smt::noodler { // Refresh the instance this->formula = prep_handler.get_modified_formula(); this->init_aut_ass = prep_handler.get_aut_assignment(); + this->init_substitution_map = prep_handler.get_substitution_map(); this->init_length_sensitive_vars = prep_handler.get_len_variables(); this->preprocessing_len_formula = prep_handler.get_len_formula(); - this->inclusions_from_preprocessing = prep_handler.get_removed_equations(); + this->inclusions_from_preprocessing = prep_handler.get_removed_inclusions_for_model(); if (!this->init_aut_ass.is_sat()) { // some automaton in the assignment is empty => we won't find solution @@ -1560,14 +1561,6 @@ namespace smt::noodler { mata::nfa::Nfa len_nfa = solution.aut_ass.sigma_automaton_of_length(len.get_unsigned()); nfa = std::make_shared(mata::nfa::intersection(*nfa, len_nfa).trim()); - // Restrict code-conversion var - if (code_subst_vars.contains(var)) { - rational to_code_value = get_arith_model_of_var(code_version_of(var)); - if (to_code_value != -1) { - update_model_and_aut_ass(var, zstring(to_code_value.get_unsigned())); // zstring(unsigned) returns char with the code point of the argument - } // for the case to_code_value == -1 we shoulh have (str.len var) != 1, so we do not need to restrict the language, as it should have been done in restrict_languages_to_lengths() - } - // Restrict int-conversion var if (int_subst_vars.contains(var)) { if (len == 0) { @@ -1591,7 +1584,19 @@ namespace smt::noodler { } } } + + // Restrict code-conversion var + if (code_subst_vars.contains(var)) { + rational to_code_value = get_arith_model_of_var(code_version_of(var)); + if (to_code_value != -1) { + solution.aut_ass.add_symbol_from_dummy(to_code_value.get_unsigned()); + update_model_and_aut_ass(var, zstring(to_code_value.get_unsigned())); // zstring(unsigned) returns char with the code point of the argument + } // for the case to_code_value == -1 we shoulh have (str.len var) != 1, so we do not need to restrict the language, as it should have been already be restricted by lenght + } } + + // we remove dummy symbol from automata, so we do not have to work with it + solution.aut_ass.replace_dummy_with_new_symbol(); is_model_initialized = true; @@ -1627,6 +1632,10 @@ namespace smt::noodler { return model_of_var.at(var); } + if (vars_whose_model_we_are_computing.contains(var)) { + util::throw_error("There is cycle in inclusion graph, cannot produce model"); + } + STRACE("str-model", tout << "Generating model for var " << var; if (solution.length_sensitive_vars.contains(var)) { @@ -1635,6 +1644,8 @@ namespace smt::noodler { tout << "\n"; ); + vars_whose_model_we_are_computing.insert(var); + regex::Alphabet alph(solution.aut_ass.get_alphabet()); if (solution.substitution_map.contains(var)) { @@ -1646,9 +1657,9 @@ namespace smt::noodler { } else if (solution.aut_ass.contains(var)) { Predicate inclusion_with_var_on_right_side; if (solution.get_inclusion_with_var_on_right_side(var, inclusion_with_var_on_right_side)) { - // TODO check if inclusion_with_var_on_right_side lays on a cycle (needs to be - // implemented solution.is_inclusion_on_cycle() is overapproximation) + // TODO check if inclusion_with_var_on_right_side lays on a cycle. // If it is on a cycle, then we need to use (and implement) the horrible proof (righ now the following will never finish) + // Right now if there is some cycle (checked using vars_whose_model_we_are_computing), we throw error. // We need to compute the vars on the right side from the vars on the left // - first we get the string model of the left side @@ -1669,34 +1680,67 @@ namespace smt::noodler { } else { std::vector>left_side_string_aut{std::make_shared(solution.aut_ass.create_word_nfa(left_side_string))}; + const auto& vars_on_right_side = inclusion_with_var_on_right_side.get_right_side(); // becase inclusion is not on cycle, all variables on the right side must be different std::vector> automata_on_right_side; - for (const auto &right_side_var : inclusion_with_var_on_right_side.get_right_side()) { + for (const auto &right_side_var : vars_on_right_side) { automata_on_right_side.push_back(solution.aut_ass.at(right_side_var)); } + SASSERT(vars_on_right_side.size() == automata_on_right_side.size()); auto noodles = mata::strings::seg_nfa::noodlify_for_equation(automata_on_right_side, left_side_string_aut, - true, + false, {{"reduce", "forward"}}); SASSERT(!noodles.empty()); - SASSERT(automata_on_right_side.size() == noodles[0].size()); - unsigned i = 0; - for (const auto &right_side_var : inclusion_with_var_on_right_side.get_right_side()) { - if (right_side_var.is_literal()) { continue; } - // becase inclusion is not on cycle, all variables on the right side must be different - zstring right_side_var_string = alph.get_string_from_mata_word(*(noodles[0][i].first->get_word())); - update_model_and_aut_ass(right_side_var, right_side_var_string); - ++i; + STRACE("str-model-noodlification", + tout << "Noodlification before and after in model generation:" << std::endl; + tout << "Left side automaton for concatenation "; + for (const auto& var_on_left_side : inclusion_with_var_on_right_side.get_left_side()) { + tout << " " << var_on_left_side; + } + tout << ":\n" << *left_side_string_aut[0]; + tout << "Right side automata:" << std::endl; + for (unsigned i = 0; i < vars_on_right_side.size(); ++i) { + tout << "Variable " << vars_on_right_side[i] << ":\n" << *automata_on_right_side[i]; + } + tout << "Noodle:\n"; + for (const auto &noodle_aut : noodles[0]) { + tout << "Automaton for right var with index " << noodle_aut.second[0] << ":\n"; + tout << *noodle_aut.first; + } + ); + unsigned index_of_right_var_that_is_not_yet_processed = 0; + for (const auto &noodle_aut : noodles[0]) { // we can take any noodle, so we take the first one + // noodle_aut.second[0] is the index of the right var whose automaton is noodle_aut.first (see compute_next_solution() for better explanation) + unsigned index_of_right_var_that_belongs_to_noodle_aut = noodle_aut.second[0]; + while (index_of_right_var_that_is_not_yet_processed < index_of_right_var_that_belongs_to_noodle_aut) { + // skipped vars means that they are empty strings + BasicTerm right_var_that_is_not_yet_processed = vars_on_right_side[index_of_right_var_that_is_not_yet_processed]; + update_model_and_aut_ass(right_var_that_is_not_yet_processed, zstring()); + ++index_of_right_var_that_is_not_yet_processed; + } + // update model based on noodle_aut + BasicTerm right_var_that_belongs_to_noodle_aut = vars_on_right_side[index_of_right_var_that_belongs_to_noodle_aut]; + if (!right_var_that_belongs_to_noodle_aut.is_literal()) { + zstring right_side_var_string = alph.get_string_from_mata_word(noodle_aut.first->get_word().value()); + SASSERT(index_of_right_var_that_is_not_yet_processed == index_of_right_var_that_belongs_to_noodle_aut); + update_model_and_aut_ass(right_var_that_belongs_to_noodle_aut, right_side_var_string); + } + ++index_of_right_var_that_is_not_yet_processed; + } + while (index_of_right_var_that_is_not_yet_processed < vars_on_right_side.size()) { + BasicTerm right_var_that_is_not_yet_processed = vars_on_right_side[index_of_right_var_that_is_not_yet_processed]; + update_model_and_aut_ass(right_var_that_is_not_yet_processed, zstring()); + ++index_of_right_var_that_is_not_yet_processed; } } return model_of_var.at(var); } else { // var is only on the left side in the inclusion graph => we can return whatever - - // TODO replace following with function that returns arbitary word from Mata zstring result; const auto& nfa = solution.aut_ass.at(var); - mata::Word accepted_word = *(nfa->get_word()); + STRACE("str-model-nfa", tout << "NFA for var " << var << " before getting some word:\n" << *nfa;); + mata::Word accepted_word = nfa->get_word().value(); return update_model_and_aut_ass(var, alph.get_string_from_mata_word(accepted_word)); } } else { diff --git a/src/smt/theory_str_noodler/decision_procedure.h b/src/smt/theory_str_noodler/decision_procedure.h index 5b1187247b1..b35a4c4bd6a 100644 --- a/src/smt/theory_str_noodler/decision_procedure.h +++ b/src/smt/theory_str_noodler/decision_procedure.h @@ -434,6 +434,8 @@ namespace smt::noodler { // keeps already computed models std::map model_of_var; + // vars for which we already called get_model() at least once (used for cyclicity detection, will be removed when get_model() can handle cycles in inclusions) + std::set vars_whose_model_we_are_computing; /** * @brief Update the model and its language in the solution of the variable @p var to @p computed_model @@ -445,9 +447,9 @@ namespace smt::noodler { zstring update_model_and_aut_ass(BasicTerm var, zstring computed_model) { model_of_var[var] = computed_model; if (solution.aut_ass.contains(var)) { - SASSERT(!mata::nfa::intersection(AutAssignment::create_word_nfa(computed_model), *solution.aut_ass[var]).is_lang_empty()); solution.aut_ass[var] = std::make_shared(AutAssignment::create_word_nfa(computed_model)); } + STRACE("str-model-res", tout << "Model for " << var << ": " << computed_model << std::endl); return computed_model; }; diff --git a/src/smt/theory_str_noodler/formula_preprocess.cpp b/src/smt/theory_str_noodler/formula_preprocess.cpp index f2fb569a6ac..d326f2ef760 100644 --- a/src/smt/theory_str_noodler/formula_preprocess.cpp +++ b/src/smt/theory_str_noodler/formula_preprocess.cpp @@ -306,6 +306,7 @@ namespace smt::noodler { * @param disallowed_vars - if any of these var occurs in equation, it cannot be removed */ void FormulaPreprocessor::remove_regular(const std::unordered_set& disallowed_vars) { + STRACE("str-prep", tout << "Preprocessing step - remove_regular\n";); std::vector> regs; this->formula.get_side_regulars(regs); std::deque> worklist(regs.begin(), regs.end()); @@ -323,7 +324,7 @@ namespace smt::noodler { continue; } - // if right side contains len vars (except when we have X = Y), we must do splitting => cannot remove + // if right side contains multiple len vars we must do splitting => cannot remove (we can remove if we have only one length var with possibly literals) bool is_right_side_len = !set_disjoint(this->len_variables, pr.second.get_side_vars(Predicate::EquationSideType::Right)); if(pr.second.get_side_vars(Predicate::EquationSideType::Right).size() > 1 && is_right_side_len) { continue; @@ -337,14 +338,10 @@ namespace smt::noodler { // we propagate the lengthness of right side variable to the left side this->len_variables.insert(left_var); // and add len constraint |X| = |Y| - this->add_to_len_formula(pr.second.get_formula_eq()); - - // we do not add this equation to removed_equation, instead we add Y to substitution map - BasicTerm right_var = pr.second.get_right_side()[0]; - substitution_map[right_var] = {left_var}; // subst_map[Y] = X (the length constraint |X| = |Y| is already there) - } else { - removed_equations.push_back(pr.second); + this->add_to_len_formula(pr.second.get_formula_eq()); } + + removed_inclusions_for_model.push_back(pr.second); this->formula.remove_predicate(pr.first); STRACE("str-prep-remove_regular", tout << "removed" << std::endl;); @@ -362,6 +359,7 @@ namespace smt::noodler { } } } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -369,6 +367,7 @@ namespace smt::noodler { * (find all Y in the formula and replace with X). */ void FormulaPreprocessor::propagate_variables() { + STRACE("str-prep", tout << "Preprocessing step - propagate_variables\n";); std::vector> regs; this->formula.get_simple_eqs(regs); std::deque worklist; @@ -421,12 +420,12 @@ namespace smt::noodler { for(const auto& pr : this->formula.get_predicates()) { map_set_insert(this->dependency, pr.first, index); } - - STRACE("str", tout << "propagate_variables\n";); } // Not true: you can have equation of two, literals which is not removed //assert(!this->formula.contains_simple_eqs()); + + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -507,6 +506,7 @@ namespace smt::noodler { * (b) X1 X X2 = Z and Z = X1 Y X2 => X = Y. Where each term can be both literal and variable. */ void FormulaPreprocessor::generate_identities() { + STRACE("str-prep", tout << "Preprocessing step - generate_identities\n";); std::set> new_preds; std::set rem_ids; size_t index = this->formula.get_max_index() + 1; @@ -557,6 +557,7 @@ namespace smt::noodler { for(const auto &pr : new_preds) { this->formula.add_predicate(pr.second, pr.first); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -649,6 +650,7 @@ namespace smt::noodler { * @param mn Minimum number of occurrences of a regular sequence to be replaced with a fresh variable. */ void FormulaPreprocessor::reduce_regular_sequence(unsigned mn) { + STRACE("str-prep", tout << "Preprocessing step - reduce_regular_sequence\n";); std::map regs; std::set new_eqs; get_regular_sublists(regs); @@ -666,6 +668,7 @@ namespace smt::noodler { this->formula.add_predicate(eq); // We do not add dependency } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -694,6 +697,7 @@ namespace smt::noodler { * literal remove from the formula and set the corresponding languages appropriately. */ void FormulaPreprocessor::propagate_eps() { + STRACE("str-prep", tout << "Preprocessing step - propagate_eps\n";); std::set eps_set; get_eps_terms(eps_set); std::deque worklist; @@ -752,7 +756,7 @@ namespace smt::noodler { this->dependency[pr.first].insert(eps_eq_id.begin(), eps_eq_id.end()); } - + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -825,6 +829,7 @@ namespace smt::noodler { * @brief Separate equations. */ void FormulaPreprocessor::separate_eqs() { + STRACE("str-prep", tout << "Preprocessing step - separate_eqs\n";); std::set add_eqs; std::set rem_ids; @@ -848,7 +853,7 @@ namespace smt::noodler { for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } - + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -883,6 +888,7 @@ namespace smt::noodler { * the end of the equation). */ void FormulaPreprocessor::remove_extension() { + STRACE("str-prep", tout << "Preprocessing step - remove_extension\n";); std::set begin_star, end_star; gather_extended_vars(Predicate::EquationSideType::Left, begin_star); gather_extended_vars(Predicate::EquationSideType::Right, end_star); @@ -965,12 +971,14 @@ namespace smt::noodler { for(const auto& pr : updates) { this->update_predicate(pr.first, pr.second); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** * @brief Remove trivial equations of the form X = X */ void FormulaPreprocessor::remove_trivial() { + STRACE("str-prep", tout << "Preprocessing step - remove_trivial\n";); std::set rem_ids; for(const auto& pr : this->formula.get_predicates()) { if(!pr.second.is_equation()) @@ -984,6 +992,7 @@ namespace smt::noodler { for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1037,6 +1046,7 @@ namespace smt::noodler { * variables but also literals. */ void FormulaPreprocessor::refine_languages() { + STRACE("str-prep", tout << "Preprocessing step - refine_languages\n";); std::set ineq_vars; for(const auto& pr : this->formula.get_predicates()) { if(!pr.second.is_inequation()) @@ -1083,6 +1093,7 @@ namespace smt::noodler { this->aut_ass[pr.first] = std::make_shared(mata::nfa::reduce(inters)); } } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1090,6 +1101,7 @@ namespace smt::noodler { * Remove L=R if single_occur(R) and L(R) = \Sigma^*. */ void FormulaPreprocessor::skip_len_sat() { + STRACE("str-prep", tout << "Preprocessing step - skip_len_sat\n";); std::set rem_ids; auto is_sigma_star = [&](const std::set& bts) { @@ -1110,24 +1122,46 @@ namespace smt::noodler { auto left_set = pr.second.get_left_set(); if(left_set.size() > 0 && is_sigma_star(left_set)) { rem_ids.insert(pr.first); - // we add the removed equation to removed_equations, but we have to swap + this->add_to_len_formula(pr.second.get_formula_eq()); + // we add the removed equation to removed_inclusions_for_model, but we have to swap // sides so that the single occurring side is on the right (we are gonna // pretend it is an inclusion and from left side compute the vars of // the right side in the model generation) - removed_equations.push_back(pr.second.get_switched_sides_predicate()); + removed_inclusions_for_model.push_back(pr.second.get_switched_sides_predicate()); + + // if we need to produce models and left side contains some length variable, + // we need to make all variables on the right side length too, so that we + // select the correct lengths during the model generation + if (!set_disjoint(this->len_variables, pr.second.get_side_vars(Predicate::EquationSideType::Left)) + && m_params.m_produce_models) { + for (BasicTerm right_var : pr.second.get_side_vars(Predicate::EquationSideType::Right)) { + len_variables.insert(right_var); + } + } } } if(this->formula.single_occurr(pr.second.get_right_set())) { auto right_set = pr.second.get_right_set(); if(right_set.size() > 0 && is_sigma_star(right_set)) { rem_ids.insert(pr.first); - removed_equations.push_back(pr.second); + this->add_to_len_formula(pr.second.get_formula_eq()); + removed_inclusions_for_model.push_back(pr.second); + // if we need to produce models and right side contains some length variable, + // we need to make all variables on the left side length too, so that we + // select the correct lengths during the model generation + if (!set_disjoint(this->len_variables, pr.second.get_side_vars(Predicate::EquationSideType::Right)) + && m_params.m_produce_models) { + for (BasicTerm left_var : pr.second.get_side_vars(Predicate::EquationSideType::Left)) { + len_variables.insert(left_var); + } + } } } } for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1137,6 +1171,7 @@ namespace smt::noodler { * @param ec Equivalence class containing length-equivalent variables. */ void FormulaPreprocessor::generate_equiv(const BasicTermEqiv& ec) { + STRACE("str-prep", tout << "Preprocessing step - generate_equiv\n";); std::set new_preds; size_t index = this->formula.get_max_index() + 1; @@ -1197,6 +1232,7 @@ namespace smt::noodler { for(const auto &pr : new_preds) { this->formula.add_predicate(pr); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1230,6 +1266,7 @@ namespace smt::noodler { * W = Z1 "A" Z3 where "A" not in L(Y1) and "A" not in L(Z1) */ void FormulaPreprocessor::infer_alignment() { + STRACE("str-prep", tout << "Preprocessing step - infer_alignment\n";); using VarSeparator = std::map>; // separators for each variable: map of literals -> set of basic terms: // for each literal (L) contains terms (T) that preceeds that literal: there is equation ... = T L @@ -1269,6 +1306,7 @@ namespace smt::noodler { } } } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1327,6 +1365,7 @@ namespace smt::noodler { * infer Y = W3 W4 */ void FormulaPreprocessor::common_prefix_propagation() { + STRACE("str-prep", tout << "Preprocessing step - common_prefix_propagation\n";); TermReplaceMap replace_map = construct_replace_map(); std::set rem_ids; size_t i = 0; @@ -1374,6 +1413,7 @@ namespace smt::noodler { for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1389,6 +1429,7 @@ namespace smt::noodler { * infer Y = W3 W4 */ void FormulaPreprocessor::common_suffix_propagation() { + STRACE("str-prep", tout << "Preprocessing step - common_suffix_propagation\n";); TermReplaceMap replace_map = construct_replace_map(); std::set rem_ids; int i = 0, j = 0; @@ -1438,6 +1479,7 @@ namespace smt::noodler { for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1486,6 +1528,7 @@ namespace smt::noodler { * setting their languages to \Sigma^*. */ void FormulaPreprocessor::underapprox_languages() { + STRACE("str-prep", tout << "Preprocessing step - underapprox_languages\n";); for(const Predicate& pred : this->formula.get_predicates_set()) { for(const BasicTerm& var : pred.get_vars()) { if(this->aut_ass.is_co_finite(var)) { @@ -1497,12 +1540,14 @@ namespace smt::noodler { } } } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** * @brief Reduce the number of diseqalities. */ void FormulaPreprocessor::reduce_diseqalities() { + STRACE("str-prep", tout << "Preprocessing step - reduce_diseqalities\n";); std::set rem_ids; for(const auto& pr : this->formula.get_predicates()) { @@ -1547,6 +1592,7 @@ namespace smt::noodler { for(const size_t & i : rem_ids) { this->formula.remove_predicate(i); } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1640,6 +1686,7 @@ namespace smt::noodler { * @param conversions */ void FormulaPreprocessor::conversions_validity(std::vector& conversions) { + STRACE("str-prep", tout << "Preprocessing step - conversions_validity\n";); mata::nfa::Nfa sigma_aut = aut_ass.sigma_automaton(); mata::nfa::Nfa only_digits_aut = AutAssignment::digit_automaton(); @@ -1650,6 +1697,7 @@ namespace smt::noodler { len_formula.succ.emplace_back(LenFormulaType::EQ, std::vector{conv.int_var, -1}); } } + STRACE("str-prep", tout << print_info(is_trace_enabled("str-nfa"))); } /** @@ -1711,4 +1759,40 @@ namespace smt::noodler { return true; } + std::string FormulaPreprocessor::print_info(bool print_nfas) { + std::stringstream res; + res << "Current formula:\n"; + for (const auto& pred : formula.get_predicates_set()) { + res << pred << std::endl; + } + res << "Current automata assignment:\n"; + for (const auto& [var, nfa] : aut_ass) { + res << var << " -> "; + if (print_nfas) { + res << std::endl << *nfa; + } else { + res << "NFA\n"; + } + } + res << "Current substition map:\n"; + for (const auto& [var, subst] : substitution_map) { + res << var << " ->"; + for (const auto& subst_var : subst) { + res << " " << subst_var; + } + res << std::endl; + } + res << "Current removed equations:\n"; + for (const auto& rem_eq : removed_inclusions_for_model) { + res << rem_eq << std::endl; + } + res << "Current length vars:"; + for (const auto& len_var : len_variables) { + res << " " << len_var; + } + res << std::endl; + res << "Current length formula: " << len_formula << std::endl; + return res.str(); + } + } // Namespace smt::noodler. diff --git a/src/smt/theory_str_noodler/formula_preprocess.h b/src/smt/theory_str_noodler/formula_preprocess.h index ae5c41ecaf9..999bbcf8266 100644 --- a/src/smt/theory_str_noodler/formula_preprocess.h +++ b/src/smt/theory_str_noodler/formula_preprocess.h @@ -314,9 +314,9 @@ namespace smt::noodler { AutAssignment aut_ass; std::unordered_map> substitution_map; - // keeps equations that were removed during preprocessing and are needed to generate model + // keeps equations that were removed during preprocessing as inclusions that are needed to generate model // (the variables on the right should be propagated from the left variables during model generation) - std::vector removed_equations; + std::vector removed_inclusions_for_model; LenNode len_formula; std::unordered_set len_variables; @@ -347,6 +347,8 @@ namespace smt::noodler { bool can_unify(const Concat& con1, const Concat& con2, const std::function &check) const; TermReplaceMap construct_replace_map() const; + std::string print_info(bool print_nfas = false); + public: FormulaPreprocessor(Formula conj, AutAssignment ass, std::unordered_set lv, const theory_str_noodler_params &par) : @@ -363,12 +365,13 @@ namespace smt::noodler { void get_regular_sublists(std::map& res) const; void get_eps_terms(std::set& res) const; const AutAssignment& get_aut_assignment() const { return this->aut_ass; } + const std::unordered_map>& get_substitution_map() const { return this->substitution_map; } const Dependency& get_dependency() const { return this->dependency; } Dependency get_flat_dependency() const; void add_to_len_formula(LenNode len_to_add) { len_formula.succ.push_back(std::move(len_to_add)); } const LenNode& get_len_formula() const { return this->len_formula; } const std::unordered_set& get_len_variables() const { return this->len_variables; } - const std::vector& get_removed_equations() const {return this->removed_equations; } + const std::vector& get_removed_inclusions_for_model() const {return this->removed_inclusions_for_model; } Formula get_modified_formula() const; @@ -386,6 +389,7 @@ namespace smt::noodler { void infer_alignment(); void common_prefix_propagation(); void common_suffix_propagation(); + void conversions_validity(std::vector& conversions); void refine_languages(); void reduce_diseqalities(); @@ -401,7 +405,6 @@ namespace smt::noodler { */ bool can_unify_not_contains(); - void conversions_validity(std::vector& conversions); /** * @brief Construct constraints to get rid of not_contains predicates. * @return false -> unsatisfiable constaint; true if it is not evident diff --git a/src/smt/theory_str_noodler/memb_heuristics_procedures.cpp b/src/smt/theory_str_noodler/memb_heuristics_procedures.cpp index 638d8acf546..880cc68d6ba 100644 --- a/src/smt/theory_str_noodler/memb_heuristics_procedures.cpp +++ b/src/smt/theory_str_noodler/memb_heuristics_procedures.cpp @@ -137,12 +137,16 @@ namespace smt::noodler { zstring MultMembHeuristicProcedure::get_model(BasicTerm var, const std::function& get_arith_model_of_var) { STRACE("str-mult-memb-heur", tout << "getting model for " << var << std::endl;); SASSERT(unions.contains(var) || intersections.contains(var)); + mata::Word word; if (unions.contains(var)) { - // TODO: add support for getting some word from "intersections[var] \intersect \neg unions[var]" on the fly - util::throw_error("Unsupported for now"); + if (intersections.contains(var)) { + word = mata::nfa::get_word_from_lang_difference(intersections.at(var), unions.at(var)).value(); + } else { + word = unions.at(var).get_word_from_complement(&alph.mata_alphabet).value(); + } + } else { + word = intersections.at(var).get_word().value(); } - - mata::Word word = *(intersections.at(var).get_word()); return alph.get_string_from_mata_word(word); } } diff --git a/src/smt/theory_str_noodler/regex.h b/src/smt/theory_str_noodler/regex.h index 4796216ca7d..c42e5c5d8cb 100644 --- a/src/smt/theory_str_noodler/regex.h +++ b/src/smt/theory_str_noodler/regex.h @@ -54,8 +54,7 @@ namespace smt::noodler::regex { }; /** - * @brief Alphabet wrapper for Z3 alphabet represented by - * std::set and a Mata alphabet. + * @brief Alphabet wrapper for Z3 alphabet represented by std::set and a Mata alphabet. */ struct Alphabet { std::set alphabet; @@ -87,7 +86,7 @@ namespace smt::noodler::regex { } /// @brief Return zstring corresponding the the word @p word, where dummy symbol is replaced with some valid symbol not in the alphabet. - zstring get_string_from_mata_word(mata::Word word) const { + zstring get_string_from_mata_word(const mata::Word& word) const { zstring res; mata::Symbol unused_symbol = get_unused_symbol(); for (mata::Symbol s : word) { diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index abb2116115f..eee667e3925 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -813,7 +813,9 @@ namespace smt::noodler { // As a heuristic, for the case we have exactly one constraint, which is of type 'x (not)in RE', we use universality/emptiness // checking of the regex (using some heuristics) instead of constructing the automaton of RE. The construction (especially complement) // can sometimes blow up, so the check should be faster. - if(this->m_membership_todo_rel.size() == 1 && !contains_word_equations && !contains_word_disequations && !contains_conversions && this->m_not_contains_todo_rel.size() == 0) { + if(this->m_membership_todo_rel.size() == 1 && !contains_word_equations && !contains_word_disequations && !contains_conversions && this->m_not_contains_todo_rel.size() == 0 + && this->len_vars.empty() // TODO: handle length vars that are not x (i.e., there are no string constraints on them, other than length ones, we just need to compute arith model) + ) { const auto& reg_data = this->m_membership_todo_rel[0]; // TODO: check if "xyz in RE" works correctly expr_ref var = std::get<0>(reg_data); @@ -888,6 +890,7 @@ namespace smt::noodler { if(symbols_in_formula.size() == 2 && !contains_word_disequations && !contains_conversions && this->m_not_contains_todo_rel.size() == 0 && this->m_membership_todo_rel.empty()) { // dummy symbol + 1 lbool result = run_length_sat(instance, aut_assignment, init_length_sensitive_vars, conversions); if(result == l_true) { + last_run_was_sat = true; return FC_DONE; } else if(result == l_false) { return FC_CONTINUE; @@ -898,6 +901,8 @@ namespace smt::noodler { if(m_params.m_try_nielsen && is_nielsen_suitable(instance, init_length_sensitive_vars)) { lbool result = run_nielsen(instance, aut_assignment, init_length_sensitive_vars); if(result == l_true) { + last_run_was_sat = true; + propagate_lengths_from_arith_model(); return FC_DONE; } else if(result == l_false) { return FC_CONTINUE; @@ -929,6 +934,8 @@ namespace smt::noodler { if(m_params.m_try_length_proc && contains_eqs_and_diseqs_only && LengthDecisionProcedure::is_suitable(instance, aut_assignment)) { lbool result = run_length_proc(instance, aut_assignment, init_length_sensitive_vars); if(result == l_true) { + last_run_was_sat = true; + propagate_lengths_from_arith_model(); return FC_DONE; } else if(result == l_false) { return FC_CONTINUE; @@ -940,6 +947,8 @@ namespace smt::noodler { STRACE("str", tout << "Try underapproximation" << std::endl); if (solve_underapprox(instance, aut_assignment, init_length_sensitive_vars, conversions) == l_true) { STRACE("str", tout << "Sat from underapproximation" << std::endl;); + last_run_was_sat = true; + propagate_lengths_from_arith_model(); return FC_DONE; } STRACE("str", tout << "Underapproximation did not help\n";); @@ -983,6 +992,7 @@ namespace smt::noodler { if (is_lengths_sat == l_true) { STRACE("str", tout << "len sat " << mk_pp(lengths, m) << std::endl;); last_run_was_sat = true; + propagate_lengths_from_arith_model(); if(precision == LenNodePrecision::OVERAPPROX) { ctx.get_fparams().is_overapprox = true; @@ -1019,6 +1029,7 @@ namespace smt::noodler { zstring theory_str_noodler::model_of_string_expr(app* str_expr) { // function that returns either the length of str var or model of int var from arith_model std::function get_arith_model_of_var = [this](BasicTerm var) -> rational { + SASSERT(arith_model != nullptr); expr_ref arg(m); // the following is similar to code in util::len_to_expr() if(!var_name.contains(var)) { @@ -1036,6 +1047,7 @@ namespace smt::noodler { arith_model->eval_expr(arg, model); bool is_int; rational val(0); + STRACE("str-arith-model", tout << "Model for " << mk_pp(arg, m) << std::flush << " is " << mk_pp(model, m) << std::endl;); VERIFY(m_util_a.is_numeral(model, val, is_int) && is_int); return val; }; @@ -1050,17 +1062,23 @@ namespace smt::noodler { // for relevant (string) var, we get the model from the decision procedure that returned sat return dec_proc->get_model(var, get_arith_model_of_var); } else { - // for non-relevant, we cannot get them from the decision procedure, but because they are not relevant, we can return anything (restricted by length) - // to get length, we cannot use get_arith_model_of_var, because it works with var_name, that contains only relevant vars - expr_ref model(m); - arith_model->eval_expr(m_util_s.str.mk_length(str_expr), model); - bool is_int; - rational val(0); - VERIFY(m_util_a.is_numeral(model, val, is_int) && is_int); - while (res.length() != val.get_unsigned()) { - res = res + zstring("a"); // we can return anything, so we will just fill it with 'a' + // for non-relevant, we cannot get them from the decision procedure, but because they are not relevant, we can return anything (restricted by length, if it is length var) + if (len_vars.contains(str_expr)) { + // to get length, we cannot use get_arith_model_of_var, because it works with var_name, that contains only relevant vars + SASSERT(arith_model != nullptr); + expr_ref model(m); + arith_model->eval_expr(m_util_s.str.mk_length(str_expr), model); + bool is_int; + rational val(0); + VERIFY(m_util_a.is_numeral(model, val, is_int) && is_int); + while (res.length() != val.get_unsigned()) { + res = res + zstring("a"); // we can return anything, so we will just fill it with 'a' + } + return res; + } else { + // we return empty string for non-relevant non-length vars, their value does not matter + return zstring(); } - return res; } } else if (m_util_s.str.is_concat(str_expr)) { // for concatenation, we just recursively get the models for arguments and then concatenate them @@ -1111,7 +1129,8 @@ namespace smt::noodler { } void theory_str_noodler::init_model(model_generator &mg) { - STRACE("str", tout << "init_model\n";); + STRACE("str", tout << "init_model\n"); + CTRACE("str-arith-model", arith_model != nullptr, tout << "Arith model:\n" << *arith_model << std::endl;); } void theory_str_noodler::finalize_model(model_generator &mg) { diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index 4418376c013..a978ab8a2fd 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -355,6 +355,9 @@ namespace smt::noodler { */ void block_curr_len(expr_ref len_formula, bool add_axiomatized = true, bool init_lengths = false); + /// @brief Propagate the lenghts of len_vars from arith_model into Z3, so that it forces correct values for the LIA part of input formula + void propagate_lengths_from_arith_model(); + /** * @brief Checks if the current instance is suitable for Nielsen decision procedure. * diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index 03cc8396b10..e70eebfc771 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -243,8 +243,9 @@ namespace smt::noodler { } lbool theory_str_noodler::check_len_sat(expr_ref len_formula, expr_ref* unsat_core) { - if (len_formula == m.mk_true()) { + if (len_formula == m.mk_true() && (len_vars.empty() || !m_params.m_produce_models)) { // we assume here that existing length constraints are satisfiable, so adding true will do nothing + // however, for model generation, we need to always produce models if we have some length vars return l_true; } @@ -422,7 +423,8 @@ namespace smt::noodler { } bool theory_str_noodler::is_mult_membership_suitable() { - if (!this->m_conversion_todo.empty() || !this->m_not_contains_todo_rel.empty()) { + // TODO handle length vars (also the ones without any constraints other than lenght ones, for those we just need to compute arith model) + if (!this->m_conversion_todo.empty() || !this->m_not_contains_todo_rel.empty() || !this->len_vars.empty()) { return false; } @@ -557,4 +559,14 @@ namespace smt::noodler { return l_true; } } + + void theory_str_noodler::propagate_lengths_from_arith_model() { + if (!m_params.m_produce_models) { return; } + SASSERT(arith_model != nullptr); + expr_ref model(m); + for (const auto& len_var : len_vars) { + arith_model->eval_expr(m_util_s.str.mk_length(len_var), model); + add_axiom(m.mk_eq(m_util_s.str.mk_length(len_var), model)); + } + } } diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc index d10b5aa54b8..03e3f840dd7 100644 --- a/src/smt/theory_str_noodler/util.cc +++ b/src/smt/theory_str_noodler/util.cc @@ -82,23 +82,6 @@ namespace smt::noodler::util { return m_util_s.is_string(expression->get_sort()) && is_variable(expression); } - std::set get_dummy_symbols(size_t new_symb_num, std::set& symbols_to_append_to) { - std::set dummy_symbols{}; - uint32_t dummy_symbol{ 0 }; - const size_t disequations_number{ new_symb_num }; - for (size_t diseq_index{ 0 }; diseq_index < disequations_number; ++diseq_index) { - while (symbols_to_append_to.find(dummy_symbol) != symbols_to_append_to.end()) { ++dummy_symbol; } - dummy_symbols.insert(dummy_symbol); - ++dummy_symbol; - } - [[maybe_unused]] const size_t dummy_symbols_number{ dummy_symbols.size() }; - assert(dummy_symbols_number == disequations_number); - [[maybe_unused]] const size_t symbols_in_formula_number{ symbols_to_append_to.size() }; - symbols_to_append_to.insert(dummy_symbols.begin(), dummy_symbols.end()); - assert(dummy_symbols_number + symbols_in_formula_number == symbols_to_append_to.size()); - return dummy_symbols; - } - void collect_terms(app* const ex, ast_manager& m, const seq_util& m_util_s, obj_map& pred_replace, std::map& var_name, std::vector& terms) { diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h index 140aecd567c..247775789aa 100644 --- a/src/smt/theory_str_noodler/util.h +++ b/src/smt/theory_str_noodler/util.h @@ -93,15 +93,6 @@ namespace smt::noodler::util { */ void get_variable_names(expr* ex, const seq_util& m_util_s, const ast_manager& m, std::unordered_set& res); - /** - * Get dummy symbols. - * - * @param[in] new_symb_num Number of added symbols. - * @param[out] symbols_to_append_to Set of symbols where dummy symbols are appended to. - * @return Set of dummy symbols. - */ - std::set get_dummy_symbols(size_t new_symb_num, std::set& symbols_to_append_to); - /** * Collect basic terms (vars, literals) from a concatenation @p ex. Append the basic terms to the output parameter * @p terms.