diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 061f403e3..0a3f880b7 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -130,8 +130,7 @@ namespace qe { visited.mark(e, true); } } - for (unsigned i = 0; i < conjs.size(); ++i) { - expr* e = conjs[i].get(); + for (expr* e : conjs) { bool cv = contains_var.is_marked(e); bool cu = contains_uf.is_marked(e); if (cv && cu) { @@ -989,11 +988,11 @@ namespace qe { todo.pop_back(); if (st->m_children.empty() && st->fml() && st->m_vars.empty() && !st->has_var()) { + TRACE("qe", st->display(tout << "appending leaf\n");); result.push_back(st->fml()); } - for (unsigned i = 0; i < st->m_children.size(); ++i) { - todo.push_back(st->m_children[i]); - } + for (auto * ch : st->m_children) + todo.push_back(ch); } } @@ -1020,9 +1019,7 @@ namespace qe { void reset() { TRACE("qe",tout << "resetting\n";); - for (unsigned i = 0; i < m_children.size(); ++i) { - dealloc(m_children[i]); - } + for (auto* ch : m_children) dealloc(ch); m_pos.reset(); m_neg.reset(); m_children.reset(); @@ -1046,9 +1043,10 @@ namespace qe { } unsigned num_free_vars() const { return m_vars.size(); } - app* const* free_vars() const { return m_vars.c_ptr(); } + // app* const* free_vars() const { return m_vars.c_ptr(); } + app_ref_vector const& free_vars() const { return m_vars; } app* free_var(unsigned i) const { return m_vars[i]; } - void reset_free_vars() { m_vars.reset(); } + void reset_free_vars() { TRACE("qe", tout << m_vars << "\n";); m_vars.reset(); } atom_set const& pos_atoms() const { return m_pos; } atom_set const& neg_atoms() const { return m_neg; } @@ -1119,7 +1117,7 @@ namespace qe { st->init(fml); st->m_vars.append(m_vars.size(), m_vars.c_ptr()); SASSERT(invariant()); - TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";); + TRACE("qe", display_node(tout); st->display_node(tout);); return st; } @@ -1133,7 +1131,7 @@ namespace qe { m_branch_index.insert(branch_id, index); st->m_vars.append(m_vars.size(), m_vars.c_ptr()); SASSERT(invariant()); - //TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";); + TRACE("qe", display_node(tout); st->display_node(tout);); return st; } @@ -1141,27 +1139,29 @@ namespace qe { display(out, ""); } - void display(std::ostream& out, char const* indent) const { - - out << indent << "node\n"; + void display_node(std::ostream& out, char const* indent = "") const { + out << indent << "node " << std::hex << this << std::dec << "\n"; if (m_var) { - out << indent << " var: " << mk_ismt2_pp(m_var.get(), m) << "\n"; + out << indent << " var: " << m_var << "\n"; } - for (unsigned i = 0; i < m_vars.size(); ++i) { - out << indent << " free: " << mk_ismt2_pp(m_vars[i], m) << "\n"; + for (app* v : m_vars) { + out << indent << " free: " << mk_pp(v, m) << "\n"; } if (m_fml) { - out << indent << " fml: " << mk_ismt2_pp(m_fml.get(), m) << "\n"; + out << indent << " fml: " << m_fml << "\n"; } for (unsigned i = 0; i < m_def.size(); ++i) { out << indent << " def: " << m_def.var(i)->get_name() << " = " << mk_ismt2_pp(m_def.def(i), m) << "\n"; } out << indent << " branches: " << m_num_branches << "\n"; + } + void display(std::ostream& out, char const* indent) const { + display_node(out, indent); std::string new_indent(indent); new_indent += " "; - for (unsigned i = 0; i < m_children.size(); ++i) { - m_children[i]->display(out, new_indent.c_str()); + for (auto * ch : m_children) { + ch->display(out, new_indent.c_str()); } } @@ -1214,6 +1214,7 @@ namespace qe { out << "(push)\n"; pp.display_smt2(out, fml); out << "(pop)\n\n"; +#if 0 DEBUG_CODE( smt_params params; params.m_simplify_bit2int = true; @@ -1227,7 +1228,8 @@ namespace qe { std::cout << "; Validation failed:\n"; std::cout << mk_pp(fml, m) << "\n"; } -); + ); +#endif } for (unsigned i = 0; i < m_children.size(); ++i) { @@ -1486,9 +1488,7 @@ namespace qe { tout << "subformula: " << mk_ismt2_pp(m_subfml, m) << "\n"; m_root.display(tout); m_root.display_validate(tout); - for (unsigned i = 0; i < m_free_vars.size(); ++i) tout << mk_ismt2_pp(m_free_vars[i].get(), m) << " "; - tout << "\n"; - ); + tout << "free: " << m_free_vars << "\n";); free_vars.append(m_free_vars); if (!m_free_vars.empty() || m_solver.inconsistent()) { @@ -1546,14 +1546,14 @@ namespace qe { app* get_var(unsigned idx) const { return m_current->free_var(idx); } - app* const* get_vars() const { return m_current->free_vars(); } + app_ref_vector const& get_vars() const { return m_current->free_vars(); } contains_app& contains(unsigned idx) { return contains(get_var(idx)); } // // The variable at idx is eliminated (without branching). // - void elim_var(unsigned idx, expr* _fml, expr* def) { + void elim_var(unsigned idx, expr* _fml, expr* def) override { app* x = get_var(idx); expr_ref fml(_fml, m); TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(def, m) << "\n";); @@ -1598,7 +1598,7 @@ namespace qe { add_literal(l3); expr_ref fml(m); fml = m.mk_or(m_literals.size(), m_literals.c_ptr()); - TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";); + TRACE("qe", tout << fml << "\n";); m_solver.assert_expr(fml); } @@ -1654,9 +1654,7 @@ namespace qe { } app* get_branch_id(app* x) { - app* result = 0; - VERIFY (m_var2branch.find(x, result)); - return result; + return m_var2branch[x]; } bool extract_partition(ptr_vector& vars) { @@ -1912,6 +1910,7 @@ namespace qe { } m_current->set_var(x, k); + TRACE("qe", tout << mk_pp(x, m) << " := " << k << "\n";); if (m_bv.is_bv(x)) { return; } @@ -1952,7 +1951,7 @@ namespace qe { vars.reset(); closed = closed && (r != l_undef); } - TRACE("qe", tout << mk_pp(fml, m) << "\n";); + TRACE("qe", tout << fml << " free: " << m_current->free_vars() << "\n";); m_current->add_child(fml)->reset_free_vars(); block_assignment(); } @@ -1961,9 +1960,7 @@ namespace qe { // variable queueing. contains_app& contains(app* x) { - contains_app* result = 0; - VERIFY(m_var2contains.find(x, result)); - return *result; + return *m_var2contains[x]; } bool find_min_weight(app*& x, rational& num_branches) { @@ -2003,6 +2000,7 @@ namespace qe { bool solved = true; while (solved) { expr_ref fml(m_current->fml(), m); + TRACE("qe", tout << fml << "\n";); conj_enum conjs(m, fml); solved = false; for (unsigned i = 0; !solved && i < m_plugins.size(); ++i) { @@ -2512,7 +2510,7 @@ namespace qe { // Access current set of variables to solve virtual unsigned get_num_vars() const { return m_vars->size(); } virtual app* get_var(unsigned idx) const { return (*m_vars)[idx].get(); } - virtual app*const* get_vars() const { return m_vars->c_ptr(); } + virtual app_ref_vector const& get_vars() const { return *m_vars; } virtual bool is_var(expr* e, unsigned& idx) const { for (unsigned i = 0; i < m_vars->size(); ++i) { if ((*m_vars)[i].get() == e) { @@ -2540,6 +2538,7 @@ namespace qe { // callback to add new variable to branch. virtual void add_var(app* x) { + TRACE("qe", tout << "add var: " << mk_pp(x, m) << "\n";); m_vars->push_back(x); } diff --git a/src/qe/qe.h b/src/qe/qe.h index b6754b384..6946f9566 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -86,7 +86,7 @@ namespace qe { // Access current set of variables to solve virtual unsigned get_num_vars() const = 0; virtual app* get_var(unsigned idx) const = 0; - virtual app*const* get_vars() const = 0; + virtual app_ref_vector const& get_vars() const = 0; virtual bool is_var(expr* e, unsigned& idx) const; virtual contains_app& contains(unsigned idx) = 0; diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 1085ec3c2..89dee9586 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -105,6 +105,7 @@ namespace qe { public: arith_util m_arith; // initialize before m_zero_i, etc. th_rewriter simplify; + app_ref_vector m_vars_added; private: arith_eq_solver m_arith_solver; bv_util m_bv; @@ -126,6 +127,7 @@ namespace qe { m_ctx(ctx), m_arith(m), simplify(m), + m_vars_added(m), m_arith_solver(m), m_bv(m), m_zero_i(m_arith.mk_numeral(numeral(0), true), m), @@ -783,6 +785,11 @@ namespace qe { } } + void add_var(app* v, bool track = true) { + m_ctx.add_var(v); + if (track) m_vars_added.push_back(v); + } + private: @@ -850,10 +857,11 @@ namespace qe { << mk_pp(result, m) << "\n";); } + void mk_big_or_symbolic(numeral up, app* x, expr* body, expr_ref& result) { app_ref z_bv(m); mk_big_or_symbolic(up, x, body, z_bv, result); - m_ctx.add_var(z_bv); + add_var(z_bv); } void mk_big_or_symbolic_blast(numeral up, app* x, expr* body, expr_ref& result) { @@ -999,9 +1007,9 @@ namespace qe { bool solve_linear(expr* p, expr* fml) { vector values; unsigned num_vars = m_ctx.get_num_vars(); - app*const* vars_ptr = m_ctx.get_vars(); + app_ref_vector const& vars = m_ctx.get_vars(); - if (!is_linear(p, num_vars, vars_ptr, values)) { + if (!is_linear(p, num_vars, vars.c_ptr(), values)) { return false; } @@ -1025,7 +1033,7 @@ namespace qe { // it has coefficient 'm' = values[index]. SASSERT(values[index] >= rational(3)); z = m.mk_fresh_const("x", m_arith.mk_int()); - m_ctx.add_var(z); + add_var(z); p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], true), z); } else { @@ -1475,16 +1483,18 @@ public: expr* m_result; rational m_coeff; expr* m_term; + ptr_vector m_vars; branch_formula(): m_fml(0), m_var(0), m_branch(0), m_result(0), m_term(0) {} - branch_formula(expr* fml, app* var, unsigned b, expr* r, rational coeff, expr* term): + branch_formula(expr* fml, app* var, unsigned b, expr* r, rational coeff, expr* term, app_ref_vector const& vars): m_fml(fml), m_var(var), m_branch(b), m_result(r), m_coeff(coeff), - m_term(term) + m_term(term), + m_vars(vars.size(), vars.c_ptr()) {} unsigned mk_hash() const { @@ -1544,6 +1554,7 @@ public: if (get_cache(x, fml, v, result)) { return; } + m_util.m_vars_added.reset(); bounds_proc& bounds = get_bounds(x, fml); bool is_lower = get_bound_sizes(bounds, x, t_size, e_size); @@ -1601,8 +1612,7 @@ public: expr_ref t(bounds.exprs(is_strict, is_lower)[index], m); rational a = bounds.coeffs(is_strict, is_lower)[index]; - - + mk_bounds(bounds, x, true, is_eq, is_strict, is_lower, index, a, t, result); mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result); @@ -1617,7 +1627,7 @@ public: { tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n"; tout << mk_pp(fml, m) << "\n"; - tout << mk_pp(result, m) << "\n"; + tout << result << "\n"; } ); } @@ -1637,7 +1647,7 @@ public: virtual void subst(contains_app& contains_x, rational const& vl, expr_ref& fml, expr_ref* def) { SASSERT(vl.is_unsigned()); - if (def) { + if (def) { get_def(contains_x, vl.get_unsigned(), fml, *def); } VERIFY(get_cache(contains_x.x(), fml, vl.get_unsigned(), fml)); @@ -1740,7 +1750,7 @@ public: x_subst x_t(m_util); bounds_proc& bounds = get_bounds(x, fml); branch_formula bf; - VERIFY (m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0), bf)); + VERIFY (m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0, m_util.m_vars_added), bf)); x_t.set_term(bf.m_term); x_t.set_coeff(bf.m_coeff); @@ -2022,16 +2032,19 @@ public: m_trail.push_back(fml); m_trail.push_back(result); if (term) m_trail.push_back(term); - m_subst.insert(branch_formula(fml, x, v, result, coeff, term)); + m_subst.insert(branch_formula(fml, x, v, result, coeff, term, m_util.m_vars_added)); } bool get_cache(app* x, expr* fml, unsigned v, expr_ref& result) { branch_formula bf; - if (!m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0), bf)) { + if (!m_subst.find(branch_formula(fml, x, v, 0, rational::zero(), 0, m_util.m_vars_added), bf)) { return false; } SASSERT(bf.m_result); result = bf.m_result; + for (app* v : bf.m_vars) { + m_util.add_var(v, false); + } return true; } @@ -2043,7 +2056,7 @@ public: if (!bounds.div_z(d, z_bv, z)) { return; } - m_ctx.add_var(z_bv); + m_util.add_var(z_bv); // // assert @@ -2120,7 +2133,7 @@ public: app* z1_bv = bounds.nested_div_z_bv(i); app* z1 = bounds.nested_div_z(i); - m_ctx.add_var(z1_bv); + m_util.add_var(z1_bv); // // assert diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 69ebc1a42..250ffff4a 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -122,7 +122,7 @@ namespace qe { // Access current set of variables to solve virtual unsigned get_num_vars() const { return m_vars.size(); } virtual app* get_var(unsigned idx) const { return m_vars[idx]; } - virtual app*const* get_vars() const { return m_vars.c_ptr(); } + virtual app_ref_vector const& get_vars() const { return m_vars; } virtual bool is_var(expr* e, unsigned& idx) const { for (unsigned i = 0; i < m_vars.size(); ++i) { if (e == m_vars[i]) return (idx = i, true);