mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

mbo

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-20 13:45:50 -07:00
parent d12efb6097
commit 339cd6e537
8 changed files with 317 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

130
src/math/simplex/model_based_opt.cpp
View file

@ -34,8 +34,7 @@ std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
namespace opt {
model_based_opt::model_based_opt():
m_objective_id(0)
model_based_opt::model_based_opt()
{
m_rows.push_back(row());
}
@ -448,5 +447,132 @@ namespace opt {
set_row(m_objective_id, coeffs, c, t_le);
}
void model_based_opt::get_live_rows(vector<row>& rows) {
for (unsigned i = 0; i < m_rows.size(); ++i) {
if (m_rows[i].m_alive) {
rows.push_back(m_rows[i]);
}
}
}
//
// pick glb and lub representative.
// The representative is picked such that it
// represents the fewest inequalities.
// The constraints that enforce a glb or lub are not forced.
// The constraints that separate the glb from ub or the lub from lb
// are not forced.
// In other words, suppose there are
// . N inequalities of the form t <= x
// . M inequalities of the form s >= x
// . t0 is glb among N under valuation.
// . s0 is lub among M under valuation.
// If N < M
// create the inequalities:
// t <= t0 for each t other than t0 (N-1 inequalities).
// t0 <= s for each s (M inequalities).
// If N >= M the construction is symmetric.
//
void model_based_opt::project(unsigned x) {
unsigned_vector& lub_rows = m_lub;
unsigned_vector& glb_rows = m_glb;
unsigned lub_index = UINT_MAX, glb_index = UINT_MAX;
bool lub_strict = false, glb_strict = false;
rational lub_val, glb_val;
rational const& x_val = m_var2value[x];
unsigned_vector const& row_ids = m_var2row_ids[x];
uint_set visited;
lub_rows.reset();
glb_rows.reset();
// select the lub and glb.
for (unsigned i = 0; i < row_ids.size(); ++i) {
unsigned row_id = row_ids[i];
if (visited.contains(row_id)) {
continue;
}
visited.insert(row_id);
row& r = m_rows[row_id];
if (!r.m_alive) {
continue;
}
rational a = get_coefficient(row_id, x);
if (a.is_zero()) {
continue;
}
if (r.m_type == t_eq) {
solve_for(row_id, x);
return;
}
if (a.is_pos()) {
rational lub_value = x_val - (r.m_value/a);
if (lub_rows.empty() ||
lub_value < lub_val ||
(lub_value == lub_val && r.m_type == t_lt && !lub_strict)) {
lub_val = lub_value;
lub_index = row_id;
lub_strict = r.m_type == t_lt;
}
lub_rows.push_back(row_id);
}
else {
SASSERT(a.is_neg());
rational glb_value = x_val - (r.m_value/a);
if (glb_rows.empty() ||
glb_value > glb_val ||
(glb_value == glb_val && r.m_type == t_lt && !glb_strict)) {
glb_val = glb_value;
glb_index = row_id;
glb_strict = r.m_type == t_lt;
}
glb_rows.push_back(row_id);
}
}
unsigned row_index = (lub_rows.size() <= glb_rows.size())? lub_index : glb_index;
glb_rows.append(lub_rows);
if (row_index == UINT_MAX) {
for (unsigned i = 0; i < glb_rows.size(); ++i) {
unsigned row_id = glb_rows[i];
SASSERT(m_rows[row_id].m_alive);
SASSERT(!get_coefficient(row_id, x).is_zero());
m_rows[row_id].m_alive = false;
}
}
else {
rational coeff = get_coefficient(row_index, x);
for (unsigned i = 0; i < glb_rows.size(); ++i) {
unsigned row_id = glb_rows[i];
if (row_id != row_index) {
resolve(row_index, coeff, row_id, x);
}
}
m_rows[row_index].m_alive = false;
}
}
void model_based_opt::solve_for(unsigned row_id1, unsigned x) {
rational a = get_coefficient(row_id1, x);
row& r1 = m_rows[row_id1];
SASSERT(!a.is_zero());
SASSERT(r1.m_type == t_eq);
SASSERT(r1.m_alive);
unsigned_vector const& row_ids = m_var2row_ids[x];
uint_set visited;
visited.insert(row_id1);
for (unsigned i = 0; i < row_ids.size(); ++i) {
unsigned row_id2 = row_ids[i];
if (!visited.contains(row_id2)) {
visited.insert(row_id2);
resolve(row_id1, a, row_id2, x);
}
}
r1.m_alive = false;
}
void model_based_opt::project(unsigned num_vars, unsigned const* vars) {
for (unsigned i = 0; i < num_vars; ++i) {
project(vars[i]);
}
}
}

