mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

fix #436, adding more length-based propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-07 14:43:53 +00:00
parent fc1f37efc9
commit 677b4bf4fe
2 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_fpa.cpp
View file

@ -30,12 +30,13 @@ namespace smt {
expr * m_e; expr * m_e;
public: public:
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) : fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
m(m), m_conversions(c), m_e(e) {} m(m), m_conversions(c), m_e(e) { m.inc_ref(e); }
virtual ~fpa2bv_conversion_trail_elem() {} virtual ~fpa2bv_conversion_trail_elem() {}
virtual void undo(theory_fpa & th) { virtual void undo(theory_fpa & th) {
expr * v = m_conversions.find(m_e); expr * v = m_conversions.find(m_e);
m_conversions.remove(m_e); m_conversions.remove(m_e);
m.dec_ref(v); m.dec_ref(v);
m.dec_ref(m_e);
} }
}; };

18
src/smt/theory_seq.cpp
View file

@ -823,6 +823,23 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
} }
bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) { bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
rational val1, val2;
if (has_length(l) && has_length(r) &&
get_length(l, val1) && get_length(r, val2) && val1 == val2) {
context& ctx = get_context();
expr_ref len1(m_util.str.mk_length(l), m);
expr_ref len2(m_util.str.mk_length(r), m);
literal lit = mk_eq(len1, len2, false);
if (ctx.get_assignment(lit) == l_true) {
lits.push_back(lit);
return true;
}
else {
TRACE("seq", tout << "Assignment: " << len1 << " = " << len2 << " " << ctx.get_assignment(lit) << "\n";);
return false;
}
}
expr_ref len1(m), len2(m); expr_ref len1(m), len2(m);
lits.reset(); lits.reset();
if (get_length(l, len1, lits) && if (get_length(l, len1, lits) &&
@ -2431,6 +2448,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero)); literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero));
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey)); add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false)); add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
} }
/* /*