mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

enabling upper bound test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-10-31 09:43:15 -07:00
parent 637b63cbe1
commit 72e82532b2
9 changed files with 82 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/opt/opt_solver.cpp
View file

@ -77,6 +77,9 @@ namespace opt {
else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) {
return dynamic_cast<smt::theory_i_arith&>(*arith_theory);
}
else if (typeid(smt::theory_inf_arith) == typeid(*arith_theory)) {
return dynamic_cast<smt::theory_inf_arith&>(*arith_theory);
}
else if (typeid(smt::theory_rdl&) == typeid(*arith_theory)) {
return dynamic_cast<smt::theory_rdl&>(*arith_theory);
}
@ -172,7 +175,8 @@ namespace opt {
return expr_ref(m.mk_true(), m);
}
else {
return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], val.get_numeral()), m);
inf_rational n = val.get_numeral();
return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], n), m);
}
}

1
src/opt/opt_solver.h
View file

@ -91,7 +91,6 @@ namespace opt {
smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
private:
smt::theory_opt& get_optimizer();
};
}

63
src/opt/optimize_objectives.cpp
View file

@ -66,24 +66,16 @@ namespace opt {
*/
lbool optimize_objectives::basic_opt(app_ref_vector& objectives) {
arith_util autil(m);
s->reset_objectives();
m_lower.reset();
m_upper.reset();
// First check_sat call to initialize theories
lbool is_sat = s->check_sat(0, 0);
if (is_sat != l_true) {
return is_sat;
}
opt_solver::scoped_push _push(*s);
opt_solver::toggle_objective _t(*s, true);
for (unsigned i = 0; i < objectives.size(); ++i) {
s->add_objective(objectives[i].get());
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
m_vars.push_back(s->add_objective(objectives[i].get()));
}
lbool is_sat = l_true;
// ready to test: is_sat = update_upper();
while (is_sat == l_true && !m_cancel) {
is_sat = update_lower();
}
@ -117,8 +109,31 @@ namespace opt {
}
lbool optimize_objectives::update_upper() {
NOT_IMPLEMENTED_YET();
return l_undef;
smt::theory_opt& opt = s->get_optimizer();
if (typeid(smt::theory_inf_arith) != typeid(opt)) {
return l_true;
}
smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt);
expr_ref bound(m);
lbool is_sat = l_true;
for (unsigned i = 0; i < m_lower.size(); ++i) {
if (m_lower[i] < m_upper[i]) {
opt_solver::scoped_push _push(*s);
smt::theory_var v = m_vars[i];
bound = th.block_upper_bound(v, m_upper[i]);
expr* bounds[1] = { bound };
is_sat = s->check_sat(1, bounds);
if (is_sat) {
IF_VERBOSE(1, verbose_stream() << "Setting lower bound for " << v << " to " << m_upper[i] << "\n";);
m_lower[i] = m_upper[i];
}
// else: TBD extract Farkas coefficients.
}
}
return l_true;
}
/**
@ -127,10 +142,22 @@ namespace opt {
*/
lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector<inf_eps>& values) {
s = &solver;
lbool result = basic_opt(objectives);
values.reset();
values.append(m_lower);
return result;
s->reset_objectives();
m_lower.reset();
m_upper.reset();
for (unsigned i = 0; i < objectives.size(); ++i) {
m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
}
// First check_sat call to initialize theories
lbool is_sat = s->check_sat(0, 0);
if (is_sat == l_true) {
is_sat = basic_opt(objectives);
values.reset();
values.append(m_lower);
}
return is_sat;
}
}

1
src/opt/optimize_objectives.h
View file

@ -33,6 +33,7 @@ namespace opt {
volatile bool m_cancel;
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
svector<smt::theory_var> m_vars;
public:
optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}

8
src/smt/theory_arith.h
View file

