mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

better behavior on disequality and branch selection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-30 22:10:33 -07:00
parent 02084dc95b
commit 4392c03b57
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_seq.cpp
View file

@ -3101,7 +3101,12 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
}
dependency* dep = m_dm.mk_leaf(assumption(~lit));
m_nqs.push_back(ne(e1, e2, dep));
expr_ref len1(m_util.str.mk_length(e1), m);
expr_ref len2(m_util.str.mk_length(e2), m);
m_rewrite(len1);
m_rewrite(len2);
literal eqlen = mk_eq(len1, len2, false);
m_nqs.push_back(ne(e1, e2, eqlen, dep));
if (ctx.get_assignment(lit) != l_undef) {
solve_nqs(m_nqs.size() - 1);
}

3
src/smt/theory_seq.h
View file

@ -178,11 +178,12 @@ namespace smt {
literal_vector m_lits;
dependency* m_dep;
public:
ne(expr_ref const& l, expr_ref const& r, dependency* dep):
ne(expr_ref const& l, expr_ref const& r, literal eqlen, dependency* dep):
m_l(l), m_r(r), m_dep(dep) {
expr_ref_vector ls(l.get_manager()); ls.push_back(l);
expr_ref_vector rs(r.get_manager()); rs.push_back(r);
m_eqs.push_back(std::make_pair(ls, rs));
m_lits.push_back(eqlen);
}
ne(expr_ref const& _l, expr_ref const& _r, vector<decomposed_eq> const& eqs, literal_vector const& lits, dependency* dep):