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

fixes for qe_arith

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-12 13:27:31 -07:00
parent 4af4466821
commit 196aed785e
2 changed files with 51 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

134
src/qe/qe_arith.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "arith_decl_plugin.h"
#include "ast_pp.h"
#include "th_rewriter.h"
#include "expr_functors.h"
namespace qe {
@ -33,61 +34,39 @@ namespace qe {
expr_ref_vector m_ineq_terms;
vector<rational> m_ineq_coeffs;
svector<bool> m_ineq_strict;
scoped_ptr<contains_app> m_var;
struct cant_project {};
// TBD: replace by "contains_x" class.
bool contains(app* var, expr* t) const {
ast_mark mark;
ptr_vector<expr> todo;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
todo.pop_back();
if (mark.is_marked(t)) {
continue;
}
mark.mark(t, true);
if (var == t) {
return true;
}
SASSERT(is_app(t));
app* ap = to_app(t);
todo.append(ap->get_num_args(), ap->get_args());
}
return false;
}
void is_linear(app* var, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
void is_linear(rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
expr* t1, *t2;
rational mul1;
if (t == var) {
if (t == m_var->x()) {
c += mul;
}
else if (a.is_mul(t, t1, t2) && a.is_numeral(t1, mul1)) {
is_linear(var, mul* mul1, t2, c, ts);
is_linear(mul* mul1, t2, c, ts);
}
else if (a.is_mul(t, t1, t2) && a.is_numeral(t2, mul1)) {
is_linear(var, mul* mul1, t1, c, ts);
is_linear(mul* mul1, t1, c, ts);
}
else if (a.is_add(t)) {
app* ap = to_app(t);
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
is_linear(var, mul, ap->get_arg(i), c, ts);
is_linear(mul, ap->get_arg(i), c, ts);
}
}
else if (a.is_sub(t, t1, t2)) {
is_linear(var, mul, t1, c, ts);
is_linear(var, -mul, t2, c, ts);
is_linear(mul, t1, c, ts);
is_linear(-mul, t2, c, ts);
}
else if (a.is_uminus(t, t1)) {
is_linear(var, -mul, t1, c, ts);
is_linear(-mul, t1, c, ts);
}
else if (a.is_numeral(t, mul1)) {
ts.push_back(a.mk_numeral(mul*mul1, m.get_sort(t)));
}
else if (contains(var, t)) {
else if ((*m_var)(t)) {
IF_VERBOSE(1, verbose_stream() << mk_pp(t, m) << "\n";);
throw cant_project();
}
@ -99,8 +78,8 @@ namespace qe {
}
}
bool is_linear(app* var, expr* lit, rational& c, expr_ref& t, bool& is_strict) {
if (!contains(var, lit)) {
bool is_linear(expr* lit, rational& c, expr_ref& t, bool& is_strict) {
if (!(*m_var)(lit)) {
return false;
}
expr* e1, *e2;
@ -114,20 +93,20 @@ namespace qe {
}
SASSERT(!m.is_not(lit));
if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
is_linear(var, mul, e1, c, ts);
is_linear(var, -mul, e2, c, ts);
is_linear( mul, e1, c, ts);
is_linear(-mul, e2, c, ts);
s = m.get_sort(e1);
is_strict = is_not;
}
else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
is_linear(var, mul, e1, c, ts);
is_linear(var, -mul, e2, c, ts);
is_linear( mul, e1, c, ts);
is_linear(-mul, e2, c, ts);
s = m.get_sort(e1);
is_strict = !is_not;
}
else if (m.is_eq(lit, e1, e2) && !is_not) {
is_linear(var, mul, e1, c, ts);
is_linear(var, -mul, e2, c, ts);
is_linear( mul, e1, c, ts);
is_linear(-mul, e2, c, ts);
s = m.get_sort(e1);
is_strict = false;
}
@ -143,14 +122,15 @@ namespace qe {
return true;
}
void project(model& model, app* var, expr_ref_vector& lits) {
unsigned num_pos = 0, num_neg = 0;
void project(model& model, expr_ref_vector& lits) {
unsigned num_pos = 0;
unsigned num_neg = 0;
expr_ref_vector new_lits(m);
for (unsigned i = 0; i < lits.size(); ++i) {
rational c(0);
expr_ref t(m);
bool is_strict;
if (is_linear(var, lits[i].get(), c, t, is_strict)) {
if (is_linear(lits[i].get(), c, t, is_strict)) {
m_ineq_coeffs.push_back(c);
m_ineq_terms.push_back(t);
m_ineq_strict.push_back(is_strict);
@ -158,7 +138,7 @@ namespace qe {
++num_pos;
}
else {
--num_neg;
++num_neg;
}
}
else {
@ -170,69 +150,39 @@ namespace qe {
if (num_pos == 0 || num_neg == 0) {
return;
}
if (num_pos < num_neg) {
unsigned max_t = find_max(model);
for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
if (i != max_t) {
if (m_ineq_coeffs[i].is_pos()) {
lits.push_back(mk_le(i, max_t));
}
else {
lits.push_back(mk_lt(i, max_t));
}
bool use_pos = num_pos < num_neg;
unsigned max_t = find_max(model, use_pos);
for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
if (i != max_t) {
if (m_ineq_coeffs[i].is_pos() == use_pos) {
lits.push_back(mk_le(i, max_t));
}
}
}
else {
unsigned min_t = find_min(model);
for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
if (i != min_t) {
if (m_ineq_coeffs[i].is_neg()) {
lits.push_back(mk_le(min_t, i));
}
else {
lits.push_back(mk_lt(min_t, i));
}
else {
lits.push_back(mk_lt(i, max_t));
}
}
}
}
unsigned find_max(model& mdl) {
return find_min_max(mdl, true);
}
unsigned find_min(model& mdl) {
return find_min_max(mdl, false);
}
unsigned find_min_max(model& mdl, bool do_max) {
unsigned find_max(model& mdl, bool do_pos) {
unsigned result;
bool found = false;
rational found_val(0), r;
expr_ref val(m);
for (unsigned i = 0; i < m_ineq_terms.size(); ++i) {
rational const& ac = m_ineq_coeffs[i];
if (ac.is_pos() && do_max) {
if (ac.is_pos() == do_pos) {
VERIFY(mdl.eval(m_ineq_terms[i].get(), val));
VERIFY(a.is_numeral(val, r));
r /= ac;
r /= abs(ac);
IF_VERBOSE(1, verbose_stream() << "max: " << mk_pp(m_ineq_terms[i].get(), m) << " " << r << " " << (!found || r > found_val) << "\n";);
if (!found || r > found_val) {
result = i;
found_val = r;
found = true;
}
}
else if (ac.is_neg() && !do_max) {
VERIFY(mdl.eval(m_ineq_terms[i].get(), val));
VERIFY(a.is_numeral(val, r));
r /= abs(ac); //// review.
if (!found || r < found_val) {
result = i;
found_val = r;
found = true;
}
}
}
SASSERT(found);
return result;
@ -300,11 +250,19 @@ namespace qe {
m(m), a(m), m_rw(m), m_ineq_terms(m) {}
expr_ref operator()(model& model, app_ref_vector& vars, expr_ref_vector const& lits) {
app_ref_vector new_vars(m);
expr_ref_vector result(lits);
for (unsigned i = 0; i < vars.size(); ++i) {
project(model, vars[i].get(), result);
m_var = alloc(contains_app, m, vars[i].get());
try {
project(model, result);
}
catch (cant_project) {
new_vars.push_back(vars[i].get());
}
}
vars.reset();
vars.append(new_vars);
expr_ref res1(m);
expr_ref tmp = qe::mk_and(result);
m_rw(tmp, res1);

5
src/test/qe_arith.cpp
View file

@ -17,6 +17,9 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
buffer << "(declare-const x Real)\n"
<< "(declare-const y Real)\n"
<< "(declare-const z Real)\n"
<< "(declare-const u Real)\n"
<< "(declare-const v Real)\n"
<< "(declare-const t Real)\n"
<< "(declare-const a Real)\n"
<< "(declare-const b Real)\n"
<< "(assert " << str << ")\n";
@ -31,6 +34,7 @@ static char const* example1 = "(and (<= x 3.0) (<= (* 3.0 x) y) (<= z y))";
static char const* example2 = "(and (<= z x) (<= x 3.0) (<= (* 3.0 x) y) (<= z y))";
static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y))";
static char const* example4 = "(and (<= z x) (<= x 3.0) (not (>= (* 3.0 x) y)) (<= z y))";
static char const* example5 = "(and (<= y x) (<= z x) (<= x u) (<= x v) (<= x t))";
static void test(char const *ex) {
smt_params params;
@ -61,4 +65,5 @@ void tst_qe_arith() {
test(example2);
test(example3);
test(example4);
test(example5);
}