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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-10-12 14:17:57 -07:00
parent 3554554533 d338fab4f6
commit 6ecd77d91c
2 changed files with 29 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/qe/qe_arith.cpp
View file

@ -105,10 +105,10 @@ namespace qe {
rational r; rational r;
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 (expr* arg : *alit) {
val = eval(alit->get_arg(i)); val = eval(arg);
if (!a.is_numeral(val, r)) return false; if (!a.is_numeral(val, r)) return false;
nums.push_back(std::make_pair(alit->get_arg(i), r)); nums.push_back(std::make_pair(arg, r));
} }
std::sort(nums.begin(), nums.end(), compare_second()); std::sort(nums.begin(), nums.end(), compare_second());
for (unsigned i = 0; i + 1 < nums.size(); ++i) { for (unsigned i = 0; i + 1 < nums.size(); ++i) {
@ -168,8 +168,8 @@ namespace qe {
} }
else if (a.is_add(t)) { else if (a.is_add(t)) {
app* ap = to_app(t); app* ap = to_app(t);
for (unsigned i = 0; i < ap->get_num_args(); ++i) { for (expr* arg : *ap) {
linearize(mbo, eval, mul, ap->get_arg(i), c, fmls, ts, tids); linearize(mbo, eval, mul, arg, c, fmls, ts, tids);
} }
} }
else if (a.is_sub(t, t1, t2)) { else if (a.is_sub(t, t1, t2)) {
@ -226,16 +226,16 @@ namespace qe {
else if (a.is_mul(t)) { else if (a.is_mul(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 (expr * arg : *ap) {
if (!is_numeral(ap->get_arg(i), r1)) return false; if (!is_numeral(arg, r1)) return false;
r *= r1; r *= r1;
} }
} }
else if (a.is_add(t)) { else if (a.is_add(t)) {
app* ap = to_app(t); app* ap = to_app(t);
r = rational(0); r = rational(0);
for (unsigned i = 0; i < ap->get_num_args(); ++i) { for (expr * arg : *ap) {
if (!is_numeral(ap->get_arg(i), r1)) return false; if (!is_numeral(arg, r1)) return false;
r += r1; r += r1;
} }
} }
@ -297,6 +297,7 @@ namespace qe {
opt::model_based_opt mbo; opt::model_based_opt mbo;
obj_map<expr, unsigned> tids; obj_map<expr, unsigned> tids;
expr_ref_vector pinned(m);
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();
@ -308,6 +309,7 @@ namespace qe {
} }
else { else {
TRACE("qe", tout << mk_pp(fml, m) << "\n";); TRACE("qe", tout << mk_pp(fml, m) << "\n";);
pinned.push_back(fml);
} }
} }
fmls.resize(j); fmls.resize(j);
@ -321,8 +323,7 @@ namespace qe {
// return those to fmls. // return those to fmls.
expr_mark var_mark, fmls_mark; expr_mark var_mark, fmls_mark;
for (unsigned i = 0; i < vars.size(); ++i) { for (app * v : vars) {
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)) {
rational r; rational r;
@ -332,17 +333,16 @@ namespace qe {
tids.insert(v, mbo.add_var(r, a.is_int(v))); tids.insert(v, mbo.add_var(r, a.is_int(v)));
} }
} }
for (unsigned i = 0; i < fmls.size(); ++i) { for (expr* fml : fmls) {
fmls_mark.mark(fmls[i].get()); fmls_mark.mark(fml);
} }
obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
ptr_vector<expr> index2expr; ptr_vector<expr> index2expr;
for (; it != end; ++it) { for (auto& kv : tids) {
expr* e = it->m_key; expr* e = kv.m_key;
if (!var_mark.is_marked(e)) { if (!var_mark.is_marked(e)) {
mark_rec(fmls_mark, e); mark_rec(fmls_mark, e);
} }
index2expr.setx(it->m_value, e, 0); index2expr.setx(kv.m_value, e, 0);
} }
j = 0; j = 0;
unsigned_vector real_vars; unsigned_vector real_vars;
@ -360,8 +360,7 @@ namespace qe {
} }
vars.resize(j); vars.resize(j);
TRACE("qe", tout << "remaining vars: " << vars << "\n"; TRACE("qe", tout << "remaining vars: " << vars << "\n";
for (unsigned i = 0; i < real_vars.size(); ++i) { for (unsigned v : real_vars) {
unsigned v = real_vars[i];
tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n"; tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
} }
mbo.display(tout);); mbo.display(tout););
@ -449,8 +448,8 @@ namespace qe {
// extract linear constraints // extract linear constraints
for (unsigned i = 0; i < fmls.size(); ++i) { for (expr * fml : fmls) {
linearize(mbo, eval, fmls[i].get(), fmls, tids); linearize(mbo, eval, fml, fmls, tids);
} }
// find optimal value // find optimal value
@ -459,11 +458,10 @@ namespace qe {
// update model to use new values that satisfy optimality // update model to use new values that satisfy optimality
ptr_vector<expr> vars; ptr_vector<expr> vars;
obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end(); for (auto& kv : tids) {
for (; it != end; ++it) { expr* e = kv.m_key;
expr* e = it->m_key;
if (is_uninterp_const(e)) { if (is_uninterp_const(e)) {
unsigned id = it->m_value; unsigned id = kv.m_value;
func_decl* f = to_app(e)->get_decl(); func_decl* f = to_app(e)->get_decl();
expr_ref val(a.mk_numeral(mbo.get_value(id), false), m); expr_ref val(a.mk_numeral(mbo.get_value(id), false), m);
mdl.register_decl(f, val); mdl.register_decl(f, val);
@ -509,10 +507,9 @@ namespace qe {
void extract_coefficients(opt::model_based_opt& mbo, model_evaluator& eval, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) { void extract_coefficients(opt::model_based_opt& mbo, model_evaluator& eval, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
coeffs.reset(); coeffs.reset();
eval.set_model_completion(true); eval.set_model_completion(true);
obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end(); for (auto& kv : ts) {
for (; it != end; ++it) {
unsigned id; unsigned id;
expr* v = it->m_key; expr* v = kv.m_key;
if (!tids.find(v, id)) { if (!tids.find(v, id)) {
rational r; rational r;
expr_ref val = eval(v); expr_ref val = eval(v);
@ -520,9 +517,9 @@ namespace qe {
id = mbo.add_var(r, a.is_int(v)); id = mbo.add_var(r, a.is_int(v));
tids.insert(v, id); tids.insert(v, id);
} }
CTRACE("qe", it->m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";); CTRACE("qe", kv.m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";);
if (!it->m_value.is_zero()) { if (!kv.m_value.is_zero()) {
coeffs.push_back(var(id, it->m_value)); coeffs.push_back(var(id, kv.m_value));
} }
} }
} }

2
src/test/main.cpp
View file

@ -233,7 +233,7 @@ int main(int argc, char ** argv) {
TST(quant_solve); TST(quant_solve);
TST(rcf); TST(rcf);
TST(polynorm); TST(polynorm);
// TST(qe_arith); TST(qe_arith);
TST(expr_substitution); TST(expr_substitution);
TST(sorting_network); TST(sorting_network);
TST(theory_pb); TST(theory_pb);