mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

move arithmetical mbp functionality to model_based_opt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-26 16:12:14 -07:00
parent 7fc294d329
commit b66d457b19
6 changed files with 76 additions and 106 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,8 +35,7 @@ std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
namespace opt { namespace opt {
model_based_opt::model_based_opt() model_based_opt::model_based_opt() {
{
m_rows.push_back(row()); m_rows.push_back(row());
} }
@ -289,7 +288,6 @@ namespace opt {
m_retired_rows.push_back(row_id); m_retired_rows.push_back(row_id);
} }
rational model_based_opt::get_row_value(row const& r) const { rational model_based_opt::get_row_value(row const& r) const {
vector<var> const& vars = r.m_vars; vector<var> const& vars = r.m_vars;
rational val = r.m_coeff; rational val = r.m_coeff;
@ -462,7 +460,6 @@ namespace opt {
} }
} }
rational model_based_opt::n_sign(rational const& b) const { rational model_based_opt::n_sign(rational const& b) const {
return rational(b.is_pos()?-1:1); return rational(b.is_pos()?-1:1);
} }
@ -937,16 +934,6 @@ namespace opt {
// 3x + t = 0 & 7 | (c*x + s) & ax <= u // 3x + t = 0 & 7 | (c*x + s) & ax <= u
// 3 | -t & 21 | (-ct + 3s) & a-t <= 3u // 3 | -t & 21 | (-ct + 3s) & a-t <= 3u
#if 0
void solve_for_int(unsigned row_id1, unsigned x) {
for (unsigned i = 0; i < num_divs(); ++i) {
add_lit(model, lits, mk_divides(c*div_divisor(i),
mk_sub(mk_mul(c, div_term(i)), mk_mul(div_coeff(i), t))));
}
}
#endif
void model_based_opt::solve_for(unsigned row_id1, unsigned x) { void model_based_opt::solve_for(unsigned row_id1, unsigned x) {
rational a = get_coefficient(row_id1, x), b; rational a = get_coefficient(row_id1, x), b;
SASSERT(!a.is_zero()); SASSERT(!a.is_zero());

7
src/model/model_evaluator.cpp
View file

@ -522,5 +522,12 @@ void model_evaluator::operator()(expr * t, expr_ref & result) {
m_imp->operator()(t, result); m_imp->operator()(t, result);
} }
expr_ref model_evaluator::operator()(expr * t) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
expr_ref result(m());
m_imp->operator()(t, result);
return result;
}

2
src/model/model_evaluator.h
View file

@ -41,6 +41,8 @@ public:
void operator()(expr * t, expr_ref & r); void operator()(expr * t, expr_ref & r);
expr_ref operator()(expr* t);
void cleanup(params_ref const & p = params_ref()); void cleanup(params_ref const & p = params_ref());
void reset(params_ref const & p = params_ref()); void reset(params_ref const & p = params_ref());

133
src/qe/qe_arith.cpp
View file

@ -33,32 +33,10 @@ Revision History:
namespace qe { namespace qe {
bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) {
expr* t1, *t2;
if (a.is_mod(e2, t1, t2) &&
a.is_numeral(e1, k) &&
k.is_zero() &&
a.is_numeral(t2, k)) {
p = t1;
return true;
}
return false;
}
bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t) {
expr* e1, *e2;
if (!a.get_manager().is_eq(e, e1, e2)) {
return false;
}
return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
}
struct arith_project_plugin::imp { struct arith_project_plugin::imp {
ast_manager& m; ast_manager& m;
arith_util a; arith_util a;
th_rewriter m_rw;
expr_ref_vector m_trail;
void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) { void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";); TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
@ -108,9 +86,10 @@ namespace qe {
ty = opt::t_eq; ty = opt::t_eq;
} }
else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) { else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) {
expr_ref val1(m), val2(m);
rational r1, r2; rational r1, r2;
eval(e1, val1); eval(e2, val2); expr_ref val1 = eval(e1);
expr_ref val2 = eval(e2);
VERIFY(a.is_numeral(val1, r1)); VERIFY(a.is_numeral(val1, r1));
VERIFY(a.is_numeral(val2, r2)); VERIFY(a.is_numeral(val2, r2));
SASSERT(r1 != r2); SASSERT(r1 != r2);
@ -127,7 +106,7 @@ namespace qe {
app* alit = to_app(lit); app* alit = to_app(lit);
vector<std::pair<expr*,rational> > nums; vector<std::pair<expr*,rational> > nums;
for (unsigned i = 0; i < alit->get_num_args(); ++i) { for (unsigned i = 0; i < alit->get_num_args(); ++i) {
eval(alit->get_arg(i), val); val = eval(alit->get_arg(i));
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
nums.push_back(std::make_pair(alit->get_arg(i), r)); nums.push_back(std::make_pair(alit->get_arg(i), r));
} }
@ -148,9 +127,8 @@ namespace qe {
bool found_eq = false; bool found_eq = false;
for (unsigned i = 0; !found_eq && i < to_app(lit)->get_num_args(); ++i) { for (unsigned i = 0; !found_eq && i < to_app(lit)->get_num_args(); ++i) {
expr* arg1 = to_app(lit)->get_arg(i), *arg2 = 0; expr* arg1 = to_app(lit)->get_arg(i), *arg2 = 0;
expr_ref val(m);
rational r; rational r;
eval(arg1, val); expr_ref val = eval(arg1);
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
if (values.find(r, arg2)) { if (values.find(r, arg2)) {
ty = opt::t_eq; ty = opt::t_eq;
@ -182,10 +160,10 @@ namespace qe {
expr* t1, *t2, *t3; expr* t1, *t2, *t3;
rational mul1; rational mul1;
expr_ref val(m); expr_ref val(m);
if (a.is_mul(t, t1, t2) && is_numeral(eval, t1, mul1)) { if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1)) {
linearize(mbo, eval, mul* mul1, t2, c, fmls, ts, tids); linearize(mbo, eval, mul* mul1, t2, c, fmls, ts, tids);
} }
else if (a.is_mul(t, t1, t2) && is_numeral(eval, t2, mul1)) { else if (a.is_mul(t, t1, t2) && is_numeral(t2, mul1)) {
linearize(mbo, eval, mul* mul1, t1, c, fmls, ts, tids); linearize(mbo, eval, mul* mul1, t1, c, fmls, ts, tids);
} }
else if (a.is_add(t)) { else if (a.is_add(t)) {
@ -205,7 +183,7 @@ namespace qe {
c += mul*mul1; c += mul*mul1;
} }
else if (m.is_ite(t, t1, t2, t3)) { else if (m.is_ite(t, t1, t2, t3)) {
eval(t1, val); val = eval(t1);
SASSERT(m.is_true(val) || m.is_false(val)); SASSERT(m.is_true(val) || m.is_false(val));
TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
if (m.is_true(val)) { if (m.is_true(val)) {
@ -218,9 +196,9 @@ namespace qe {
linearize(mbo, eval, mul, t3, c, fmls, ts, tids); linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
} }
} }
else if (a.is_mod(t, t1, t2) && is_numeral(eval, t2, mul1)) { else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1)) {
rational r; rational r;
eval(t, val); val = eval(t);
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
c += mul*r; c += mul*r;
// t1 mod mul1 == r // t1 mod mul1 == r
@ -236,45 +214,39 @@ namespace qe {
} }
} }
bool is_numeral(model_evaluator& eval, expr* t, rational& r) { bool is_numeral(expr* t, rational& r) {
expr* t1, *t2, *t3; expr* t1, *t2;
rational r1, r2; rational r1, r2;
expr_ref val(m); if (a.is_numeral(t, r)) {
if (a.is_numeral(t, r)) return true; // no-op
}
if (a.is_uminus(t, t1) && is_numeral(eval, t1, r)) { else if (a.is_uminus(t, t1) && is_numeral(t1, r)) {
r.neg(); r.neg();
return true;
} }
else if (a.is_mul(t, t1, t2) && is_numeral(eval, t1, r1) && is_numeral(eval, t2, r2)) { else if (a.is_mul(t)) {
r = r1*r2;
return true;
}
else if (a.is_add(t)) {
app* ap = to_app(t); app* ap = to_app(t);
r = rational(1); r = rational(1);
for (unsigned i = 0; i < ap->get_num_args(); ++i) { for (unsigned i = 0; i < ap->get_num_args(); ++i) {
if (!is_numeral(eval, ap->get_arg(i), r1)) return false; if (!is_numeral(ap->get_arg(i), r1)) return false;
r *= r1; r *= r1;
} }
return true;
} }
else if (m.is_ite(t, t1, t2, t3)) { else if (a.is_add(t)) {
eval(t1, val); app* ap = to_app(t);
if (m.is_true(val)) { r = rational(0);
return is_numeral(eval, t1, r); for (unsigned i = 0; i < ap->get_num_args(); ++i) {
if (!is_numeral(ap->get_arg(i), r1)) return false;
r += r1;
}
}
else if (a.is_sub(t, t1, t2) && is_numeral(t1, r1) && is_numeral(t2, r2)) {
r = r1 - r2;
} }
else { else {
return is_numeral(eval, t2, r);
}
}
else if (a.is_sub(t, t1, t2) && is_numeral(eval, t1, r1) && is_numeral(eval, t2, r2)) {
r = r1 - r2;
return true;
}
return false; return false;
} }
return true;
}
struct compare_second { struct compare_second {
bool operator()(std::pair<expr*, rational> const& a, bool operator()(std::pair<expr*, rational> const& a,
@ -292,14 +264,9 @@ namespace qe {
} }
imp(ast_manager& m): imp(ast_manager& m):
m(m), a(m), m_rw(m), m_trail(m) { m(m), a(m) {}
params_ref params;
params.set_bool("gcd_rouding", true);
m_rw.updt_params(params);
}
~imp() { ~imp() {}
}
bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return false; return false;
@ -330,7 +297,6 @@ namespace qe {
opt::model_based_opt mbo; opt::model_based_opt mbo;
obj_map<expr, unsigned> tids; obj_map<expr, unsigned> tids;
m_trail.reset();
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i].get(); expr* fml = fmls[i].get();
@ -359,9 +325,8 @@ namespace qe {
app* v = vars[i].get(); app* v = vars[i].get();
var_mark.mark(v); var_mark.mark(v);
if (is_arith(v) && !tids.contains(v)) { if (is_arith(v) && !tids.contains(v)) {
expr_ref val(m);
rational r; rational r;
eval(v, val); expr_ref val = eval(v);
a.is_numeral(val, r); a.is_numeral(val, r);
TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
tids.insert(v, mbo.add_var(r, a.is_int(v))); tids.insert(v, mbo.add_var(r, a.is_int(v)));
@ -426,7 +391,7 @@ namespace qe {
default: UNREACHABLE(); default: UNREACHABLE();
} }
fmls.push_back(t); fmls.push_back(t);
VERIFY(model.eval(t, val)); val = eval(t);
CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";); CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";);
continue; continue;
} }
@ -450,8 +415,7 @@ namespace qe {
case opt::t_le: t = a.mk_le(t, s); break; case opt::t_le: t = a.mk_le(t, s); break;
case opt::t_eq: t = a.mk_eq(t, s); break; case opt::t_eq: t = a.mk_eq(t, s); break;
case opt::t_mod: { case opt::t_mod: {
rational sval; if (!r.m_coeff.is_zero()) {
if (!a.is_numeral(s, sval) || !sval.is_zero()) {
t = a.mk_sub(t, s); t = a.mk_sub(t, s);
} }
t = a.mk_eq(a.mk_mod(t, a.mk_numeral(r.m_mod, true)), a.mk_int(0)); t = a.mk_eq(a.mk_mod(t, a.mk_numeral(r.m_mod, true)), a.mk_int(0));
@ -460,15 +424,13 @@ namespace qe {
} }
fmls.push_back(t); fmls.push_back(t);
VERIFY(model.eval(t, val)); val = eval(t);
CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";); CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";);
} }
} }
opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
validate_model(mdl, fmls0);
m_trail.reset();
SASSERT(a.is_real(t)); SASSERT(a.is_real(t));
expr_ref_vector fmls(fmls0); expr_ref_vector fmls(fmls0);
opt::model_based_opt mbo; opt::model_based_opt mbo;
@ -483,6 +445,8 @@ namespace qe {
extract_coefficients(mbo, eval, ts, tids, coeffs); extract_coefficients(mbo, eval, ts, tids, coeffs);
mbo.set_objective(coeffs, c); mbo.set_objective(coeffs, c);
SASSERT(validate_model(eval, fmls0));
// extract linear constraints // extract linear constraints
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
@ -509,8 +473,7 @@ namespace qe {
} }
} }
expr_ref val(a.mk_numeral(value.get_rational(), false), m); expr_ref val(a.mk_numeral(value.get_rational(), false), m);
expr_ref tval(m); expr_ref tval = eval(t);
eval(t, tval);
// update the predicate 'bound' which forces larger values when 'strict' is true. // update the predicate 'bound' which forces larger values when 'strict' is true.
// strict: bound := valuue < t // strict: bound := valuue < t
@ -527,15 +490,14 @@ namespace qe {
ge = a.mk_ge(t, val); ge = a.mk_ge(t, val);
gt = a.mk_gt(t, val); gt = a.mk_gt(t, val);
} }
validate_model(mdl, fmls0); SASSERT(validate_model(eval, fmls0));
return value; return value;
} }
bool validate_model(model& mdl, expr_ref_vector const& fmls) { bool validate_model(model_evaluator& eval, expr_ref_vector const& fmls) {
bool valid = true; bool valid = true;
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
expr_ref val(m); expr_ref val = eval(fmls[i]);
VERIFY(mdl.eval(fmls[i], val));
if (!m.is_true(val)) { if (!m.is_true(val)) {
valid = false; valid = false;
TRACE("qe", tout << mk_pp(fmls[i], m) << " := " << val << "\n";); TRACE("qe", tout << mk_pp(fmls[i], m) << " := " << val << "\n";);
@ -553,17 +515,10 @@ namespace qe {
expr* v = it->m_key; expr* v = it->m_key;
if (!tids.find(v, id)) { if (!tids.find(v, id)) {
rational r; rational r;
expr_ref val(m); expr_ref val = eval(v);
eval(v, val); a.is_numeral(val, r);
if (a.is_numeral(val, r)) {
id = mbo.add_var(r, a.is_int(v)); id = mbo.add_var(r, a.is_int(v));
}
else {
TRACE("qe", tout << "extraction of coefficients cancelled\n";);
return;
}
tids.insert(v, id); tids.insert(v, id);
m_trail.push_back(v);
} }
CTRACE("qe", it->m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";); CTRACE("qe", it->m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";);
if (!it->m_value.is_zero()) { if (!it->m_value.is_zero()) {

2
src/qe/qe_arith.h
View file

@ -37,8 +37,6 @@ namespace qe {
bool arith_project(model& model, app* var, expr_ref_vector& lits); bool arith_project(model& model, app* var, expr_ref_vector& lits);
// match e := t mod k = 0.
bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t);
}; };

21
src/qe/qe_arith_plugin.cpp
View file

@ -36,6 +36,27 @@ Revision History:
namespace qe { namespace qe {
static bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) {
expr* t1, *t2;
if (a.is_mod(e2, t1, t2) &&
a.is_numeral(e1, k) &&
k.is_zero() &&
a.is_numeral(t2, k)) {
p = t1;
return true;
}
return false;
}
static bool is_divides(arith_util& a, expr* e, rational& k, expr_ref& t) {
expr* e1, *e2;
if (!a.get_manager().is_eq(e, e1, e2)) {
return false;
}
return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
}
class bound { class bound {
rational m_coeff; rational m_coeff;
expr_ref m_term; expr_ref m_term;