mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #5121

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-28 16:14:37 -07:00
parent 6aa766a544
commit 0432311b11
2 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_seq.cpp
View file

@ -1454,9 +1454,12 @@ bool theory_seq::internalize_term(app* term) {
return true; return true;
} }
void theory_seq::add_length(expr* e, expr* l) { void theory_seq::add_length(expr* l) {
expr* e = nullptr;
VERIFY(m_util.str.is_length(l, e));
if (has_length(e))
return;
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";); TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
SASSERT(!m_has_length.contains(l));
m_length.push_back(l); m_length.push_back(l);
m_has_length.insert(e); m_has_length.insert(e);
m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e)); m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
@ -1504,7 +1507,7 @@ bool theory_seq::add_length_to_eqc(expr* e) {
if (!has_length(o)) { if (!has_length(o)) {
expr_ref len(m_util.str.mk_length(o), m); expr_ref len(m_util.str.mk_length(o), m);
ensure_enode(len); ensure_enode(len);
add_length(o, len); add_length(len);
change = true; change = true;
} }
n = n->get_next(); n = n->get_next();
@ -2471,6 +2474,7 @@ void theory_seq::enque_axiom(expr* e) {
void theory_seq::deque_axiom(expr* n) { void theory_seq::deque_axiom(expr* n) {
TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";); TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";);
if (m_util.str.is_length(n)) { if (m_util.str.is_length(n)) {
add_length(n);
m_ax.add_length_axiom(n); m_ax.add_length_axiom(n);
if (!ctx.at_base_level()) { if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(*this, alloc(replay_axiom, m, n))); m_trail_stack.push(push_replay(*this, alloc(replay_axiom, m, n)));

2
src/smt/theory_seq.h
View file

@ -555,7 +555,7 @@ namespace smt {
void add_axiom(literal_vector& lits); void add_axiom(literal_vector& lits);
bool has_length(expr *e) const { return m_has_length.contains(e); } bool has_length(expr *e) const { return m_has_length.contains(e); }
void add_length(expr* e, expr* l); void add_length(expr* l);
bool add_length_to_eqc(expr* n); bool add_length_to_eqc(expr* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len); bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
void enforce_length_coherence(enode* n1, enode* n2); void enforce_length_coherence(enode* n1, enode* n2);