mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
99da56a786
commit
284fcc2c04
|
@ -156,17 +156,17 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
|
|||
unsigned len = 0;
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < m_es.size(); ++i) {
|
||||
if (m_util.str.is_string(m_es[i], b)) {
|
||||
if (m_util.str.is_string(m_es[i].get(), b)) {
|
||||
len += b.length();
|
||||
}
|
||||
else if (m_util.str.is_unit(m_es[i])) {
|
||||
else if (m_util.str.is_unit(m_es[i].get())) {
|
||||
len += 1;
|
||||
}
|
||||
else if (m_util.str.is_empty(m_es[i])) {
|
||||
else if (m_util.str.is_empty(m_es[i].get())) {
|
||||
// skip
|
||||
}
|
||||
else {
|
||||
m_es[j] = m_es[i];
|
||||
m_es[j] = m_es[i].get();
|
||||
++j;
|
||||
}
|
||||
}
|
||||
|
@ -177,7 +177,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
|
|||
if (j != m_es.size() || j != 1) {
|
||||
expr_ref_vector es(m());
|
||||
for (unsigned i = 0; i < j; ++i) {
|
||||
es.push_back(m_util.str.mk_length(m_es[i]));
|
||||
es.push_back(m_util.str.mk_length(m_es[i].get()));
|
||||
}
|
||||
if (len != 0) {
|
||||
es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
|
||||
|
@ -207,14 +207,14 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
// check if subsequence of b is in a.
|
||||
ptr_vector<expr> as, bs;
|
||||
expr_ref_vector as(m()), bs(m());
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
bool found = false;
|
||||
for (unsigned i = 0; !found && i < as.size(); ++i) {
|
||||
if (bs.size() > as.size() - i) break;
|
||||
unsigned j = 0;
|
||||
for (; j < bs.size() && as[j+i] == bs[j]; ++j) {};
|
||||
for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
|
||||
found = j == bs.size();
|
||||
}
|
||||
if (found) {
|
||||
|
@ -292,7 +292,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
expr* b1 = m_util.str.get_leftmost_concat(b);
|
||||
isc1 = m_util.str.is_string(a1, s1);
|
||||
isc2 = m_util.str.is_string(b1, s2);
|
||||
ptr_vector<expr> as, bs;
|
||||
expr_ref_vector as(m()), bs(m());
|
||||
|
||||
if (a1 != b1 && isc1 && isc2) {
|
||||
if (s1.length() <= s2.length()) {
|
||||
|
@ -342,7 +342,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
unsigned i = 0;
|
||||
for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {};
|
||||
for (; i < as.size() && i < bs.size() && as[i].get() == bs[i].get(); ++i) {};
|
||||
if (i == as.size()) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
|
@ -350,7 +350,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
if (i == bs.size()) {
|
||||
expr_ref_vector es(m());
|
||||
for (unsigned j = i; j < as.size(); ++j) {
|
||||
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j]));
|
||||
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
|
||||
}
|
||||
result = mk_and(es);
|
||||
return BR_REWRITE3;
|
||||
|
@ -522,7 +522,6 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
expr* a, *b;
|
||||
zstring s;
|
||||
bool change = false;
|
||||
expr_ref_vector trail(m());
|
||||
m_lhs.reset();
|
||||
m_rhs.reset();
|
||||
m_util.str.get_concat(l, m_lhs);
|
||||
|
@ -545,7 +544,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
expr* r = m_rhs.back();
|
||||
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
|
||||
std::swap(l, r);
|
||||
std::swap(m_lhs, m_rhs);
|
||||
m_lhs.swap(m_rhs);
|
||||
}
|
||||
if (l == r) {
|
||||
m_lhs.pop_back();
|
||||
|
@ -575,7 +574,6 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
else {
|
||||
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
|
||||
m_rhs[m_rhs.size()-1] = s2;
|
||||
trail.push_back(s2);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -587,10 +585,10 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
// solve from front
|
||||
unsigned head1 = 0, head2 = 0;
|
||||
while (true) {
|
||||
while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
|
||||
while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1].get())) {
|
||||
++head1;
|
||||
}
|
||||
while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
|
||||
while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2].get())) {
|
||||
++head2;
|
||||
}
|
||||
if (head1 == m_lhs.size() || head2 == m_rhs.size()) {
|
||||
|
@ -598,11 +596,11 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
}
|
||||
SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
|
||||
|
||||
expr* l = m_lhs[head1];
|
||||
expr* r = m_rhs[head2];
|
||||
expr* l = m_lhs[head1].get();
|
||||
expr* r = m_rhs[head2].get();
|
||||
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
|
||||
std::swap(l, r);
|
||||
std::swap(m_lhs, m_rhs);
|
||||
m_lhs.swap(m_rhs);
|
||||
}
|
||||
if (l == r) {
|
||||
++head1;
|
||||
|
@ -631,7 +629,6 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
else {
|
||||
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
|
||||
m_rhs[m_rhs.size()-1] = s2;
|
||||
trail.push_back(s2);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -643,8 +640,8 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
zstring s1, s2;
|
||||
while (head1 < m_lhs.size() &&
|
||||
head2 < m_rhs.size() &&
|
||||
m_util.str.is_string(m_lhs[head1], s1) &&
|
||||
m_util.str.is_string(m_rhs[head2], s2)) {
|
||||
m_util.str.is_string(m_lhs[head1].get(), s1) &&
|
||||
m_util.str.is_string(m_rhs[head2].get(), s2)) {
|
||||
unsigned l = std::min(s1.length(), s2.length());
|
||||
for (unsigned i = 0; i < l; ++i) {
|
||||
if (s1[i] != s2[i]) {
|
||||
|
@ -656,14 +653,12 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
}
|
||||
else {
|
||||
m_lhs[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
|
||||
trail.push_back(m_lhs[head1]);
|
||||
}
|
||||
if (l == s2.length()) {
|
||||
++head2;
|
||||
}
|
||||
else {
|
||||
m_rhs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
|
||||
trail.push_back(m_rhs[head2]);
|
||||
}
|
||||
change = true;
|
||||
}
|
||||
|
@ -681,11 +676,9 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
|
|||
m_rhs.pop_back();
|
||||
if (l < s1.length()) {
|
||||
m_lhs.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
|
||||
trail.push_back(m_lhs.back());
|
||||
}
|
||||
if (l < s2.length()) {
|
||||
m_rhs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
|
||||
trail.push_back(m_rhs.back());
|
||||
}
|
||||
change = true;
|
||||
}
|
||||
|
|
|
@ -32,7 +32,7 @@ Notes:
|
|||
class seq_rewriter {
|
||||
seq_util m_util;
|
||||
arith_util m_autil;
|
||||
ptr_vector<expr> m_es, m_lhs, m_rhs;
|
||||
expr_ref_vector m_es, m_lhs, m_rhs;
|
||||
|
||||
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_seq_length(expr* a, expr_ref& result);
|
||||
|
@ -63,7 +63,7 @@ class seq_rewriter {
|
|||
|
||||
public:
|
||||
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
|
||||
m_util(m), m_autil(m) {
|
||||
m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) {
|
||||
}
|
||||
ast_manager & m() const { return m_util.get_manager(); }
|
||||
family_id get_fid() const { return m_util.get_family_id(); }
|
||||
|
|
|
@ -626,7 +626,7 @@ bool seq_util::str::is_string(expr const* n, zstring& s) const {
|
|||
}
|
||||
|
||||
|
||||
void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
|
||||
void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
|
||||
expr* e1, *e2;
|
||||
while (is_concat(e, e1, e2)) {
|
||||
get_concat(e1, es);
|
||||
|
|
|
@ -271,7 +271,7 @@ public:
|
|||
MATCH_BINARY(is_in_re);
|
||||
MATCH_UNARY(is_unit);
|
||||
|
||||
void get_concat(expr* e, ptr_vector<expr>& es) const;
|
||||
void get_concat(expr* e, expr_ref_vector& es) const;
|
||||
expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }
|
||||
};
|
||||
|
||||
|
|
|
@ -815,7 +815,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void setup::setup_seq() {
|
||||
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
|
||||
m_context.register_plugin(alloc(theory_seq, m_manager));
|
||||
}
|
||||
|
||||
void setup::setup_card() {
|
||||
|
|
|
@ -145,6 +145,7 @@ theory_seq::theory_seq(ast_manager& m):
|
|||
}
|
||||
|
||||
theory_seq::~theory_seq() {
|
||||
m_trail_stack.reset();
|
||||
}
|
||||
|
||||
|
||||
|
@ -157,6 +158,9 @@ final_check_status theory_seq::final_check_eh() {
|
|||
if (simplify_and_solve_eqs()) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (solve_nqs()) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (ctx.inconsistent()) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
|
@ -209,7 +213,7 @@ bool theory_seq::check_ineqs() {
|
|||
bool theory_seq::branch_variable() {
|
||||
context& ctx = get_context();
|
||||
unsigned sz = m_eqs.size();
|
||||
ptr_vector<expr> ls, rs;
|
||||
expr_ref_vector ls(m), rs(m);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
unsigned k = (i + m_branch_variable_head) % sz;
|
||||
eq e = m_eqs[k];
|
||||
|
@ -218,11 +222,11 @@ bool theory_seq::branch_variable() {
|
|||
m_util.str.get_concat(e.m_lhs, ls);
|
||||
m_util.str.get_concat(e.m_rhs, rs);
|
||||
|
||||
if (!ls.empty() && find_branch_candidate(ls[0], rs)) {
|
||||
if (!ls.empty() && find_branch_candidate(ls[0].get(), rs)) {
|
||||
m_branch_variable_head = k;
|
||||
return true;
|
||||
}
|
||||
if (!rs.empty() && find_branch_candidate(rs[0], ls)) {
|
||||
if (!rs.empty() && find_branch_candidate(rs[0].get(), ls)) {
|
||||
m_branch_variable_head = k;
|
||||
return true;
|
||||
}
|
||||
|
@ -230,7 +234,7 @@ bool theory_seq::branch_variable() {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::find_branch_candidate(expr* l, ptr_vector<expr> const& rs) {
|
||||
bool theory_seq::find_branch_candidate(expr* l, expr_ref_vector const& rs) {
|
||||
|
||||
TRACE("seq", tout << mk_pp(l, m) << " "
|
||||
<< (is_var(l)?"var":"not var") << "\n";);
|
||||
|
@ -434,8 +438,7 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) {
|
|||
set_conflict(deps);
|
||||
return true;
|
||||
}
|
||||
if (lhs.size() == 1 && l == lhs[0].get() &&
|
||||
rhs.size() == 1 && r == rhs[0].get()) {
|
||||
if (unchanged(l, lhs) && unchanged(r, rhs)) {
|
||||
return false;
|
||||
}
|
||||
SASSERT(lhs.size() == rhs.size());
|
||||
|
@ -558,8 +561,115 @@ bool theory_seq::pre_process_eqs(bool simplify_or_solve) {
|
|||
return change;
|
||||
}
|
||||
|
||||
bool theory_seq::solve_nqs() {
|
||||
bool change = false;
|
||||
context & ctx = get_context();
|
||||
for (unsigned i = 0; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
|
||||
change = solve_ne(i) || change;
|
||||
if (m_nqs[i].is_solved()) {
|
||||
m_nqs.erase_and_swap(i);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
return change;
|
||||
}
|
||||
|
||||
bool theory_seq::solve_ne(unsigned idx) {
|
||||
context& ctx = get_context();
|
||||
seq_rewriter rw(m);
|
||||
bool change = false;
|
||||
ne const& n = m_nqs[idx];
|
||||
TRACE("seq", display_disequation(tout, n););
|
||||
|
||||
SASSERT(!n.is_solved());
|
||||
for (unsigned i = 0; i < n.m_lits.size(); ++i) {
|
||||
switch (ctx.get_assignment(n.m_lits[i])) {
|
||||
case l_true:
|
||||
erase_lit(idx, i);
|
||||
--i;
|
||||
break;
|
||||
case l_false:
|
||||
// mark as solved in
|
||||
mark_solved(idx);
|
||||
return false;
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < n.m_lhs.size(); ++i) {
|
||||
expr_ref_vector lhs(m), rhs(m);
|
||||
enode_pair_dependency* deps = 0;
|
||||
expr* l = n.m_lhs[i];
|
||||
expr* r = n.m_rhs[i];
|
||||
expr_ref lh = canonize(l, deps);
|
||||
expr_ref rh = canonize(r, deps);
|
||||
if (!rw.reduce_eq(lh, rh, lhs, rhs)) {
|
||||
mark_solved(idx);
|
||||
return change;
|
||||
}
|
||||
else if (unchanged(l, lhs) && unchanged(r, rhs)) {
|
||||
// continue
|
||||
}
|
||||
else if (unchanged(r, lhs) && unchanged(l, rhs)) {
|
||||
// continue
|
||||
}
|
||||
else {
|
||||
TRACE("seq", tout << lhs.size() << "\n";
|
||||
for (unsigned j = 0; j < lhs.size(); ++j) {
|
||||
tout << mk_pp(lhs[j].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << mk_pp(l, m) << " != " << mk_pp(r, m) << "\n";);
|
||||
|
||||
for (unsigned j = 0; j < lhs.size(); ++j) {
|
||||
expr_ref nl(lhs[j].get(), m);
|
||||
expr_ref nr(rhs[j].get(), m);
|
||||
if (m_util.is_seq(nl) || m_util.is_re(nl)) {
|
||||
//std::cout << "push_ne " << nl << " != " << nr << "\n";
|
||||
m_trail_stack.push(push_ne(*this, idx, nl, nr));
|
||||
}
|
||||
else {
|
||||
//std::cout << "push_lit\n";
|
||||
literal lit(mk_eq(nl, nr, false));
|
||||
m_trail_stack.push(push_lit(*this, idx, ~lit));
|
||||
ctx.mark_as_relevant(lit);
|
||||
}
|
||||
}
|
||||
m_trail_stack.push(push_dep(*this, idx, deps));
|
||||
erase_index(idx, i);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
if (n.m_lits.empty() && n.m_lhs.empty()) {
|
||||
set_conflict(n.m_dep);
|
||||
return true;
|
||||
}
|
||||
return change;
|
||||
}
|
||||
|
||||
void theory_seq::erase_lit(unsigned idx, unsigned i) {
|
||||
ne const& n = m_nqs[idx];
|
||||
if (n.m_lits.size() < i + 1) {
|
||||
m_trail_stack.push(set_lit(*this, idx, i, n.m_lits.back()));
|
||||
}
|
||||
m_trail_stack.push(pop_lit(*this, idx));
|
||||
}
|
||||
|
||||
void theory_seq::mark_solved(unsigned idx) {
|
||||
m_trail_stack.push(solved_ne(*this, idx));
|
||||
}
|
||||
|
||||
void theory_seq::erase_index(unsigned idx, unsigned i) {
|
||||
ne const& n = m_nqs[idx];
|
||||
unsigned sz = n.m_lhs.size();
|
||||
if (i + 1 != sz) {
|
||||
m_trail_stack.push(set_ne(*this, idx, i, n.m_lhs[sz-1], n.m_rhs[sz-1]));
|
||||
}
|
||||
m_trail_stack.push(pop_ne(*this, idx));
|
||||
}
|
||||
|
||||
bool theory_seq::simplify_and_solve_eqs() {
|
||||
context & ctx = get_context();
|
||||
context & ctx = get_context();
|
||||
bool change = simplify_eqs();
|
||||
while (!ctx.inconsistent() && solve_basic_eqs()) {
|
||||
simplify_eqs();
|
||||
|
@ -620,6 +730,7 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
|
|||
|
||||
void theory_seq::display(std::ostream & out) const {
|
||||
if (m_eqs.size() == 0 &&
|
||||
m_nqs.size() == 0 &&
|
||||
m_ineqs.empty() &&
|
||||
m_rep.empty() &&
|
||||
m_exclude.empty()) {
|
||||
|
@ -630,6 +741,10 @@ void theory_seq::display(std::ostream & out) const {
|
|||
out << "Equations:\n";
|
||||
display_equations(out);
|
||||
}
|
||||
if (m_nqs.size() > 0) {
|
||||
out << "Disequations:\n";
|
||||
display_disequations(out);
|
||||
}
|
||||
if (!m_ineqs.empty()) {
|
||||
out << "Negative constraints:\n";
|
||||
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
|
||||
|
@ -654,6 +769,25 @@ void theory_seq::display_equations(std::ostream& out) const {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_seq::display_disequations(std::ostream& out) const {
|
||||
for (unsigned i = 0; i < m_nqs.size(); ++i) {
|
||||
display_disequation(out, m_nqs[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
|
||||
for (unsigned j = 0; j < e.m_lits.size(); ++j) {
|
||||
out << e.m_lits[j] << " ";
|
||||
}
|
||||
if (e.m_lits.size() > 0) {
|
||||
out << "\n";
|
||||
}
|
||||
for (unsigned j = 0; j < e.m_lhs.size(); ++j) {
|
||||
out << mk_pp(e.m_lhs[j], m) << " != " << mk_pp(e.m_rhs[j], m) << "\n";
|
||||
}
|
||||
display_deps(out, e.m_dep);
|
||||
}
|
||||
|
||||
void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const {
|
||||
vector<enode_pair, false> _eqs;
|
||||
const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
|
||||
|
@ -735,9 +869,6 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
|
|||
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
|
||||
result = e;
|
||||
}
|
||||
else if (m.is_eq(e, e1, e2)) {
|
||||
result = m.mk_eq(expand(e1, deps), expand(e2, deps));
|
||||
}
|
||||
else if (m_util.str.is_prefix(e, e1, e2)) {
|
||||
result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps));
|
||||
}
|
||||
|
@ -762,6 +893,9 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
|
|||
else {
|
||||
result = e;
|
||||
}
|
||||
if (result == e) {
|
||||
deps = 0;
|
||||
}
|
||||
expr_dep edr(result, deps);
|
||||
m_rep.add_cache(e, edr);
|
||||
eqs = m_dm.mk_join(eqs, deps);
|
||||
|
@ -1164,6 +1298,13 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
|
|||
}
|
||||
}
|
||||
else {
|
||||
//if (m_util.str.is_prefix(e, e1, e2)) {
|
||||
// could add negative prefix axioms:
|
||||
// len(e1) <= len(e2) => e2 = seq.prefix.left(e2)*seq.prefix.right(e2)
|
||||
// & len(seq.prefix.left(e2)) = len(e1)
|
||||
// & seq.prefix.left(e2) != e1
|
||||
// or could solve prefix/suffix disunification constraints.
|
||||
//}
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
|
||||
m_ineqs.push_back(e);
|
||||
}
|
||||
|
@ -1181,15 +1322,15 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
|
|||
}
|
||||
|
||||
void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
|
||||
expr* e1 = get_enode(v1)->get_owner();
|
||||
expr* e2 = get_enode(v2)->get_owner();
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
|
||||
m_ineqs.push_back(mk_eq_atom(e1, e2));
|
||||
enode* n1 = get_enode(v1);
|
||||
enode* n2 = get_enode(v2);
|
||||
expr_ref e1(n1->get_owner(), m);
|
||||
expr_ref e2(n2->get_owner(), m);
|
||||
m_nqs.push_back(ne(e1, e2, m_dm.mk_leaf(enode_pair(n1, n2))));
|
||||
m_exclude.update(e1, e2);
|
||||
}
|
||||
|
||||
void theory_seq::push_scope_eh() {
|
||||
TRACE("seq", tout << "push " << m_eqs.size() << "\n";);
|
||||
theory::push_scope_eh();
|
||||
m_rep.push_scope();
|
||||
m_exclude.push_scope();
|
||||
|
@ -1197,16 +1338,17 @@ void theory_seq::push_scope_eh() {
|
|||
m_trail_stack.push_scope();
|
||||
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
|
||||
m_eqs.push_scope();
|
||||
m_nqs.push_scope();
|
||||
}
|
||||
|
||||
void theory_seq::pop_scope_eh(unsigned num_scopes) {
|
||||
TRACE("seq", tout << "pop " << m_eqs.size() << "\n";);
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
m_dm.pop_scope(num_scopes);
|
||||
m_rep.pop_scope(num_scopes);
|
||||
m_exclude.pop_scope(num_scopes);
|
||||
m_eqs.pop_scopes(num_scopes);
|
||||
m_eqs.pop_scope(num_scopes);
|
||||
m_nqs.pop_scope(num_scopes);
|
||||
}
|
||||
|
||||
void theory_seq::restart_eh() {
|
||||
|
|
|
@ -104,6 +104,136 @@ namespace smt {
|
|||
eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
|
||||
};
|
||||
|
||||
|
||||
// asserted or derived disqequality with dependencies
|
||||
struct ne {
|
||||
bool m_solved;
|
||||
expr_ref_vector m_lhs;
|
||||
expr_ref_vector m_rhs;
|
||||
literal_vector m_lits;
|
||||
enode_pair_dependency* m_dep;
|
||||
ne(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
|
||||
m_solved(false), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(d) {
|
||||
m_lhs.push_back(l);
|
||||
m_rhs.push_back(r);
|
||||
}
|
||||
ne(ne const& other):
|
||||
m_solved(other.m_solved), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
|
||||
ne& operator=(ne const& other) {
|
||||
m_solved = other.m_solved;
|
||||
m_lhs.reset(); m_lhs.append(other.m_lhs);
|
||||
m_rhs.reset(); m_rhs.append(other.m_rhs);
|
||||
m_lits.reset(); m_lits.append(other.m_lits);
|
||||
m_dep = other.m_dep;
|
||||
return *this;
|
||||
}
|
||||
bool is_solved() const { return m_solved; }
|
||||
};
|
||||
|
||||
class pop_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
literal m_lit;
|
||||
public:
|
||||
pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) {
|
||||
th.m_nqs.ref(m_idx).m_lits.pop_back();
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); }
|
||||
};
|
||||
class push_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) {
|
||||
th.m_nqs.ref(m_idx).m_lits.push_back(lit);
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); }
|
||||
};
|
||||
class set_lit : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
unsigned m_i;
|
||||
literal m_lit;
|
||||
public:
|
||||
set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit):
|
||||
m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) {
|
||||
th.m_nqs.ref(m_idx).m_lits[i] = lit;
|
||||
}
|
||||
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }
|
||||
};
|
||||
void erase_lit(unsigned idx, unsigned i);
|
||||
|
||||
class solved_ne : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; }
|
||||
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false; }
|
||||
};
|
||||
void mark_solved(unsigned idx);
|
||||
|
||||
class push_ne : public trail<theory_seq> {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) {
|
||||
th.m_nqs.ref(m_idx).m_lhs.push_back(l);
|
||||
th.m_nqs.ref(m_idx).m_rhs.push_back(r);
|
||||
}
|
||||
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); }
|
||||
};
|
||||
|
||||
class pop_ne : public trail<theory_seq> {
|
||||
expr_ref m_lhs;
|
||||
expr_ref m_rhs;
|
||||
unsigned m_idx;
|
||||
public:
|
||||
pop_ne(theory_seq& th, unsigned idx):
|
||||
m_lhs(th.m_nqs[idx].m_lhs.back(), th.m),
|
||||
m_rhs(th.m_nqs[idx].m_rhs.back(), th.m),
|
||||
m_idx(idx) {
|
||||
th.m_nqs.ref(idx).m_lhs.pop_back();
|
||||
th.m_nqs.ref(idx).m_rhs.pop_back();
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs);
|
||||
th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs);
|
||||
m_lhs.reset();
|
||||
m_rhs.reset();
|
||||
}
|
||||
};
|
||||
|
||||
class set_ne : public trail<theory_seq> {
|
||||
expr_ref m_lhs;
|
||||
expr_ref m_rhs;
|
||||
unsigned m_idx;
|
||||
unsigned m_i;
|
||||
public:
|
||||
set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r):
|
||||
m_lhs(th.m_nqs[idx].m_lhs[i], th.m),
|
||||
m_rhs(th.m_nqs[idx].m_rhs[i], th.m),
|
||||
m_idx(idx),
|
||||
m_i(i) {
|
||||
th.m_nqs.ref(idx).m_lhs[i] = l;
|
||||
th.m_nqs.ref(idx).m_rhs[i] = r;
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs;
|
||||
th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs;
|
||||
m_lhs.reset();
|
||||
m_rhs.reset();
|
||||
}
|
||||
};
|
||||
|
||||
class push_dep : public trail<theory_seq> {
|
||||
enode_pair_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) {
|
||||
th.m_nqs.ref(idx).m_dep = d;
|
||||
}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_nqs.ref(m_idx).m_dep = m_dep;
|
||||
}
|
||||
};
|
||||
|
||||
void erase_index(unsigned idx, unsigned i);
|
||||
|
||||
struct stats {
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(stats)); }
|
||||
|
@ -114,6 +244,7 @@ namespace smt {
|
|||
enode_pair_dependency_manager m_dm;
|
||||
solution_map m_rep; // unification representative.
|
||||
scoped_vector<eq> m_eqs; // set of current equations.
|
||||
scoped_vector<ne> m_nqs; // set of current disequalities.
|
||||
|
||||
seq_factory* m_factory; // value factory
|
||||
expr_ref_vector m_ineqs; // inequalities to check solution against
|
||||
|
@ -174,13 +305,17 @@ namespace smt {
|
|||
bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
|
||||
bool solve_basic_eqs();
|
||||
|
||||
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);
|
||||
void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
|
||||
void propagate_eq(bool_var v, expr* e1, expr* e2);
|
||||
void set_conflict(enode_pair_dependency* dep);
|
||||
|
||||
bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
|
||||
bool find_branch_candidate(expr* l, expr_ref_vector const& rs);
|
||||
bool assume_equality(expr* l, expr* r);
|
||||
|
||||
// variable solving utilities
|
||||
|
@ -219,6 +354,8 @@ namespace smt {
|
|||
|
||||
// diagnostics
|
||||
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;
|
||||
public:
|
||||
theory_seq(ast_manager& m);
|
||||
|
|
|
@ -46,7 +46,7 @@ public:
|
|||
m_elems_lim.push_back(m_elems_start);
|
||||
}
|
||||
|
||||
void pop_scopes(unsigned num_scopes) {
|
||||
void pop_scope(unsigned num_scopes) {
|
||||
if (num_scopes == 0) return;
|
||||
unsigned new_size = m_sizes.size() - num_scopes;
|
||||
unsigned src_lim = m_src_lim[new_size];
|
||||
|
@ -72,6 +72,12 @@ public:
|
|||
return m_elems[m_index[idx]];
|
||||
}
|
||||
|
||||
// breaks abstraction, caller must ensure backtracking.
|
||||
T& ref(unsigned idx) {
|
||||
SASSERT(idx < m_size);
|
||||
return m_elems[m_index[idx]];
|
||||
}
|
||||
|
||||
void set(unsigned idx, T const& t) {
|
||||
SASSERT(idx < m_size);
|
||||
unsigned n = m_index[idx];
|
||||
|
@ -102,6 +108,13 @@ public:
|
|||
SASSERT(invariant());
|
||||
}
|
||||
|
||||
void erase_and_swap(unsigned i) {
|
||||
if (i + 1 < size()) {
|
||||
set(i, m_elems[m_index[i]]);
|
||||
}
|
||||
pop_back();
|
||||
}
|
||||
|
||||
unsigned size() const { return m_size; }
|
||||
|
||||
bool empty() const { return m_size == 0; }
|
||||
|
|
Loading…
Reference in a new issue