mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-13 20:32:18 -07:00
parent 63f89f8c45
commit 3989d238c0
8 changed files with 78 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/macros/macro_finder.cpp
View file

@ -22,13 +22,13 @@ Revision History:
#include"ast_pp.h"
#include"ast_ll_pp.h"
bool macro_finder::is_macro(expr * n, app * & head, expr * & def) {
bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false;
TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls();
return m_util.is_simple_macro(body, num_decls, head, def);
return m_util.is_ite_macro(body, num_decls, head, def);
}
/**
@ -171,23 +171,20 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
for (unsigned i = 0; i < num; i++) {
expr * n = exprs[i];
proof * pr = m_manager.proofs_enabled() ? prs[i] : 0;
expr_ref new_n(m_manager);
expr_ref new_n(m_manager), def(m_manager);
proof_ref new_pr(m_manager);
m_macro_manager.expand_macros(n, pr, new_n, new_pr);
app * head = 0;
expr * def = 0;
app * t = 0;
app_ref head(m_manager), t(m_manager);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << mk_pp(new_n, m_manager) << "\n";);
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
found_new_macro = true;
}
else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) {
TRACE("macro_finder_found", tout << "found new arith macro:\n" << mk_pp(new_n, m_manager) << "\n";);
TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
found_new_macro = true;
}
else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << mk_pp(head, m_manager) << "\n" << mk_pp(t, m_manager) << "\n" <<
mk_pp(def, m_manager) << "\n";);
TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
found_new_macro = true;
}

2
src/ast/macros/macro_finder.h
View file

@ -41,7 +41,7 @@ class macro_finder {
bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool is_macro(expr * n, app * & head, expr * & def);
bool is_macro(expr * n, app_ref & head, expr_ref & def);
bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);

30
src/ast/macros/macro_util.cpp
View file

@ -176,7 +176,7 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
def will contain t
*/
bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
@ -189,6 +189,22 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head
return false;
}
bool macro_util::is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const {
if (is_simple_macro(n, num_decls, head, def)) {
return true;
}
expr* c, *t, *e;
expr_ref def1(m_manager), def2(m_manager);
app_ref head2(m_manager);
if (m_manager.is_ite(n, c, t, e) &&
is_ite_macro(t, num_decls, head, def1) &&
is_ite_macro(e, num_decls, head2, def2) && head == head2) {
def = m_manager.mk_ite(c, def1, def2);
return true;
}
return false;
}
/**
\brief Return true if n is of the form
@ -206,7 +222,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head
def will contain t
*/
bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
@ -302,7 +318,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
/**
\brief Auxiliary function for is_pseudo_predicate_macro. It detects the pattern (= (f X) t)
*/
bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t) {
bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) {
if (!m_manager.is_eq(n))
return false;
expr * lhs = to_app(n)->get_arg(0);
@ -332,7 +348,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app * & head, app
\brief Returns true if n if of the form (forall (X) (iff (= (f X) t) def[X]))
where t is a ground term, (f X) is the head.
*/
bool macro_util::is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def) {
bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false;
TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@ -870,9 +886,8 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
THEN M'(atom) = true
*/
void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) {
if (m_manager.is_eq(atom) || m_manager.is_iff(atom)) {
expr * lhs = to_app(atom)->get_arg(0);
expr * rhs = to_app(atom)->get_arg(1);
expr* lhs, *rhs;
if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
if (is_quasi_macro_head(lhs, num_decls) &&
!is_forbidden(to_app(lhs)->get_decl()) &&
!occurs(to_app(lhs)->get_decl(), rhs) &&
@ -884,7 +899,6 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
else if (is_hint_atom(lhs, rhs)) {
insert_quasi_macro(to_app(lhs), num_decls, rhs, 0, false, true, true, r);
}
if (is_quasi_macro_head(rhs, num_decls) &&
!is_forbidden(to_app(rhs)->get_decl()) &&

11
src/ast/macros/macro_util.h
View file

@ -102,11 +102,12 @@ public:
basic_simplifier_plugin * get_basic_simp() const;
bool is_macro_head(expr * n, unsigned num_decls) const;
bool is_left_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const;
bool is_right_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const;
bool is_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
bool is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def);
}
bool is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const;
bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
@ -114,8 +115,8 @@ public:
return is_arith_macro(n, num_decls, head, def, inv);
}
bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
void quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const;