mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

pin elements in expr2depth

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-06 11:45:29 +01:00
parent eac659f748
commit 6df628edc7
5 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_implied_equalities.cpp
View file

@ -284,7 +284,7 @@ namespace smt {
} }
lbool reduce_cond(model_ref& model, expr* e) { lbool reduce_cond(model_ref& model, expr* e) {
expr* e1, *e2; expr* e1 = 0, *e2 = 0;
if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) { if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) {
if (e1 == e2) { if (e1 == e2) {
return l_true; return l_true;

2
src/smt/theory_lra.cpp
View file

@ -689,7 +689,7 @@ namespace smt {
SASSERT(!ctx().b_internalized(atom)); SASSERT(!ctx().b_internalized(atom));
bool_var bv = ctx().mk_bool_var(atom); bool_var bv = ctx().mk_bool_var(atom);
ctx().set_var_theory(bv, get_id()); ctx().set_var_theory(bv, get_id());
expr* n1, *n2; expr* n1 = 0, *n2 = 0;
rational r; rational r;
lra_lp::bound_kind k; lra_lp::bound_kind k;
theory_var v = null_theory_var; theory_var v = null_theory_var;

6
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -70,11 +70,13 @@ struct interval {
if (is_wrapped()) { if (is_wrapped()) {
// l >= b.l >= b.h >= h // l >= b.l >= b.h >= h
return b.is_wrapped() && h <= b.h && l >= b.l; return b.is_wrapped() && h <= b.h && l >= b.l;
} else if (b.is_wrapped()) { }
else if (b.is_wrapped()) {
// b.l > b.h >= h >= l // b.l > b.h >= h >= l
// h >= l >= b.l > b.h // h >= l >= b.l > b.h
return h <= b.h || l >= b.l; return h <= b.h || l >= b.l;
} else { }
else {
// //
return l >= b.l && h <= b.h; return l >= b.l && h <= b.h;
} }

2
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -430,6 +430,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) {
if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
compute_depth(lhs); compute_depth(lhs);
compute_depth(rhs); compute_depth(rhs);
m_trail.push_back(lhs);
m_trail.push_back(rhs);
if (is_gt(lhs, rhs)) { if (is_gt(lhs, rhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
m_scoped_substitution.insert(lhs, rhs, pr); m_scoped_substitution.insert(lhs, rhs, pr);

3
src/tactic/core/dom_simplify_tactic.h
View file

@ -146,6 +146,7 @@ class expr_substitution_simplifier : public dom_simplifier {
expr_substitution m_subst; expr_substitution m_subst;
scoped_expr_substitution m_scoped_substitution; scoped_expr_substitution m_scoped_substitution;
obj_map<expr, unsigned> m_expr2depth; obj_map<expr, unsigned> m_expr2depth;
expr_ref_vector m_trail;
// move from asserted_formulas to here.. // move from asserted_formulas to here..
void compute_depth(expr* e); void compute_depth(expr* e);
@ -153,7 +154,7 @@ class expr_substitution_simplifier : public dom_simplifier {
unsigned depth(expr* e) { return m_expr2depth[e]; } unsigned depth(expr* e) { return m_expr2depth[e]; }
public: public:
expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {} expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
virtual ~expr_substitution_simplifier() {} virtual ~expr_substitution_simplifier() {}
virtual bool assert_expr(expr * t, bool sign); virtual bool assert_expr(expr * t, bool sign);