@ -273,14 +273,14 @@ namespace smt {
class atom : public bound {
protected:
bool_var m_bvar;
numeral m_k;
inf_numeral m_k;
unsigned m_atom_kind:2; // atom kind
unsigned m_is_true:1; // cache: true if the atom was assigned to true.
public:
atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind);
atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind);
atom_kind get_atom_kind() const { return static_cast<atom_kind>(m_atom_kind); }
virtual ~atom() {}
numeral const & get_k() const { return m_k; }
inf_numeral const & get_k() const { return m_k; }
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_is_true; }
void assign_eh(bool is_true, inf_numeral const & epsilon);
@ -999,7 +999,7 @@ namespace smt {
virtual theory_var add_objective(app* term);
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
virtual expr* block_upper_bound(theory_var v, inf_numeral const& val);
// -----------------------------------
//
// Pretty Printing

36
src/smt/theory_arith_aux.h
View file

@ -367,7 +367,7 @@ namespace smt {
// -----------------------------------
template<typename Ext>
theory_arith<Ext>::atom::atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind):
theory_arith<Ext>::atom::atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind):
bound(v, inf_numeral::zero(), B_LOWER, true),
m_bvar(bv),
m_k(k),
@ -997,6 +997,22 @@ namespace smt {
}
}
template<typename Ext>
expr* theory_arith<Ext>::block_upper_bound(theory_var v, inf_numeral const& val) {
ast_manager& m = get_manager();
context& ctx = get_context();
std::ostringstream strm;
strm << val << " <= " << v;
expr* b = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort());
bool_var bv = ctx.mk_bool_var(b);
atom* a = alloc(atom, bv, v, val, A_LOWER);
m_unassigned_atoms[v]++;
m_var_occs[v].push_back(a);
m_atoms.push_back(a);
insert_bv2a(bv, a);
return b;
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
return m_objective_value;
@ -1117,15 +1133,6 @@ namespace smt {
);
pivot<true>(x_i, x_j, a_ij, false);
TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n";
if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " ";
if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " ";
tout << "value x_i: " << get_value(x_i) << "\n";
if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " ";
if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
tout << "value x_j: " << get_value(x_j) << "\n";
);
SASSERT(is_non_base(x_i));
SASSERT(is_base(x_j));
@ -1137,15 +1144,6 @@ namespace smt {
move_xi_to_lower = a_ij.is_neg();
move_to_bound(x_i, move_xi_to_lower);
TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n";
if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " ";
if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " ";
tout << "value x_i: " << get_value(x_i) << "\n";
if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " ";
if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
tout << "value x_j: " << get_value(x_j) << "\n";
);
row & r2 = m_rows[get_var_row(x_j)];
coeff.neg();
add_tmp_row(r, coeff, r2);

8
src/smt/theory_arith_core.h
View file

@ -801,7 +801,7 @@ namespace smt {
void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
theory_var v = a1->get_var();
literal l1(a1->get_bool_var());
numeral const & k1(a1->get_k());
inf_numeral const & k1(a1->get_k());
atom_kind kind1 = a1->get_atom_kind();
TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";);
atoms & occs = m_var_occs[v];
@ -810,7 +810,7 @@ namespace smt {
for (; it != end; ++it) {
atom * a2 = *it;
literal l2(a2->get_bool_var());
numeral const & k2 = a2->get_k();
inf_numeral const & k2 = a2->get_k();
atom_kind kind2 = a2->get_atom_kind();
SASSERT(k1 != k2 || kind1 != kind2);
SASSERT(a2->get_var() == v);
@ -880,7 +880,7 @@ namespace smt {
ctx.set_var_theory(bv, get_id());
rational _k;
m_util.is_numeral(rhs, _k);
numeral k(_k);
inf_numeral k(_k);
atom * a = alloc(atom, bv, v, k, kind);
mk_bound_axioms(a);
m_unassigned_atoms[v]++;
@ -2475,7 +2475,7 @@ namespace smt {
bool_var bv = a->get_bool_var();
literal l(bv);
if (get_context().get_assignment(bv) == l_undef) {
numeral const & k2 = a->get_k();
inf_numeral const & k2 = a->get_k();
delta.reset();
if (a->get_atom_kind() == A_LOWER) {
// v >= k k >= k2 |- v >= k2

2
src/smt/theory_arith_pp.h
View file

@ -428,7 +428,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::display_atom(std::ostream & out, atom * a, bool show_sign) const {
theory_var v = a->get_var();
numeral const & k = a->get_k();
inf_numeral const & k = a->get_k();
enode * e = get_enode(v);
if (show_sign) {
if (!a->is_true())

8
src/smt/theory_opt.h
View file

@ -27,14 +27,16 @@ Notes:
namespace smt {
class theory_opt {
public:
typedef inf_eps_rational<inf_rational> inf_eps;
virtual bool maximize(theory_var v) { UNREACHABLE(); return false; };
virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v) {
virtual inf_eps get_objective_value(theory_var v) {
UNREACHABLE();
inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
return r;
return inf_eps(rational(1), inf_rational(0));
}
virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; }
};
}