From 8fe3caa1010f9fb3c7e35612f0c18264a047da60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Apr 2020 17:55:18 -0700
Subject: [PATCH] throttle digit constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_seq.cpp | 4 +++-
src/smt/theory_seq.h | 1 +
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8c501d531..00145970a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -982,7 +982,9 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
}
expr* u = nullptr;
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);
if (get_context().get_assignment(is_digit) != l_true) {
propagate_lit(dep, 0, nullptr, is_digit);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f09d6b89a..47f64564e 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -425,6 +425,7 @@ namespace smt {
re2automaton m_mk_aut;
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;
final_check_status final_check_eh() override;