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

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-mpf-rem

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-05 12:24:29 +01:00
parent 40b9d0871a 0286cee450
commit 50910e5b3b
3 changed files with 221 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/rewriter/th_rewriter.cpp
View file

@ -212,14 +212,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// auxiliary function for pull_ite_core
expr * mk_eq_value(expr * lhs, expr * value) {
SASSERT(m().is_value(value));
if (m().is_value(lhs)) {
if (m().are_equal(lhs, value)) {
return m().mk_true();
}
else if (m().are_distinct(lhs, value)) {
return m().mk_false();
}
if (m().are_equal(lhs, value)) {
return m().mk_true();
}
else if (m().are_distinct(lhs, value)) {
return m().mk_false();
}
return m().mk_eq(lhs, value);
}

91
src/qe/qe_arith.cpp
View file

@ -51,13 +51,6 @@ namespace qe {
}
return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
}
#if 0
obj_map<expr, unsigned> m_expr2var;
ptr_vector<expr> m_var2expr;
#endif
struct arith_project_plugin::imp {
@ -88,18 +81,23 @@ namespace qe {
}
}
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) {
rational w;
if (ts.find(x, w)) {
ts.insert(x, w + v);
}
else {
TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << "\n";);
ts.insert(x, v);
}
}
void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map<expr, unsigned>& tids) {
//
// extract linear inequalities from literal 'lit' into the model-based optimization manager 'mbo'.
// It uses the current model to choose values for conditionals and it primes mbo with the current
// interpretation of sub-expressions that are treated as variables for mbo.
//
void linearize(opt::model_based_opt& mbo, model& model, expr* lit, obj_map<expr, unsigned>& tids) {
obj_map<expr, rational> ts;
rational c(0), mul(1);
expr_ref t(m);
@ -112,19 +110,19 @@ namespace qe {
SASSERT(!m.is_not(lit));
if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
if (is_not) mul.neg();
linearize(model, mul, e1, c, ts);
linearize(model, -mul, e2, c, ts);
linearize(mbo, model, mul, e1, c, ts, tids);
linearize(mbo, model, -mul, e2, c, ts, tids);
ty = is_not ? opt::t_lt : opt::t_le;
}
else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
if (is_not) mul.neg();
linearize(model, mul, e1, c, ts);
linearize(model, -mul, e2, c, ts);
linearize(mbo, model, mul, e1, c, ts, tids);
linearize(mbo, model, -mul, e2, c, ts, tids);
ty = is_not ? opt::t_le: opt::t_lt;
}
else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
linearize(model, mul, e1, c, ts);
linearize(model, -mul, e2, c, ts);
linearize(mbo, model, mul, e1, c, ts, tids);
linearize(mbo, model, -mul, e2, c, ts, tids);
ty = opt::t_eq;
}
else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
@ -137,55 +135,63 @@ namespace qe {
UNREACHABLE();
}
else {
TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
return;
}
if (ty == opt::t_lt && is_int()) {
#if 0
TBD for integers
if (ty == opt::t_lt && false) {
c += rational(1);
ty = opt::t_le;
}
#endif
vars coeffs;
extract_coefficients(ts, tids, coeffs);
extract_coefficients(mbo, model, ts, tids, coeffs);
mbo.add_constraint(coeffs, c, ty);
}
void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map<expr, rational>& ts) {
//
// convert linear arithmetic term into an inequality for mbo.
//
void linearize(opt::model_based_opt& mbo, model& model, rational const& mul, expr* t, rational& c,
obj_map<expr, rational>& ts, obj_map<expr, unsigned>& tids) {
expr* t1, *t2, *t3;
rational mul1;
expr_ref val(m);
if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) {
linearize(model, mul* mul1, t2, c, ts);
linearize(mbo, model, mul* mul1, t2, c, ts, tids);
}
else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) {
linearize(model, mul* mul1, t1, c, ts);
linearize(mbo, model, mul* mul1, t1, c, ts, tids);
}
else if (a.is_add(t)) {
app* ap = to_app(t);
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
linearize(model, mul, ap->get_arg(i), c, ts);
linearize(mbo, model, mul, ap->get_arg(i), c, ts, tids);
}
}
else if (a.is_sub(t, t1, t2)) {
linearize(model, mul, t1, c, ts);
linearize(model, -mul, t2, c, ts);
linearize(mbo, model, mul, t1, c, ts, tids);
linearize(mbo, model, -mul, t2, c, ts, tids);
}
else if (a.is_uminus(t, t1)) {
linearize(model, -mul, t1, c, ts);
linearize(mbo, model, -mul, t1, c, ts, tids);
}
else if (a.is_numeral(t, mul1)) {
c += mul*mul1;
}
else if (extract_mod(model, t, val)) {
insert_mul(val, mul, ts);
}
else if (m.is_ite(t, t1, t2, t3)) {
VERIFY(model.eval(t1, val));
SASSERT(m.is_true(val) || m.is_false(val));
TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
if (m.is_true(val)) {
linearize(model, mul, t2, c, ts);
linearize(mbo, model, mul, t2, c, ts, tids);
linearize(mbo, model, t1, tids);
}
else {
linearize(model, mul, t3, c, ts);
expr_ref not_t1(mk_not(m, t1), m);
linearize(mbo, model, mul, t3, c, ts, tids);
linearize(mbo, model, not_t1, tids);
}
}
else {
@ -193,6 +199,9 @@ namespace qe {
}
}
//
// extract linear terms from t into c and ts.
//
void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
expr* t1, *t2, *t3;
rational mul1;
@ -245,7 +254,9 @@ namespace qe {
}
}
//
// extract linear inequalities from literal lit.
//
bool is_linear(model& model, expr* lit, bool& found_eq) {
rational c(0), mul(1);
expr_ref t(m);
@ -977,13 +988,13 @@ namespace qe {
// extract objective function.
vars coeffs;
rational c(0), mul(1);
linearize(mdl, mul, t, c, ts);
extract_coefficients(ts, tids, coeffs);
linearize(mbo, mdl, mul, t, c, ts, tids);
extract_coefficients(mbo, mdl, ts, tids, coeffs);
mbo.set_objective(coeffs, c);
// extract linear constraints
for (unsigned i = 0; i < fmls.size(); ++i) {
linearize(mdl, mbo, fmls[i], tids);
linearize(mbo, mdl, fmls[i], tids);
}
// find optimal value
@ -1021,13 +1032,21 @@ namespace qe {
return value;
}
void extract_coefficients(obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
coeffs.reset();
obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
for (; it != end; ++it) {
unsigned id;
if (!tids.find(it->m_key, id)) {
id = tids.size();
rational r;
expr_ref val(m);
if (model.eval(it->m_key, val) && a.is_numeral(val, r)) {
id = mbo.add_var(r);
}
else {
TRACE("qe", tout << "extraction of coefficients cancelled\n";);
return;
}
tids.insert(it->m_key, id);
}
coeffs.push_back(var(id, it->m_value));

164
src/test/qe_arith.cpp
View file

@ -280,12 +280,170 @@ static void test2(char const *ex) {
ctx.assert_expr(pr1);
ctx.assert_expr(npr2);
VERIFY(l_false == ctx.check());
ctx.pop(1);
ctx.pop(1);
}
typedef opt::model_based_opt::var var_t;
static void mk_var(unsigned x, app_ref& v) {
ast_manager& m = v.get_manager();
arith_util a(m);
std::ostringstream strm;
strm << "v" << x;
v = m.mk_const(symbol(strm.str().c_str()), a.mk_real());
}
static void mk_term(vector<var_t> const& vars, rational const& coeff, app_ref& term) {
ast_manager& m = term.get_manager();
expr_ref_vector ts(m);
arith_util a(m);
for (unsigned i = 0; i < vars.size(); ++i) {
app_ref var(m);
mk_var(vars[i].m_id, var);
rational coeff = vars[i].m_coeff;
ts.push_back(a.mk_mul(a.mk_numeral(coeff, false), var));
}
ts.push_back(a.mk_numeral(coeff, a.mk_real()));
term = a.mk_add(ts.size(), ts.c_ptr());
}
static void add_random_ineq(
expr_ref_vector& fmls,
opt::model_based_opt& mbo,
random_gen& r,
svector<int> const& values,
unsigned max_vars,
unsigned max_coeff)
{
ast_manager& m = fmls.get_manager();
arith_util a(m);
unsigned num_vars = values.size();
uint_set used_vars;
vector<var_t> vars;
int value = 0;
for (unsigned i = 0; i < max_vars; ++i) {
unsigned x = r(num_vars);
if (used_vars.contains(x)) {
continue;
}
used_vars.insert(x);
int coeff = r(max_coeff + 1);
if (coeff == 0) {
continue;
}
unsigned sign = r(2);
coeff = sign == 0 ? coeff : -coeff;
vars.push_back(var_t(x, rational(coeff)));
value += coeff*values[x];
}
unsigned abs_value = value < 0 ? - value : value;
// value + k <= 0
// k <= - value
// range for k is 2*|value|
// k <= - value - range
opt::ineq_type rel = opt::t_le;
int coeff = 0;
if (r(4) == 0) {
rel = opt::t_eq;
coeff = -value;
}
else {
if (abs_value > 0) {
coeff = -value - r(2*abs_value);
}
else {
coeff = 0;
}
if (coeff != -value && r(3) == 0) {
rel = opt::t_lt;
}
}
expr_ref fml(m);
app_ref t1(m);
app_ref t2(a.mk_numeral(rational(0), a.mk_real()), m);
mk_term(vars, rational(coeff), t1);
switch (rel) {
case opt::t_eq:
fml = m.mk_eq(t1, t2);
break;
case opt::t_lt:
fml = a.mk_lt(t1, t2);
break;
case opt::t_le:
fml = a.mk_le(t1, t2);
break;
}
fmls.push_back(fml);
mbo.add_constraint(vars, rational(coeff), rel);
}
static void test_maximize(opt::model_based_opt& mbo, ast_manager& m, unsigned num_vars, expr_ref_vector const& fmls, app* t) {
qe::arith_project_plugin plugin(m);
model mdl(m);
expr_ref bound(m);
arith_util a(m);
for (unsigned i = 0; i < num_vars; ++i) {
app_ref var(m);
mk_var(i, var);
rational val = mbo.get_value(i);
mdl.register_decl(var->get_decl(), a.mk_numeral(val, false));
}
opt::inf_eps value1 = plugin.maximize(fmls, mdl, t, bound);
opt::inf_eps value2 = mbo.maximize();
std::cout << "optimal: " << value1 << " " << value2 << "\n";
mbo.display(std::cout);
}
static void check_random_ineqs(random_gen& r, ast_manager& m, unsigned num_vars, unsigned max_value, unsigned num_ineqs, unsigned max_vars, unsigned max_coeff) {
opt::model_based_opt mbo;
expr_ref_vector fmls(m);
svector<int> values;
for (unsigned i = 0; i < num_vars; ++i) {
values.push_back(r(max_value + 1));
mbo.add_var(rational(values.back()));
}
for (unsigned i = 0; i < num_ineqs; ++i) {
add_random_ineq(fmls, mbo, r, values, max_vars, max_coeff);
}
vector<var_t> vars;
vars.reset();
vars.push_back(var_t(0, rational(2)));
vars.push_back(var_t(1, rational(-2)));
mbo.set_objective(vars, rational(0));
mbo.display(std::cout);
app_ref t(m);
mk_term(vars, rational(0), t);
test_maximize(mbo, m, num_vars, fmls, t);
for (unsigned i = 0; i < values.size(); ++i) {
std::cout << i << ": " << values[i] << " -> " << mbo.get_value(i) << "\n";
}
}
static void check_random_ineqs() {
random_gen r(1);
ast_manager m;
reg_decl_plugins(m);
for (unsigned i = 0; i < 100; ++i) {
check_random_ineqs(r, m, 4, 5, 5, 3, 6);
}
}
void tst_qe_arith() {
check_random_ineqs();
return;
// enable_trace("qe");
testI(example8);
testR(example7);