mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

throttle digit constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-22 17:55:18 -07:00
parent c7878e384c
commit 8fe3caa101
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -982,7 +982,9 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
} }
expr* u = nullptr; expr* u = nullptr;
for (expr* r : rs) { for (expr* r : rs) {
if (m_util.str.is_unit(r, u)) { if (m_util.str.is_unit(r, u) && !m_is_digit.contains(u)) {
m_is_digit.insert(u);
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_is_digit, u));
literal is_digit = m_ax.is_digit(u); literal is_digit = m_ax.is_digit(u);
if (get_context().get_assignment(is_digit) != l_true) { if (get_context().get_assignment(is_digit) != l_true) {
propagate_lit(dep, 0, nullptr, is_digit); propagate_lit(dep, 0, nullptr, is_digit);

1
src/smt/theory_seq.h
View file

@ -425,6 +425,7 @@ namespace smt {
re2automaton m_mk_aut; re2automaton m_mk_aut;
obj_hashtable<expr> m_fixed; // string variables that are fixed length. obj_hashtable<expr> m_fixed; // string variables that are fixed length.
obj_hashtable<expr> m_is_digit; // expressions that have been constrained to be digits
void init(context* ctx) override; void init(context* ctx) override;
final_check_status final_check_eh() override; final_check_status final_check_eh() override;