From eded7d023d85b947d3e68e2c8f27d1ddb9b66447 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Apr 2020 16:00:03 -0700
Subject: [PATCH] fix #4006
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/muz/base/rule_properties.cpp | 20 ++--
src/muz/base/rule_properties.h | 2 +
src/smt/seq_eq_solver.cpp | 155 +++++++++++++++++++++++++++++++
src/smt/theory_seq.cpp | 150 +++---------------------------
4 files changed, 181 insertions(+), 146 deletions(-)
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 875612bd8..5896504cf 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -28,7 +28,7 @@ Notes:
using namespace datalog;
rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p):
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p),
- m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m),
+ m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), m_rec(m),
m_generate_proof(false), m_collected(false), m_is_monotone(true) {}
rule_properties::~rule_properties() {}
@@ -207,19 +207,20 @@ void rule_properties::operator()(quantifier* n) {
void rule_properties::operator()(app* n) {
func_decl_ref f_out(m);
expr* n1 = nullptr, *n2 = nullptr;
+ func_decl* f = n->get_decl();
rational r;
if (m_is_predicate(n)) {
insert(m_interp_pred, m_rule);
}
- else if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) {
- m_uninterp_funs.insert(n->get_decl(), m_rule);
+ else if (is_uninterp(n) && !m_dl.is_rule_sort(f->get_range())) {
+ m_uninterp_funs.insert(f, m_rule);
}
else if (m_dt.is_accessor(n)) {
sort* s = m.get_sort(n->get_arg(0));
SASSERT(m_dt.is_datatype(s));
if (m_dt.get_datatype_constructors(s)->size() > 1) {
bool found = false;
- func_decl * c = m_dt.get_accessor_constructor(n->get_decl());
+ func_decl * c = m_dt.get_accessor_constructor(f);
unsigned ut_size = m_rule->get_uninterpreted_tail_size();
unsigned t_size = m_rule->get_tail_size();
for (unsigned i = ut_size; !found && i < t_size; ++i) {
@@ -229,17 +230,20 @@ void rule_properties::operator()(app* n) {
}
}
if (!found) {
- m_uninterp_funs.insert(n->get_decl(), m_rule);
+ m_uninterp_funs.insert(f, m_rule);
}
}
}
- else if (m_a.is_considered_uninterpreted(n->get_decl(), n->get_num_args(), n->get_args(), f_out)) {
- m_uninterp_funs.insert(n->get_decl(), m_rule);
+ else if (m_a.is_considered_uninterpreted(f, n->get_num_args(), n->get_args(), f_out)) {
+ m_uninterp_funs.insert(f, m_rule);
}
else if ((m_a.is_mod(n, n1, n2) || m_a.is_div(n, n1, n2) ||
m_a.is_idiv(n, n1, n2) || m_a.is_rem(n, n1, n2))
&& (!evaluates_to_numeral(n2, r) || r.is_zero())) {
- m_uninterp_funs.insert(n->get_decl(), m_rule);
+ m_uninterp_funs.insert(f, m_rule);
+ }
+ else if (m_rec.is_defined(f)) {
+ m_uninterp_funs.insert(f, m_rule);
}
check_sort(m.get_sort(n));
}
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index 591d95c1a..42d1f349b 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -26,6 +26,7 @@ Notes:
#include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
#include "muz/base/dl_rule.h"
#include "ast/expr_functors.h"
@@ -40,6 +41,7 @@ namespace datalog {
arith_util m_a;
bv_util m_bv;
array_util m_ar;
+ recfun::util m_rec;
bool m_generate_proof;
rule* m_rule;
obj_map<quantifier, rule*> m_quantifiers;
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 86e1645ca..af24adeac 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1618,3 +1618,158 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
return true;
}
+/**
+ match X abc = defg Y, for abc, defg non-empty
+*/
+
+bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
+ if (ls.size() > 1 && is_var(ls[0]) &&
+ rs.size() > 1 && is_var(rs.back())) {
+ xs.reset();
+ ys.reset();
+ x = ls[0];
+ y = rs.back();
+ for (unsigned i = 1; i < ls.size(); ++i) {
+ if (!m_util.str.is_unit(ls[i])) return false;
+ }
+ for (unsigned i = 0; i < rs.size()-1; ++i) {
+ if (!m_util.str.is_unit(rs[i])) return false;
+ }
+ xs.append(ls.size()-1, ls.c_ptr() + 1);
+ ys.append(rs.size()-1, rs.c_ptr());
+ return true;
+ }
+ return false;
+}
+
+/*
+ match: Description TBD
+*/
+
+bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
+ expr_ref& x1, expr_ref_vector& xs, expr_ref& x2,
+ expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+ if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
+ rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+ unsigned l_start = 1;
+ for (; l_start < ls.size()-1; ++l_start) {
+ if (m_util.str.is_unit(ls[l_start])) break;
+ }
+ if (l_start == ls.size()-1) return false;
+ unsigned l_end = l_start;
+ for (; l_end < ls.size()-1; ++l_end) {
+ if (!m_util.str.is_unit(ls[l_end])) break;
+ }
+ --l_end;
+ unsigned r_start = 1;
+ for (; r_start < rs.size()-1; ++r_start) {
+ if (m_util.str.is_unit(rs[r_start])) break;
+ }
+ if (r_start == rs.size()-1) return false;
+ unsigned r_end = r_start;
+ for (; r_end < rs.size()-1; ++r_end) {
+ if (!m_util.str.is_unit(rs[r_end])) break;
+ }
+ --r_end;
+ for (unsigned i = l_start; i < l_end+1; ++i) {
+ if (!m_util.str.is_unit(ls[i])) return false;
+ }
+ for (unsigned i = r_start; i < r_end+1; ++i) {
+ if (!m_util.str.is_unit(rs[i])) return false;
+ }
+ xs.reset();
+ xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
+ x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
+ x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
+ ys.reset();
+ ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+ y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+ y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+ return true;
+ }
+ return false;
+}
+
+/*
+ match: Description TBD
+*/
+
+bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
+ expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
+ if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
+ rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+ unsigned l_start = ls.size()-1;
+ for (; l_start > 0; --l_start) {
+ if (!m_util.str.is_unit(ls[l_start])) break;
+ }
+ if (l_start == ls.size()-1) return false;
+ ++l_start;
+ unsigned r_end = rs.size()-2;
+ for (; r_end > 0; --r_end) {
+ if (m_util.str.is_unit(rs[r_end])) break;
+ }
+ if (r_end == 0) return false;
+ unsigned r_start = r_end;
+ for (; r_start > 0; --r_start) {
+ if (!m_util.str.is_unit(rs[r_start])) break;
+ }
+ ++r_start;
+ for (unsigned i = l_start; i < ls.size(); ++i) {
+ if (!m_util.str.is_unit(ls[i])) return false;
+ }
+ for (unsigned i = r_start; i < r_end+1; ++i) {
+ if (!m_util.str.is_unit(rs[i])) return false;
+ }
+ xs.reset();
+ xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
+ x = m_util.str.mk_concat(l_start, ls.c_ptr());
+ ys.reset();
+ ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+ y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+ y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+ return true;
+ }
+ return false;
+}
+
+/*
+ match: Description TBD
+*/
+
+bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs,
+ expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
+ if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
+ rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+ unsigned l_start = 0;
+ for (; l_start < ls.size()-1; ++l_start) {
+ if (!m_util.str.is_unit(ls[l_start])) break;
+ }
+ if (l_start == 0) return false;
+ unsigned r_start = 1;
+ for (; r_start < rs.size()-1; ++r_start) {
+ if (m_util.str.is_unit(rs[r_start])) break;
+ }
+ if (r_start == rs.size()-1) return false;
+ unsigned r_end = r_start;
+ for (; r_end < rs.size()-1; ++r_end) {
+ if (!m_util.str.is_unit(rs[r_end])) break;
+ }
+ --r_end;
+ for (unsigned i = 0; i < l_start; ++i) {
+ if (!m_util.str.is_unit(ls[i])) return false;
+ }
+ for (unsigned i = r_start; i < r_end+1; ++i) {
+ if (!m_util.str.is_unit(rs[i])) return false;
+ }
+ xs.reset();
+ xs.append(l_start, ls.c_ptr());
+ x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
+ ys.reset();
+ ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+ y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+ y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+ return true;
+ }
+ return false;
+}
+
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 19f0dfdcd..5d02d005c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1168,143 +1168,6 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
return false;
}
-bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
- if (ls.size() > 1 && is_var(ls[0]) &&
- rs.size() > 1 && is_var(rs.back())) {
- xs.reset();
- ys.reset();
- x = ls[0];
- y = rs.back();
- for (unsigned i = 1; i < ls.size(); ++i) {
- if (!m_util.str.is_unit(ls[i])) return false;
- }
- for (unsigned i = 0; i < rs.size()-1; ++i) {
- if (!m_util.str.is_unit(rs[i])) return false;
- }
- xs.append(ls.size()-1, ls.c_ptr() + 1);
- ys.append(rs.size()-1, rs.c_ptr());
- return true;
- }
- return false;
-}
-
-bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
- expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
- if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
- rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
- unsigned l_start = 1;
- for (; l_start < ls.size()-1; ++l_start) {
- if (m_util.str.is_unit(ls[l_start])) break;
- }
- if (l_start == ls.size()-1) return false;
- unsigned l_end = l_start;
- for (; l_end < ls.size()-1; ++l_end) {
- if (!m_util.str.is_unit(ls[l_end])) break;
- }
- --l_end;
- unsigned r_start = 1;
- for (; r_start < rs.size()-1; ++r_start) {
- if (m_util.str.is_unit(rs[r_start])) break;
- }
- if (r_start == rs.size()-1) return false;
- unsigned r_end = r_start;
- for (; r_end < rs.size()-1; ++r_end) {
- if (!m_util.str.is_unit(rs[r_end])) break;
- }
- --r_end;
- for (unsigned i = l_start; i < l_end+1; ++i) {
- if (!m_util.str.is_unit(ls[i])) return false;
- }
- for (unsigned i = r_start; i < r_end+1; ++i) {
- if (!m_util.str.is_unit(rs[i])) return false;
- }
- xs.reset();
- xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
- x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
- x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
- ys.reset();
- ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
- y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
- y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
- return true;
- }
- return false;
-}
-
-bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs,
- expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
- if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
- rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
- unsigned l_start = ls.size()-1;
- for (; l_start > 0; --l_start) {
- if (!m_util.str.is_unit(ls[l_start])) break;
- }
- if (l_start == ls.size()-1) return false;
- ++l_start;
- unsigned r_end = rs.size()-2;
- for (; r_end > 0; --r_end) {
- if (m_util.str.is_unit(rs[r_end])) break;
- }
- if (r_end == 0) return false;
- unsigned r_start = r_end;
- for (; r_start > 0; --r_start) {
- if (!m_util.str.is_unit(rs[r_start])) break;
- }
- ++r_start;
- for (unsigned i = l_start; i < ls.size(); ++i) {
- if (!m_util.str.is_unit(ls[i])) return false;
- }
- for (unsigned i = r_start; i < r_end+1; ++i) {
- if (!m_util.str.is_unit(rs[i])) return false;
- }
- xs.reset();
- xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
- x = m_util.str.mk_concat(l_start, ls.c_ptr());
- ys.reset();
- ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
- y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
- y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
- return true;
- }
- return false;
-}
-
-bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs,
- expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
- if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
- rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
- unsigned l_start = 0;
- for (; l_start < ls.size()-1; ++l_start) {
- if (!m_util.str.is_unit(ls[l_start])) break;
- }
- if (l_start == 0) return false;
- unsigned r_start = 1;
- for (; r_start < rs.size()-1; ++r_start) {
- if (m_util.str.is_unit(rs[r_start])) break;
- }
- if (r_start == rs.size()-1) return false;
- unsigned r_end = r_start;
- for (; r_end < rs.size()-1; ++r_end) {
- if (!m_util.str.is_unit(rs[r_end])) break;
- }
- --r_end;
- for (unsigned i = 0; i < l_start; ++i) {
- if (!m_util.str.is_unit(ls[i])) return false;
- }
- for (unsigned i = r_start; i < r_end+1; ++i) {
- if (!m_util.str.is_unit(rs[i])) return false;
- }
- xs.reset();
- xs.append(l_start, ls.c_ptr());
- x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
- ys.reset();
- ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
- y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
- y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
- return true;
- }
- return false;
-}
bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
if (ls.empty() || rs.empty()) {
@@ -2521,7 +2384,18 @@ app* theory_seq::get_ite_value(expr* e) {
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
app* e = n->get_owner();
context& ctx = get_context();
- TRACE("seq", tout << mk_pp(n->get_owner(), m) << "\n";);
+ TRACE("seq", tout << mk_pp(e, m) << "\n";);
+
+ // Shortcut for well-founded values to avoid some quadratic overhead
+ expr* x = nullptr, *y = nullptr, *z = nullptr;
+ if (m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) &&
+ ctx.e_internalized(z) && ctx.e_internalized(y)) {
+ sort* srt = m.get_sort(e);
+ seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt);
+ sv->add_unit(ctx.get_enode(z));
+ sv->add_string(y);
+ return sv;
+ }
e = get_ite_value(e);
if (m_util.is_seq(e)) {
unsigned start = m_concat.size();