From ad8eb8fdcb9e0d9f19fb19d9ee7a14f3cbce0112 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Apr 2020 22:44:02 -0700
Subject: [PATCH] #4024
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/model/model_evaluator.cpp | 9 +----
src/smt/seq_eq_solver.cpp | 58 ++++++++++++++++++++++++++++++
src/smt/theory_seq.cpp | 67 +++++------------------------------
3 files changed, 67 insertions(+), 67 deletions(-)
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 328afad73..72a0e4ab2 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -178,14 +178,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = val;
return BR_DONE;
}
-#if 0
- func_decl* g = nullptr;
- VERIFY(m_ar.is_as_array(f, g));
- auto* fi = m_model.get_func_interp(g);
- result = fi->get_array_interp(g);
- if (result) return BR_REWRITE_FULL;
-#endif
- return BR_FAILED;
+ // fall through
}
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index af24adeac..f49d5f648 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1773,3 +1773,61 @@ bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const
return false;
}
+/**
+ nth(x,idx) = rhs =>
+ x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
+ NB: need 0 <= idx < len(rhs)
+*/
+bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
+ expr* s = nullptr, *idx = nullptr;
+ if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
+ rational r;
+ bool idx_is_zero = m_autil.is_numeral(idx, r) && r.is_zero();
+ expr_ref_vector ls1(m), rs1(m);
+ expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
+ m_rewrite(idx1);
+ expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
+ ls1.push_back(s);
+ if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));
+ rs1.push_back(m_util.str.mk_unit(rhs));
+ rs1.push_back(m_sk.mk_post(s, idx1));
+ TRACE("seq", tout << ls1 << "\n"; tout << rs1 << "\n";);
+ m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));
+ return true;
+ }
+ return false;
+}
+
+bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
+ if (solve_nth_eq2(ls, rs, dep)) {
+ return true;
+ }
+ if (ls.size() != 1 || rs.size() <= 1) {
+ return false;
+ }
+ expr* l = ls.get(0);
+ rational val;
+ if (!get_length(l, val) || val != rational(rs.size())) {
+ return false;
+ }
+ for (unsigned i = 0; i < rs.size(); ++i) {
+ unsigned k = 0;
+ expr* ru = nullptr, *r = nullptr;
+ if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth_i(ru, r, k) && k == i && r == l) {
+ continue;
+ }
+ return false;
+ }
+ add_solution(l, mk_concat(rs, m.get_sort(l)), dep);
+ return true;
+}
+
+bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
+ if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) {
+ return true;
+ }
+ if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
+ return true;
+ }
+ return false;
+}
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 207b2d643..93a01e95c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1002,65 +1002,6 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
return true;
}
-/**
- nth(x,idx) = rhs =>
- x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
- NB: need 0 <= idx < len(rhs)
-*/
-bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
- expr* s = nullptr, *idx = nullptr;
- if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
- rational r;
- bool idx_is_zero = m_autil.is_numeral(idx, r) && r.is_zero();
- expr_ref_vector ls1(m), rs1(m);
- expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
- m_rewrite(idx1);
- expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
- ls1.push_back(s);
- if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));
- rs1.push_back(m_util.str.mk_unit(rhs));
- rs1.push_back(m_sk.mk_post(s, idx1));
- TRACE("seq", tout << ls1 << "\n"; tout << rs1 << "\n";);
- m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));
- return true;
- }
- return false;
-}
-
-bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
- if (solve_nth_eq2(ls, rs, dep)) {
- return true;
- }
- if (ls.size() != 1 || rs.size() <= 1) {
- return false;
- }
- expr* l = ls.get(0);
- rational val;
- if (!get_length(l, val) || val != rational(rs.size())) {
- return false;
- }
- for (unsigned i = 0; i < rs.size(); ++i) {
- unsigned k = 0;
- expr* ru = nullptr, *r = nullptr;
- if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth_i(ru, r, k) && k == i && r == l) {
- continue;
- }
- return false;
- }
- add_solution(l, mk_concat(rs, m.get_sort(l)), dep);
- return true;
-}
-
-bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
- if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) {
- return true;
- }
- if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
- return true;
- }
-
- return false;
-}
bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
@@ -2847,6 +2788,14 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
if (!arg1 || !arg2) return true;
result = m_util.str.mk_index(arg1, arg2, e3);
}
+#if 0
+ else if (m_util.str.is_nth_i(e, e1, e2)) {
+ arg1 = try_expand(e1, deps);
+ if (!arg1) return true;
+ result = m_util.str.mk_nth_i(arg1, e2);
+ // m_rewrite(result);
+ }
+#endif
else if (m_util.str.is_last_index(e, e1, e2)) {
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);