mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

working on upper bound optimziation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-03 14:54:42 -08:00
parent e5698119d7
commit c0de1e34ac
17 changed files with 343 additions and 125 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_arith.h
View file

@ -90,6 +90,7 @@ namespace smt {
static const int dead_row_id = -1;
protected:
bool proofs_enabled() const { return get_manager().proofs_enabled(); }
bool coeffs_enabled() const { return proofs_enabled() || m_bound_watch != null_bool_var; }
struct linear_monomial {
numeral m_coeff;
@ -995,11 +996,19 @@ namespace smt {
// Optimization
//
// -----------------------------------
virtual bool maximize(theory_var v);
virtual inf_eps_rational<inf_rational> maximize(theory_var v);
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);
expr* block_upper_bound(theory_var v, inf_numeral const& val);
void enable_record_conflict(expr* bound);
void record_conflict(unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params, parameter* params);
inf_eps_rational<inf_rational> conflict_minimize();
private:
bool_var m_bound_watch;
inf_eps_rational<inf_rational> m_upper_bound;
public:
// -----------------------------------
//
// Pretty Printing

174
src/smt/theory_arith_aux.h
View file

@ -21,6 +21,8 @@ Revision History:
#include"inf_eps_rational.h"
#include"theory_arith.h"
#include"smt_farkas_util.h"
#include"th_rewriter.h"
namespace smt {
@ -977,14 +979,20 @@ namespace smt {
}
template<typename Ext>
bool theory_arith<Ext>::maximize(theory_var v) {
inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v) {
bool r = max_min(v, true);
if (!r && at_upper(v)) {
if (at_upper(v)) {
m_objective_value = get_value(v);
}
return r || at_upper(v);
else if (!r) {
m_objective_value = inf_eps_rational<inf_rational>::infinity();
}
return m_objective_value;
}
/**
\brief: assert val < v
*/
template<typename Ext>
expr* theory_arith<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
ast_manager& m = get_manager();
@ -1000,6 +1008,9 @@ namespace smt {
}
}
/**
\brief assert val <= v
*/
template<typename Ext>
expr* theory_arith<Ext>::block_upper_bound(theory_var v, inf_numeral const& val) {
ast_manager& m = get_manager();
@ -1007,29 +1018,154 @@ namespace smt {
std::ostringstream strm;
strm << val << " <= v" << v;
expr* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
bool_var bv = ctx.mk_bool_var(b);
ctx.set_var_theory(bv, get_id());
// ctx.set_enode_flag(bv, true);
inf_numeral val1 = val;
if (!Ext::is_infinite(val)) {
val1 += Ext::m_real_epsilon;
if (!ctx.b_internalized(b)) {
bool_var bv = ctx.mk_bool_var(b);
ctx.set_var_theory(bv, get_id());
// ctx.set_enode_flag(bv, true);
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);
TRACE("arith", tout << mk_pp(b, m) << "\n";
display_atom(tout, a, false););
}
atom* a = alloc(atom, bv, v, val1, A_LOWER);
m_unassigned_atoms[v]++;
m_var_occs[v].push_back(a);
m_atoms.push_back(a);
insert_bv2a(bv, a);
TRACE("arith", tout << mk_pp(b, m) << "\n";
display_atom(tout, a, false);
display_atoms(tout););
return b;
}
/**
\brief enable watching bound atom.
*/
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
return m_objective_value;
void theory_arith<Ext>::enable_record_conflict(expr* bound) {
m_params.m_arith_bound_prop = BP_NONE;
SASSERT(propagation_mode() == BP_NONE); // bound propagtion rules are not (yet) handled.
if (bound) {
context& ctx = get_context();
m_bound_watch = ctx.get_bool_var(bound);
}
else {
m_bound_watch = null_bool_var;
}
m_upper_bound = -inf_eps_rational<inf_rational>::infinity();
}
/**
\brief
pos < 0
==
r(Ax <= b) + q(v <= val)
==
val' <= q*v & q*v <= q*val
q*v - val' >= 0
=>
(q*v - val' - q*v)/q >= -v
==
val/q <= v
*/
template<typename Ext>
void theory_arith<Ext>::record_conflict(
unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params, parameter* params) {
ast_manager& m = get_manager();
context& ctx = get_context();
if (null_bool_var == m_bound_watch) {
return;
}
unsigned idx = num_lits;
for (unsigned i = 0; i < num_lits; ++i) {
if (m_bound_watch == lits[i].var()) {
//SASSERT(!lits[i].sign());
idx = i;
break;
}
}
if (idx == num_lits) {
return;
}
SASSERT(num_params == 1 + num_lits + num_eqs);
SASSERT(params[0].is_symbol());
SASSERT(params[0].get_symbol() == symbol("farkas")); // for now, just handle this rule.
farkas_util farkas(m);
expr_ref tmp(m), vq(m);
expr* x, *y, *e;
rational q;
for (unsigned i = 0; i < num_lits; ++i) {
parameter const& pa = params[i+1];
SASSERT(pa.is_rational());
if (idx == i) {
q = abs(pa.get_rational());
continue;
}
ctx.literal2expr(~lits[i], tmp);
farkas.add(abs(pa.get_rational()), to_app(tmp));
}
for (unsigned i = 0; i < num_eqs; ++i) {
enode_pair const& p = eqs[i];
x = p.first->get_owner();
y = p.second->get_owner();
tmp = m.mk_not(m.mk_eq(x,y));
parameter const& pa = params[1 + num_lits + i];
SASSERT(pa.is_rational());
farkas.add(abs(pa.get_rational()), to_app(tmp));
}
tmp = farkas.get();
std::cout << tmp << "\n";
atom* a = get_bv2a(m_bound_watch);
SASSERT(a);
expr_ref_vector terms(m);
vector<rational> mults;
bool strict = false;
if (m_util.is_le(tmp, x, y) || m_util.is_ge(tmp, y, x)) {
}
else if (m_util.is_lt(tmp, x, y) || m_util.is_gt(tmp, y, x)) {
strict = true;
}
else if (m.is_eq(tmp, x, y)) {
}
else {
UNREACHABLE();
}
e = var2expr(a->get_var());
q = -q*farkas.get_normalize_factor();
SASSERT(!m_util.is_int(e) || q.is_int()); // TBD: not fully handled.
if (q.is_one()) {
vq = e;
}
else {
vq = m_util.mk_mul(m_util.mk_numeral(q, q.is_int()), e);
}
vq = m_util.mk_add(m_util.mk_sub(x, y), vq);
if (!q.is_one()) {
vq = m_util.mk_div(vq, m_util.mk_numeral(q, q.is_int()));
}
th_rewriter rw(m);
rw(vq, tmp);
IF_VERBOSE(1, verbose_stream() << tmp << "\n";);
VERIFY(m_util.is_numeral(tmp, q));
if (m_upper_bound < q) {
m_upper_bound = q;
if (strict) {
m_upper_bound -= get_epsilon(a->get_var());
}
}
}
/**
\brief find the minimal upper bound on the variable that was last enabled
for conflict recording.
*/
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::conflict_minimize() {
return m_upper_bound;
}
/**
\brief Maximize (Minimize) the given temporary row.
Return true if succeeded.

26
src/smt/theory_arith_core.h
View file

@ -879,7 +879,7 @@ namespace smt {
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
rational _k;
m_util.is_numeral(rhs, _k);
VERIFY(m_util.is_numeral(rhs, _k));
inf_numeral k(_k);
atom * a = alloc(atom, bv, v, k, kind);
mk_bound_axioms(a);
@ -1315,7 +1315,8 @@ namespace smt {
m_assume_eq_head(0),
m_nl_rounds(0),
m_nl_gb_exhausted(false),
m_nl_new_exprs(m) {
m_nl_new_exprs(m),
m_bound_watch(null_bool_var) {
}
template<typename Ext>
@ -1980,7 +1981,7 @@ namespace smt {
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";);
antecedents& ante = get_antecedents();
explain_bound(r, idx, !is_below, delta, ante);
b->push_justification(ante, numeral(1), proofs_enabled());
b->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(),
@ -2123,8 +2124,8 @@ namespace smt {
void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) {
SASSERT(b1->get_var() == b2->get_var());
antecedents& ante = get_antecedents();
b1->push_justification(ante, numeral(1), proofs_enabled());
b2->push_justification(ante, numeral(1), proofs_enabled());
b1->push_justification(ante, numeral(1), coeffs_enabled());
b2->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
TRACE("arith_conflict", tout << "bound conflict\n";);
@ -2383,7 +2384,7 @@ namespace smt {
if (!b->has_justification())
continue;
if (!relax_bounds() || delta.is_zero()) {
b->push_justification(ante, it->m_coeff, proofs_enabled());
b->push_justification(ante, it->m_coeff, coeffs_enabled());
continue;
}
numeral coeff = it->m_coeff;
@ -2445,7 +2446,7 @@ namespace smt {
SASSERT(!is_b_lower || k_2 <= k_1);
SASSERT(is_b_lower || k_2 >= k_1);
if (new_atom == 0) {
b->push_justification(ante, coeff, proofs_enabled());
b->push_justification(ante, coeff, coeffs_enabled());
continue;
}
SASSERT(!is_b_lower || k_2 < k_1);
@ -2459,7 +2460,7 @@ namespace smt {
delta -= coeff*(k_2 - k_1);
}
TRACE("propagate_bounds", tout << "delta (after replace): " << delta << "\n";);
new_atom->push_justification(ante, coeff, proofs_enabled());
new_atom->push_justification(ante, coeff, coeffs_enabled());
SASSERT(delta >= inf_numeral::zero());
}
}
@ -2659,13 +2660,13 @@ namespace smt {
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
tout << " ";
if (proofs_enabled()) {
if (coeffs_enabled()) {
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
}
}
for (unsigned i = 0; i < num_eqs; i++) {
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
if (proofs_enabled()) {
if (coeffs_enabled()) {
tout << "bound: " << bounds.eq_coeffs()[i] << "\n";
}
}
@ -2673,6 +2674,7 @@ namespace smt {
tout << bounds.params(proof_rule)[i] << "\n";
}
tout << "\n";);
record_conflict(num_literals, lits, num_eqs, eqs, bounds.num_params(), bounds.params(proof_rule));
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(get_id(), r, num_literals, lits, num_eqs, eqs,
@ -2689,8 +2691,8 @@ namespace smt {
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead() && is_fixed(it->m_var)) {
lower(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());
upper(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());
lower(it->m_var)->push_justification(antecedents, it->m_coeff, coeffs_enabled());
upper(it->m_var)->push_justification(antecedents, it->m_coeff, coeffs_enabled());
}
}
}

12
src/smt/theory_arith_int.h
View file

@ -525,7 +525,7 @@ namespace smt {
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
}
else {
SASSERT(at_upper(x_j));
@ -541,7 +541,7 @@ namespace smt {
}
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
}
pol.push_back(row_entry(new_a_ij, x_j));
}
@ -566,7 +566,7 @@ namespace smt {
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
}
else {
SASSERT(at_upper(x_j));
@ -579,7 +579,7 @@ namespace smt {
new_a_ij.neg(); // the upper terms are inverted
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
}
TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
pol.push_back(row_entry(new_a_ij, x_j));
@ -772,8 +772,8 @@ namespace smt {
// u += ncoeff * lower_bound(v).get_rational();
u.addmul(ncoeff, lower_bound(v).get_rational());
}
lower(v)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
}
else if (gcds.is_zero()) {
gcds = abs_ncoeff;

3
src/smt/theory_diff_logic.h
View file

@ -311,9 +311,8 @@ namespace smt {
//
// -----------------------------------
virtual bool maximize(theory_var v);
virtual inf_eps_rational<inf_rational> maximize(theory_var v);
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);
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);

15
src/smt/theory_diff_logic_def.h
View file

@ -1001,7 +1001,7 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
}
template<typename Ext>
bool theory_diff_logic<Ext>::maximize(theory_var v) {
inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
objective_term const& objective = m_objectives[v];
IF_VERBOSE(1,
@ -1029,12 +1029,14 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
for (unsigned i = 0; i < potentials.size(); ++i) {
tout << "v" << i << " -> " << potentials[i] << "\n";
});
rational r = m_objective_value.get_rational().to_rational();
rational i = m_objective_value.get_infinitesimal().to_rational();
return inf_eps_rational<inf_rational>(inf_rational(r, i));
}
else {
std::cout << "Unbounded objective" << std::endl;
return inf_eps_rational<inf_rational>::infinity();
}
return is_optimal;
}
template<typename Ext>
@ -1054,13 +1056,6 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
return result;
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_diff_logic<Ext>::get_objective_value(theory_var v) {
rational r = m_objective_value.get_rational().to_rational();
rational i = m_objective_value.get_infinitesimal().to_rational();
return inf_eps_rational<inf_rational>(inf_rational(r, i));
}
template<typename Ext>
expr* theory_diff_logic<Ext>::block_lower_bound(theory_var v, inf_rational const& val) {
ast_manager& m = get_manager();

8
src/smt/theory_opt.h
View file

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