From 78550ec816129e9b8184618f09b6750b7107cf29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 31 Dec 2015 07:48:14 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 8 +- src/ast/seq_decl_plugin.cpp | 2 +- src/smt/theory_seq.cpp | 177 +++++++++++++++++++----------- src/smt/theory_seq.h | 64 ++++++----- 4 files changed, 152 insertions(+), 99 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 77baa36fc..00b4371d9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -475,6 +475,10 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { for (; i < as.size() && i < bs.size(); ++i) { all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get()); if (as[i].get() != bs[i].get()) { + if (all_values) { + result = m().mk_false(); + return BR_DONE; + } break; } }; @@ -483,10 +487,6 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { return BR_DONE; } SASSERT(i < as.size()); - if (all_values && (i < bs.size() || m_util.str.is_unit(as[i+1].get()))) { - result = m().mk_false(); - return BR_DONE; - } if (i == bs.size()) { expr_ref_vector es(m()); for (unsigned j = i; j < as.size(); ++j) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 57ccd1a3e..70ee4298b 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -611,7 +611,7 @@ app* seq_decl_plugin::mk_string(zstring const& s) { bool seq_decl_plugin::is_value(app* e) const { return - is_app_of(e, m_family_id, OP_STRING_CONST) || + is_app_of(e, m_family_id, OP_SEQ_EMPTY) || (is_app_of(e, m_family_id, OP_SEQ_UNIT) && m_manager->is_value(e->get_arg(0))); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b9886a609..4f9273322 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -39,12 +39,12 @@ struct display_expr { -void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) { +void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) { if (e == r) { return; } m_cache.reset(); - std::pair value; + std::pair value; if (m_map.find(e, value)) { add_trail(DEL, e, value.first, value.second); } @@ -54,7 +54,7 @@ void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d add_trail(INS, e, r, d); } -void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d) { +void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, dependency* d) { m_updates.push_back(op); m_lhs.push_back(l); m_rhs.push_back(r); @@ -65,8 +65,8 @@ bool theory_seq::solution_map::is_root(expr* e) const { return !m_map.contains(e); } -expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { - std::pair value; +expr* theory_seq::solution_map::find(expr* e, dependency*& d) { + std::pair value; d = 0; expr* result = e; while (m_map.find(result, value)) { @@ -80,7 +80,7 @@ expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { } expr* theory_seq::solution_map::find(expr* e) { - std::pair value; + std::pair value; while (m_map.find(e, value)) { e = value.first; } @@ -258,11 +258,15 @@ bool theory_seq::find_branch_candidate(expr* l, expr_ref_vector const& rs) { return false; } + + bool all_units = true; + expr_ref_vector cases(m); expr_ref v0(m), v(m); v0 = m_util.str.mk_empty(m.get_sort(l)); if (l_false != assume_equality(l, v0)) { return true; } + cases.push_back(v0); for (unsigned j = 0; j < rs.size(); ++j) { if (occurs(l, rs[j])) { return false; @@ -276,12 +280,23 @@ bool theory_seq::find_branch_candidate(expr* l, expr_ref_vector const& rs) { return true; } } + all_units = false; } + all_units &= m_util.str.is_unit(rs[j]); v0 = (j == 0)? rs[0] : m_util.str.mk_concat(v0, rs[j]); + cases.push_back(v0); if (l_false != assume_equality(l, v0)) { return true; } } + if (all_units) { + literal_vector lits; + for (unsigned i = 0; i < cases.size(); ++i) { + lits.push_back(mk_eq(l, cases[i].get(), false)); + } + get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + return true; + } return false; } @@ -328,7 +343,6 @@ bool theory_seq::propagate_length_coherence(expr* e) { tout << " lo: " << lo << " hi: " << hi << "\n"; ); - literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true)))); expr_ref seq(e, m); expr_ref_vector elems(m); unsigned _lo = lo.get_unsigned(); @@ -337,25 +351,24 @@ bool theory_seq::propagate_length_coherence(expr* e) { elems.push_back(head); seq = tail; } + expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); elems.push_back(seq); tail = m_util.str.mk_concat(elems.size(), elems.c_ptr()); // len(e) >= low => e = tail - add_axiom(~low, mk_eq(e, tail, false)); - assume_equality(tail, e); + literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true)))); + add_axiom(~low, mk_eq(e, tail, false)); + assume_equality(seq, emp); if (upper_bound(e, hi)) { expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m); expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m); add_axiom(~mk_literal(high1), mk_literal(high2)); } - //m_replay_length_coherence.push_back(e); - //m_replay_length_coherence_qhead = m_replay_length_coherence.size(); return true; } bool theory_seq::check_length_coherence() { - if (m_length.empty()) return true; context& ctx = get_context(); bool coherent = true; obj_hashtable::iterator it = m_length.begin(), end = m_length.end(); @@ -366,10 +379,10 @@ bool theory_seq::check_length_coherence() { expr_ref head(m), tail(m); if (!propagate_length_coherence(e) && l_false == assume_equality(e, emp)) { - mk_decompose(e, head, tail); // e = emp \/ e = unit(head.elem(e))*tail(e) + mk_decompose(e, head, tail); expr_ref conc(m_util.str.mk_concat(head, tail), m); - add_axiom(mk_eq_empty(e), mk_eq(e, conc, false)); + propagate_is_conc(e, conc); assume_equality(tail, emp); } return false; @@ -378,6 +391,24 @@ bool theory_seq::check_length_coherence() { return coherent; } +/* + lit => s != "" +*/ +void theory_seq::propagate_non_empty(literal lit, expr* s) { + SASSERT(get_context().get_assignment(lit) == l_true); + propagate_lit(0, 1, &lit, ~mk_eq_empty(s)); +} + +void theory_seq::propagate_is_conc(expr* e, expr* conc) { + TRACE("seq", tout << mk_pp(conc, m) << " is non-empty\n";); + context& ctx = get_context(); + literal lit = ~mk_eq_empty(e); + SASSERT(ctx.get_assignment(lit) == l_true); + propagate_lit(0, 1, &lit, mk_eq(e, conc, false)); + expr_ref e1(e, m), e2(conc, m); + m_eqs.push_back(eq(e1, e2, m_dm.mk_leaf(assumption(lit)))); +} + expr_ref theory_seq::mk_nth(expr* s, expr* idx) { sort* char_sort = 0; VERIFY(m_util.is_seq(m.get_sort(s), char_sort)); @@ -435,36 +466,55 @@ bool theory_seq::is_solved() { return true; } -void theory_seq::propagate_lit(enode_pair_dependency* dep, unsigned n, literal const* lits, literal lit) { +void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const { + svector assumptions; + const_cast(m_dm).linearize(dep, assumptions); + for (unsigned i = 0; i < assumptions.size(); ++i) { + assumption const& a = assumptions[i]; + if (a.lit != null_literal) { + lits.push_back(a.lit); + } + if (a.n1 != 0) { + eqs.push_back(enode_pair(a.n1, a.n2)); + } + } +} + + + +void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits, literal lit) { context& ctx = get_context(); ctx.mark_as_relevant(lit); - vector _eqs; - m_dm.linearize(dep, _eqs); + literal_vector lits(n, _lits); + enode_pair_vector eqs; + linearize(dep, eqs, lits); TRACE("seq", ctx.display_detailed_literal(tout, lit); - tout << " <- "; ctx.display_literals_verbose(tout, n, lits); display_deps(tout, dep);); + tout << " <- "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); display_deps(tout, dep);); justification* js = ctx.mk_justification( ext_theory_propagation_justification( - get_id(), ctx.get_region(), n, lits, _eqs.size(), _eqs.c_ptr(), lit)); + get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit)); ctx.assign(lit, js); } -void theory_seq::set_conflict(enode_pair_dependency* dep, literal_vector const& lits) { +void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) { context& ctx = get_context(); - vector _eqs; - m_dm.linearize(dep, _eqs); + enode_pair_vector eqs; + literal_vector lits(_lits); + linearize(dep, eqs, lits); TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); display_deps(tout, dep); ;); ctx.set_conflict( ctx.mk_justification( ext_theory_conflict_justification( - get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), _eqs.size(), _eqs.c_ptr(), 0, 0))); + get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, 0))); } -void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) { +void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { context& ctx = get_context(); - vector _eqs; - m_dm.linearize(dep, _eqs); + literal_vector lits; + enode_pair_vector eqs; + linearize(dep, eqs, lits); TRACE("seq", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- "; display_deps(tout, dep); @@ -472,13 +522,13 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)); + get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); ctx.assign_eq(n1, n2, eq_justification(js)); } -bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps, bool& propagated) { +bool theory_seq::simplify_eq(expr* l, expr* r, dependency* deps, bool& propagated) { context& ctx = get_context(); seq_rewriter rw(m); expr_ref_vector lhs(m), rhs(m); @@ -518,7 +568,7 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps, bool return true; } -bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps, bool& propagated) { +bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps, bool& propagated) { expr_ref lh = canonize(l, deps); expr_ref rh = canonize(r, deps); if (lh == rh) { @@ -571,7 +621,7 @@ bool theory_seq::is_nth(expr* e) const { return is_skolem(m_nth, e); } -bool theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { +bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) { if (l == r) { return false; } @@ -645,7 +695,7 @@ bool theory_seq::solve_ne(unsigned idx) { } for (unsigned i = 0; i < n.m_lhs.size(); ++i) { expr_ref_vector lhs(m), rhs(m); - enode_pair_dependency* deps = 0; + dependency* deps = 0; expr* l = n.m_lhs[i]; expr* r = n.m_rhs[i]; expr_ref lh = canonize(l, deps); @@ -744,16 +794,15 @@ bool theory_seq::internalize_term(app* term) { ctx.set_var_theory(bv, get_id()); ctx.mark_as_relevant(bv); } - else { - enode* e = 0; - if (ctx.e_internalized(term)) { - e = ctx.get_enode(term); - } - else { - e = ctx.mk_enode(term, false, m.is_bool(term), true); - } - mk_var(e); + enode* e = 0; + if (ctx.e_internalized(term)) { + e = ctx.get_enode(term); } + else { + e = ctx.mk_enode(term, false, m.is_bool(term), true); + } + mk_var(e); + return true; } @@ -846,13 +895,15 @@ void theory_seq::display_disequation(std::ostream& out, ne const& e) const { display_deps(out, e.m_dep); } -void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const { - vector _eqs; - const_cast(m_dm).linearize(dep, _eqs); - for (unsigned i = 0; i < _eqs.size(); ++i) { - out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m); +void theory_seq::display_deps(std::ostream& out, dependency* dep) const { + literal_vector lits; + enode_pair_vector eqs; + linearize(dep, eqs, lits); + for (unsigned i = 0; i < eqs.size(); ++i) { + out << " " << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m); } out << "\n"; + get_context().display_literals_verbose(tout, lits.size(), lits.c_ptr()); } void theory_seq::collect_statistics(::statistics & st) const { @@ -953,7 +1004,7 @@ app* theory_seq::mk_value(app* e) { expr* e1; expr_ref result(e, m); if (m_util.str.is_unit(e, e1)) { - enode_pair_dependency* deps = 0; + dependency* deps = 0; result = expand(e1, deps); bv_util bv(m); rational val; @@ -1027,15 +1078,15 @@ bool theory_seq::can_propagate() { return m_axioms_head < m_axioms.size(); } -expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) { +expr_ref theory_seq::canonize(expr* e, dependency*& eqs) { expr_ref result = expand(e, eqs); m_rewrite(result); return result; } -expr_ref theory_seq::expand(expr* e0, enode_pair_dependency*& eqs) { +expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { expr_ref result(m); - enode_pair_dependency* deps = 0; + dependency* deps = 0; expr_dep ed; if (m_rep.find_cache(e0, ed)) { eqs = m_dm.mk_join(eqs, ed.second); @@ -1073,9 +1124,9 @@ expr_ref theory_seq::expand(expr* e0, enode_pair_dependency*& eqs) { return result; } -void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) { +void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) { if (a != b) { - dep = m_dm.mk_join(dep, m_dm.mk_leaf(std::make_pair(a, b))); + dep = m_dm.mk_join(dep, m_dm.mk_leaf(assumption(a, b))); } } @@ -1517,12 +1568,6 @@ void theory_seq::propagate_step(bool_var v, expr* step) { propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx))); } -/* - lit => len(s) > 0 -*/ -void theory_seq::propagate_non_empty(literal lit, expr* s) { - propagate_lit(0, 1, &lit, ~mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(0)))); -} literal theory_seq::mk_literal(expr* _e) { expr_ref e(_e, m); @@ -1585,9 +1630,7 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2, bool add_to_eqs) { if (add_to_eqs) { SASSERT(l_true == ctx.get_assignment(v)); expr_ref l(e1, m), r(e2, m); - enode* m1 = ensure_enode(ctx.bool_var2expr(v)); - enode* m2 = ctx.get_enode(m.mk_true()); - enode_pair_dependency* deps = m_dm.mk_leaf(enode_pair(m1, m2)); + dependency* deps = m_dm.mk_leaf(assumption(literal(v))); m_eqs.push_back(eq(l, r, deps)); } literal lit(v); @@ -1616,7 +1659,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { propagate_eq(v, f, e2, true); } else { - // !prefix(e1,e2) => len(e1) > 0; + // !prefix(e1,e2) => e1 != "" propagate_non_empty(literal(v, true), e1); add_atom(e); } @@ -1639,9 +1682,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { f = m_util.str.mk_concat(f1, e2, f2); propagate_eq(v, f, e1, true); } - else { + else if (!canonizes(false, e)) { literal lit(v, true); - propagate_non_empty(lit, e2); + propagate_non_empty(literal(v, true), e2); propagate_lit(0, 1, &lit, ~mk_literal(m_util.str.mk_prefix(e2, e1))); add_atom(e); } @@ -1680,11 +1723,11 @@ void theory_seq::add_atom(expr* e) { void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); - if (n1 != n2) { + if (n1 != n2 && m_util.is_seq(n1->get_owner())) { expr_ref o1(n1->get_owner(), m); expr_ref o2(n2->get_owner(), m); TRACE("seq", tout << o1 << " = " << o2 << "\n";); - enode_pair_dependency* deps = m_dm.mk_leaf(enode_pair(n1, n2)); + dependency* deps = m_dm.mk_leaf(assumption(n1, n2)); bool propagated = false; if (!simplify_eq(o1, o2, deps, propagated)) { m_eqs.push_back(eq(o1, o2, deps)); @@ -1709,6 +1752,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { if (!m.is_false(eq)) { m_nqs.push_back(ne(e1, e2)); } + // add solution for variable that is non-empty? } void theory_seq::push_scope_eh() { @@ -2019,8 +2063,9 @@ bool theory_seq::add_suffix2suffix(expr* e) { bool theory_seq::canonizes(bool sign, expr* e) { context& ctx = get_context(); - enode_pair_dependency* deps = 0; + dependency* deps = 0; expr_ref cont = canonize(e, deps); + TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";); if ((m.is_true(cont) && !sign) || (m.is_false(cont) && sign)) { propagate_lit(deps, 0, 0, ctx.get_literal(e)); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 798dd1341..2de6a36d0 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -32,11 +32,17 @@ Revision History: namespace smt { class theory_seq : public theory { - typedef scoped_dependency_manager enode_pair_dependency_manager; - typedef enode_pair_dependency_manager::dependency enode_pair_dependency; - + struct assumption { + enode* n1, *n2; + literal lit; + assumption(enode* n1, enode* n2): n1(n1), n2(n2), lit(null_literal) {} + assumption(literal lit): n1(0), n2(0), lit(lit) {} + }; + typedef scoped_dependency_manager dependency_manager; + typedef dependency_manager::dependency dependency; + typedef trail_stack th_trail_stack; - typedef std::pair expr_dep; + typedef std::pair expr_dep; typedef obj_map eqdep_map_t; // cache to track evaluations under equalities @@ -55,26 +61,26 @@ namespace smt { class solution_map { enum map_update { INS, DEL }; ast_manager& m; - enode_pair_dependency_manager& m_dm; + dependency_manager& m_dm; eqdep_map_t m_map; eval_cache m_cache; expr_ref_vector m_lhs, m_rhs; - ptr_vector m_deps; + ptr_vector m_deps; svector m_updates; unsigned_vector m_limit; - void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d); + void add_trail(map_update op, expr* l, expr* r, dependency* d); public: - solution_map(ast_manager& m, enode_pair_dependency_manager& dm): + solution_map(ast_manager& m, dependency_manager& dm): m(m), m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {} bool empty() const { return m_map.empty(); } - void update(expr* e, expr* r, enode_pair_dependency* d); + void update(expr* e, expr* r, dependency* d); void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); } bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); } - expr* find(expr* e, enode_pair_dependency*& d); + expr* find(expr* e, dependency*& d); expr* find(expr* e); bool is_root(expr* e) const; - void cache(expr* e, expr* r, enode_pair_dependency* d); + void cache(expr* e, expr* r, dependency* d); void reset_cache() { m_cache.reset(); } void push_scope() { m_limit.push_back(m_updates.size()); } void pop_scope(unsigned num_scopes); @@ -103,8 +109,8 @@ namespace smt { struct eq { expr_ref m_lhs; expr_ref m_rhs; - enode_pair_dependency* m_dep; - eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d): + dependency* m_dep; + eq(expr_ref& l, expr_ref& r, dependency* d): m_lhs(l), m_rhs(r), m_dep(d) {} eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {} eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; } @@ -118,7 +124,7 @@ namespace smt { expr_ref_vector m_lhs; expr_ref_vector m_rhs; literal_vector m_lits; - enode_pair_dependency* m_dep; + dependency* m_dep; ne(expr_ref& l, expr_ref& r): m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) { m_lhs.push_back(l); @@ -229,10 +235,10 @@ namespace smt { }; class push_dep : public trail { - enode_pair_dependency* m_dep; + dependency* m_dep; unsigned m_idx; public: - push_dep(theory_seq& th, unsigned idx, enode_pair_dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) { + push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) { th.m_nqs.ref(idx).m_dep = d; } virtual void undo(theory_seq& th) { @@ -254,7 +260,7 @@ namespace smt { unsigned m_solve_eqs; }; ast_manager& m; - enode_pair_dependency_manager m_dm; + dependency_manager m_dm; solution_map m_rep; // unification representative. scoped_vector m_eqs; // set of current equations. scoped_vector m_nqs; // set of current disequalities. @@ -317,19 +323,20 @@ namespace smt { bool pre_process_eqs(bool simplify_or_solve, bool& propagated); bool simplify_eqs(bool& propagated) { return pre_process_eqs(true, propagated); } bool solve_basic_eqs(bool& propagated) { return pre_process_eqs(false, propagated); } - bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep, bool& propagated); - bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep, bool& propagated); + bool simplify_eq(expr* l, expr* r, dependency* dep, bool& propagated); + bool solve_unit_eq(expr* l, expr* r, dependency* dep, bool& propagated); bool solve_nqs(); bool solve_ne(unsigned i); bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; } // asserting consequences - void propagate_lit(enode_pair_dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); } - void propagate_lit(enode_pair_dependency* dep, unsigned n, literal const* lits, literal lit); - void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2); + void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; + void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); } + void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); + void propagate_eq(dependency* dep, enode* n1, enode* n2); void propagate_eq(bool_var v, expr* e1, expr* e2, bool add_to_eqs = false); - void set_conflict(enode_pair_dependency* dep, literal_vector const& lits = literal_vector()); + void set_conflict(dependency* dep, literal_vector const& lits = literal_vector()); bool find_branch_candidate(expr* l, expr_ref_vector const& rs); lbool assume_equality(expr* l, expr* r); @@ -337,12 +344,12 @@ namespace smt { // variable solving utilities bool occurs(expr* a, expr* b); bool is_var(expr* b); - bool add_solution(expr* l, expr* r, enode_pair_dependency* dep); + bool add_solution(expr* l, expr* r, dependency* dep); bool is_nth(expr* a) const; expr_ref mk_nth(expr* s, expr* idx); - expr_ref canonize(expr* e, enode_pair_dependency*& eqs); - expr_ref expand(expr* e, enode_pair_dependency*& eqs); - void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); + expr_ref canonize(expr* e, dependency*& eqs); + expr_ref expand(expr* e, dependency*& eqs); + void add_dependency(dependency*& dep, enode* a, enode* b); void get_concat(expr* e, ptr_vector& concats); @@ -408,6 +415,7 @@ namespace smt { bool add_contains2contains(expr* e); bool canonizes(bool sign, expr* e); void propagate_non_empty(literal lit, expr* s); + void propagate_is_conc(expr* e, expr* conc); void propagate_acc_rej_length(bool_var v, expr* acc_rej); bool propagate_automata(); void add_atom(expr* e); @@ -416,7 +424,7 @@ namespace smt { void display_equations(std::ostream& out) const; void display_disequations(std::ostream& out) const; void display_disequation(std::ostream& out, ne const& e) const; - void display_deps(std::ostream& out, enode_pair_dependency* deps) const; + void display_deps(std::ostream& out, dependency* deps) const; public: theory_seq(ast_manager& m); virtual ~theory_seq();