21
src/math/simplex/model_based_opt.h
View file

@ -48,7 +48,6 @@ namespace opt {
}
};
};
private:
struct row {
row(): m_type(t_le), m_value(0), m_alive(false) {}
vector<var> m_vars; // variables with coefficients
@ -58,11 +57,14 @@ namespace opt {
bool m_alive; // rows can be marked dead if they have been processed.
};
private:
vector<row> m_rows;
unsigned m_objective_id;
static const unsigned m_objective_id = 0;
vector<unsigned_vector> m_var2row_ids;
vector<rational> m_var2value;
vector<var> m_new_vars;
unsigned_vector m_lub, m_glb;
bool invariant();
bool invariant(unsigned index, row const& r);
@ -81,6 +83,10 @@ namespace opt {
void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);
void project(unsigned var);
void solve_for(unsigned row_id, unsigned x);
public:
model_based_opt();
@ -106,6 +112,17 @@ namespace opt {
//
inf_eps maximize();
//
// Project set of variables from inequalities.
//
void project(unsigned num_vars, unsigned const* vars);
//
// Extract current rows (after projection).
//
void get_live_rows(vector<row>& rows);
void display(std::ostream& out) const;
void display(std::ostream& out, row const& r) const;

6
src/qe/qe_arith.cpp
View file

@ -29,6 +29,7 @@ Revision History:
#include "expr_functors.h"
#include "expr_safe_replace.h"
#include "model_based_opt.h"
#include "model_evaluator.h"
namespace qe {
@ -658,6 +659,9 @@ namespace qe {
bool new_max = true;
rational max_r, r;
expr_ref val(m);
model_evaluator eval(mdl);
eval.set_model_completion(true);
bool is_int = a.is_int(m_var->x());
for (unsigned i = 0; i < num_ineqs(); ++i) {
rational const& ac = m_ineq_coeffs[i];
@ -669,7 +673,7 @@ namespace qe {
// ac < 0: x + t/ac > 0 <=> x > max { - t/ac | ac < 0 } = max { t/|ac| | ac < 0 }
//
if (ac.is_pos() == do_pos) {
VERIFY(mdl.eval(ineq_term(i), val));
eval(ineq_term(i), val);
VERIFY(a.is_numeral(val, r));
r /= abs(ac);
new_max =

92
src/qe/qe_mbp.cpp
View file

@ -28,10 +28,15 @@ Revision History:
#include "th_rewriter.h"
#include "model_v2_pp.h"
#include "expr_functors.h"
#include "for_each_expr.h"
using namespace qe;
struct noop_op_proc {
void operator()(expr*) {}
};
/**
\brief return two terms that are equal in the model.
@ -106,6 +111,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
class mbp::impl {
ast_manager& m;
th_rewriter m_rw;
ptr_vector<project_plugin> m_plugins;
expr_mark m_visited;
@ -130,7 +136,6 @@ class mbp::impl {
is_var.mark(vars[i].get());
}
expr_ref tmp(m), t(m), v(m);
th_rewriter rw(m);
for (unsigned i = 0; i < lits.size(); ++i) {
expr* e = lits[i].get(), *l, *r;
if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
@ -141,7 +146,7 @@ class mbp::impl {
is_rem.mark(v);
for (unsigned j = 0; j < lits.size(); ++j) {
sub(lits[j].get(), tmp);
rw(tmp);
m_rw(tmp);
lits[j] = tmp;
}
}
@ -177,6 +182,29 @@ class mbp::impl {
}
void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) {
ast_manager& m = vars.get_manager();
expr_mark lit_visited;
for_each_expr_proc<noop_op_proc> fe;
for (unsigned i = 0; i < lits.size(); ++i) {
for_each_expr(fe, lit_visited, lits[i].get());
}
unsigned j = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
app* var = vars[i].get();
if (lit_visited.is_marked(var)) {
if (i != j) {
vars[j] = vars[i].get();
}
++j;
}
}
if (vars.size() != j) {
vars.resize(j);
}
}
void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) {
TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
ptr_vector<expr> todo;
@ -210,6 +238,42 @@ class mbp::impl {
}
}
void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
expr_safe_replace sub(m);
expr_ref val(m);
unsigned j = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
app* var = vars[i].get();
if (m.is_bool(var)) {
VERIFY(model.eval(var, val));
sub.insert(var, val);
}
else {
if (j != i) {
vars[j] = vars[i].get();
}
++j;
}
}
if (j != vars.size()) {
vars.resize(j);
j = 0;
for (unsigned i = 0; i < fmls.size(); ++i) {
sub(fmls[i].get(), val);
m_rw(val);
if (!m.is_true(val)) {
if (j != i) {
fmls[j] = fmls[i].get();
}
++j;
}
}
if (j != fmls.size()) {
fmls.resize(j);
}
}
}
public:
@ -333,7 +397,7 @@ public:
m_visited.reset();
}
impl(ast_manager& m):m(m) {
impl(ast_manager& m):m(m), m_rw(m) {
add_plugin(alloc(arith_project_plugin, m));
add_plugin(alloc(datatype_project_plugin, m));
add_plugin(alloc(array_project_plugin, m));
@ -359,14 +423,16 @@ public:
void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) {
expr_ref val(m), tmp(m);
app_ref var(m);
th_rewriter rw(m);
expr_ref_vector unused_fmls(m);
bool progress = true;
TRACE("qe", tout << vars << " " << fmls << "\n";);
while (progress && !vars.empty()) {
preprocess_solve(model, vars, fmls);
preprocess_solve(model, vars, fmls);
filter_variables(model, vars, fmls, unused_fmls);
project_bools(model, vars, fmls);
while (progress && !vars.empty() && !fmls.empty()) {
app_ref_vector new_vars(m);
progress = false;
while (!vars.empty()) {
while (!vars.empty() && !fmls.empty()) {
var = vars.back();
vars.pop_back();
project_plugin* p = get_plugin(var);
@ -377,7 +443,7 @@ public:
new_vars.push_back(var);
}
}
if (!progress && !new_vars.empty() && force_elim) {
if (!progress && !new_vars.empty() && !fmls.empty() && force_elim) {
var = new_vars.back();
new_vars.pop_back();
expr_safe_replace sub(m);
@ -385,7 +451,7 @@ public:
sub.insert(var, val);
for (unsigned i = 0; i < fmls.size(); ++i) {
sub(fmls[i].get(), tmp);
rw(tmp);
m_rw(tmp);
if (m.is_true(tmp)) {
project_plugin::erase(fmls, i);
}
@ -396,9 +462,17 @@ public:
progress = true;
}
vars.append(new_vars);
if (progress) {
preprocess_solve(model, vars, fmls);
}
}
if (fmls.empty()) {
vars.reset();
}
fmls.append(unused_fmls);
TRACE("qe", tout << vars << " " << fmls << "\n";);
}
};
mbp::mbp(ast_manager& m) {

1
src/qe/qe_mbp.h
View file

@ -37,6 +37,7 @@ namespace qe {
virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0;
virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0;
virtual family_id get_family_id() = 0;
virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; };
static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits);

3
src/qe/qsat.cpp
View file

@ -575,6 +575,7 @@ namespace qe {
lbool check_sat() {
while (true) {
++m_stats.m_num_rounds;
IF_VERBOSE(3, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";);
check_cancel();
expr_ref_vector asms(m_asms);
m_pred_abs.get_assumptions(m_model.get(), asms);
@ -1191,7 +1192,7 @@ namespace qe {
lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) {
expr_ref_vector defs(m);
expr_ref fml = negate_core(fmls);
expr_ref fml = mk_and(fmls);
hoist(fml);
m_objective = t;
m_value = opt::inf_eps();

8
src/smt/theory_pb.cpp
View file

@ -1063,7 +1063,7 @@ namespace smt {
}
#endif
else {
IF_VERBOSE(3, display(verbose_stream() << "no propagation ", c, true););
IF_VERBOSE(14, display(verbose_stream() << "no propagation ", c, true););
}
}
@ -1637,7 +1637,7 @@ namespace smt {
// same order as the assignment stack.
// It is not a correctness bug but causes to miss lemmas.
//
IF_VERBOSE(2, display_resolved_lemma(verbose_stream()););
IF_VERBOSE(12, display_resolved_lemma(verbose_stream()););
TRACE("pb", display_resolved_lemma(tout););
return false;
}
@ -1735,12 +1735,12 @@ namespace smt {
// 3x + 3y + z + u >= 4
// ~x /\ ~y => z + u >=
IF_VERBOSE(4, display(verbose_stream() << "lemma1: ", m_lemma););
IF_VERBOSE(14, display(verbose_stream() << "lemma1: ", m_lemma););
hoist_maximal_values();
lbool is_true = m_lemma.normalize(false);
m_lemma.prune(false);
IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma););
IF_VERBOSE(14, display(verbose_stream() << "lemma2: ", m_lemma););
//unsigned l_size = m_ineq_literals.size() + ((is_true==l_false)?0:m_lemma.size());
//if (s_min_l_size >= l_size) {
// verbose_stream() << "(pb.conflict min size: " << l_size << ")\n";

75
src/test/model_based_opt.cpp
View file

@ -216,6 +216,77 @@ static void test4() {
std::cout << "u: " << mbo.get_value(u) << "\n";
}
static void test5() {
opt::model_based_opt mbo;
unsigned x = mbo.add_var(rational(2));
unsigned y = mbo.add_var(rational(3));
unsigned z = mbo.add_var(rational(4));
unsigned u = mbo.add_var(rational(5));
add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
add_ineq(mbo, x, 1, z, -1, 0, opt::t_le);
add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
add_ineq(mbo, z, 1, u, -1, 1, opt::t_le);
unsigned vars[2] = { y, z };
mbo.project(1, vars);
mbo.display(std::cout);
mbo.project(1, vars);
mbo.display(std::cout);
mbo.project(1, vars+1);
mbo.display(std::cout);
vector<opt::model_based_opt::row> rows;
mbo.get_live_rows(rows);
}
static void test6() {
opt::model_based_opt mbo;
unsigned x0 = mbo.add_var(rational(1));
unsigned x = mbo.add_var(rational(2));
unsigned y = mbo.add_var(rational(3));
unsigned z = mbo.add_var(rational(4));
unsigned u = mbo.add_var(rational(5));
unsigned v = mbo.add_var(rational(6));
unsigned w = mbo.add_var(rational(6));
add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le);
add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
add_ineq(mbo, y, 1, z, -1, 1, opt::t_le);
add_ineq(mbo, y, 1, v, -1, 1, opt::t_le);
add_ineq(mbo, y, 1, w, -1, 1, opt::t_le);
mbo.display(std::cout);
mbo.project(1, &y);
mbo.display(std::cout);
}
static void test7() {
opt::model_based_opt mbo;
unsigned x0 = mbo.add_var(rational(2));
unsigned x = mbo.add_var(rational(1));
unsigned y = mbo.add_var(rational(3));
unsigned z = mbo.add_var(rational(4));
unsigned u = mbo.add_var(rational(5));
unsigned v = mbo.add_var(rational(6));
unsigned w = mbo.add_var(rational(6));
add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le);
add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt);
add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
add_ineq(mbo, y, 1, z, -1, 1, opt::t_le);
add_ineq(mbo, y, 1, v, -1, 1, opt::t_le);
add_ineq(mbo, y, 1, w, -1, 1, opt::t_lt);
mbo.display(std::cout);
mbo.project(1, &y);
mbo.display(std::cout);
}
// test with mix of upper and lower bounds
void tst_model_based_opt() {
@ -224,4 +295,8 @@ void tst_model_based_opt() {
test2();
test3();
test4();
test5();
test6();
test7();
}