mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #2624

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-10 19:20:02 -07:00
parent ecba7b3cde
commit ca7d066c4e
6 changed files with 66 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/ast/rewriter/arith_rewriter.cpp
View file

@ -483,6 +483,28 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
return BR_REWRITE_FULL;
}
}
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (m().is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) {
switch (kind) {
case LE: result = a1 <= a2 ? m().mk_or(c, m_util.mk_le(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a1 ? m().mk_or(c, m_util.mk_ge(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m().mk_or(c, m().mk_eq(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2;
}
}
if (m().is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) {
switch (kind) {
case LE: result = a1 <= a2 ? m().mk_or(m().mk_not(c), m_util.mk_le(t, arg2)) : m().mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a1 ? m().mk_or(m().mk_not(c), m_util.mk_ge(t, arg2)) : m().mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m().mk_or(m().mk_not(c), m().mk_eq(t, arg2)) : m().mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2;
}
}
if (m().is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) {
switch (kind) {
case LE: result = m().mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2;
case GE: result = m().mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
case EQ: result = m().mk_ite(c, m().mk_eq(t, arg2), m().mk_eq(e, arg2)); return BR_REWRITE2;
}
}
if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
a2.neg();
new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));

61
src/ast/static_features.cpp
View file

@ -20,7 +20,7 @@ Revision History:
#include "ast/ast_pp.h"
static_features::static_features(ast_manager & m):
m_manager(m),
m(m),
m_autil(m),
m_bvutil(m),
m_arrayutil(m),
@ -123,31 +123,32 @@ bool static_features::is_diff_term(expr const * e, rational & r) const {
}
if (is_numeral(e, r))
return true;
return m_autil.is_add(e) && to_app(e)->get_num_args() == 2 && is_numeral(to_app(e)->get_arg(0), r) && !is_arith_expr(to_app(e)->get_arg(1));
expr* a1 = nullptr, *a2 = nullptr;
return m_autil.is_add(e, a1, a2) && is_numeral(a1, r) && !is_arith_expr(a2) && !m.is_ite(a2);
}
bool static_features::is_diff_atom(expr const * e) const {
if (!is_bool(e))
return false;
if (!m_manager.is_eq(e) && !is_arith_expr(e))
if (!m.is_eq(e) && !is_arith_expr(e))
return false;
SASSERT(to_app(e)->get_num_args() == 2);
expr * lhs = to_app(e)->get_arg(0);
expr * rhs = to_app(e)->get_arg(1);
if (!is_arith_expr(lhs) && !is_arith_expr(rhs))
if (!is_arith_expr(lhs) && !is_arith_expr(rhs) && !m.is_ite(lhs) && !m.is_ite(rhs))
return true;
if (!is_numeral(rhs))
return false;
// lhs can be 'x' or '(+ x (* -1 y))' or '(+ (* -1 x) y)'
if (!is_arith_expr(lhs))
if (!is_arith_expr(lhs) && !m.is_ite(lhs))
return true;
expr* arg1, *arg2;
if (!m_autil.is_add(lhs, arg1, arg2))
return false;
expr* m1, *m2;
if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2))
if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2))
return true;
if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2))
if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2))
return true;
return false;
@ -159,7 +160,7 @@ bool static_features::is_gate(expr const * e) const {
case OP_ITE: case OP_AND: case OP_OR: case OP_XOR: case OP_IMPLIES:
return true;
case OP_EQ:
return m_manager.is_bool(e);
return m.is_bool(e);
}
}
return false;
@ -170,12 +171,12 @@ void static_features::update_core(expr * e) {
// even if a benchmark does not contain any theory interpreted function decls, we still have to install
// the theory if the benchmark contains constants or function applications of an interpreted sort.
sort * s = m_manager.get_sort(e);
if (!m_manager.is_uninterp(s))
sort * s = m.get_sort(e);
if (!m.is_uninterp(s))
mark_theory(s->get_family_id());
bool _is_gate = is_gate(e);
bool _is_eq = m_manager.is_eq(e);
bool _is_eq = m.is_eq(e);
if (_is_gate) {
m_cnf = false;
m_num_nested_formulas++;
@ -191,12 +192,12 @@ void static_features::update_core(expr * e) {
acc_num(arg);
// Must check whether arg is diff logic or not.
// Otherwise, problem can be incorrectly tagged as diff logic.
sort * arg_s = m_manager.get_sort(arg);
sort * arg_s = m.get_sort(arg);
family_id fid_arg = arg_s->get_family_id();
if (fid_arg == m_afid) {
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
@ -238,7 +239,7 @@ void static_features::update_core(expr * e) {
bool _is_le_ge = m_autil.is_le(e) || m_autil.is_ge(e);
if (_is_le_ge) {
m_num_arith_ineqs++;
TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m_manager) << "\n";);
TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";);
if (is_diff_atom(e))
m_num_diff_ineqs++;
if (!is_arith_expr(to_app(e)->get_arg(0)))
@ -255,14 +256,14 @@ void static_features::update_core(expr * e) {
if (is_numeral(to_app(e)->get_arg(1))) {
acc_num(to_app(e)->get_arg(1));
m_num_arith_eqs++;
TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m_manager) << "\n";);
TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";);
if (is_diff_atom(e))
m_num_diff_eqs++;
if (!is_arith_expr(to_app(e)->get_arg(0)))
m_num_simple_eqs++;
}
sort * s = m_manager.get_sort(to_app(e)->get_arg(0));
if (!m_manager.is_uninterp(s)) {
sort * s = m.get_sort(to_app(e)->get_arg(0));
if (!m.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_eqs(fid);
@ -300,7 +301,7 @@ void static_features::update_core(expr * e) {
m_num_interpreted_constants++;
}
if (fid == m_afid) {
// std::cout << mk_pp(e, m_manager) << "\n";
// std::cout << mk_pp(e, m) << "\n";
switch (to_app(e)->get_decl_kind()) {
case OP_MUL:
if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) {
@ -320,8 +321,8 @@ void static_features::update_core(expr * e) {
m_num_uninterpreted_exprs++;
if (to_app(e)->get_num_args() == 0) {
m_num_uninterpreted_constants++;
sort * s = m_manager.get_sort(e);
if (!m_manager.is_uninterp(s)) {
sort * s = m.get_sort(e);
if (!m.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_constants(fid);
@ -329,7 +330,7 @@ void static_features::update_core(expr * e) {
}
}
if (m_arrayutil.is_array(e)) {
TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";);
TRACE("sf_array", tout << mk_ismt2_pp(e, m) << "\n";);
sort * ty = to_app(e)->get_decl()->get_range();
mark_theory(ty->get_family_id());
unsigned n = ty->get_num_parameters();
@ -347,8 +348,8 @@ void static_features::update_core(expr * e) {
}
if (!_is_eq && !_is_gate) {
for (expr * arg : *to_app(e)) {
sort * arg_s = m_manager.get_sort(arg);
if (!m_manager.is_uninterp(arg_s)) {
sort * arg_s = m.get_sort(arg);
if (!m.is_uninterp(arg_s)) {
family_id fid_arg = arg_s->get_family_id();
if (fid_arg != fid && fid_arg != null_family_id) {
m_num_aliens++;
@ -357,7 +358,7 @@ void static_features::update_core(expr * e) {
SASSERT(!_is_le_ge);
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
@ -385,7 +386,7 @@ void static_features::update_core(sort * s) {
}
void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) {
TRACE("static_features", tout << "processing\n" << mk_pp(e, m_manager) << "\n";);
TRACE("static_features", tout << "processing\n" << mk_pp(e, m) << "\n";);
if (is_var(e))
return;
if (is_marked(e)) {
@ -413,7 +414,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
if (is_basic_expr(e)) {
switch (to_app(e)->get_decl_kind()) {
case OP_ITE:
form_ctx_new = m_manager.is_bool(e);
form_ctx_new = m.is_bool(e);
ite_ctx_new = true;
break;
case OP_AND:
@ -435,7 +436,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
unsigned num_args = to_app(e)->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(e)->get_arg(i);
if (m_manager.is_not(arg))
if (m.is_not(arg))
arg = to_app(arg)->get_arg(0);
process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new, stack_depth+1);
depth = std::max(depth, get_depth(arg));
@ -490,7 +491,7 @@ void static_features::process_root(expr * e) {
return;
}
m_num_roots++;
if (m_manager.is_or(e)) {
if (m.is_or(e)) {
mark(e);
m_num_clauses++;
m_num_bool_exprs++;
@ -503,7 +504,7 @@ void static_features::process_root(expr * e) {
unsigned or_and_depth = 0;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(e)->get_arg(i);
if (m_manager.is_not(arg))
if (m.is_not(arg))
arg = to_app(arg)->get_arg(0);
process(arg, true, true, false, 0);
depth = std::max(depth, get_depth(arg));
@ -547,7 +548,7 @@ bool static_features::internal_family(symbol const & f_name) const {
void static_features::display_family_data(std::ostream & out, char const * prefix, unsigned_vector const & data) const {
for (unsigned fid = 0; fid < data.size(); fid++) {
symbol const & n = m_manager.get_family_name(fid);
symbol const & n = m.get_family_name(fid);
if (!internal_family(n))
out << prefix << "_" << n << " " << data[fid] << "\n";
}

6
src/ast/static_features.h
View file

@ -29,7 +29,7 @@ Revision History:
#include "util/map.h"
struct static_features {
ast_manager & m_manager;
ast_manager & m;
arith_util m_autil;
bv_util m_bvutil;
array_util m_arrayutil;
@ -120,7 +120,7 @@ struct static_features {
bool is_marked(ast * e) const { return m_already_visited.is_marked(e); }
void mark(ast * e) { m_already_visited.mark(e, true); }
bool is_bool(expr const * e) const { return m_manager.is_bool(e); }
bool is_bool(expr const * e) const { return m.is_bool(e); }
bool is_basic_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_bfid; }
bool is_arith_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_afid; }
bool is_numeral(expr const * e) const { return m_autil.is_numeral(e); }
@ -130,7 +130,7 @@ struct static_features {
bool is_diff_atom(expr const * e) const;
bool is_gate(expr const * e) const;
void mark_theory(family_id fid) {
if (fid != null_family_id && !m_manager.is_builtin_family_id(fid) && !m_theories.get(fid, false)) {
if (fid != null_family_id && !m.is_builtin_family_id(fid) && !m_theories.get(fid, false)) {
m_theories.setx(fid, true, false);
m_num_theories++;
}

2
src/smt/params/smt_params.cpp
View file

@ -142,7 +142,6 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_profile_res_sub);
DISPLAY_PARAM(m_display_bool_var2expr);
DISPLAY_PARAM(m_display_ll_bool_var2expr);
DISPLAY_PARAM(m_abort_after_preproc);
DISPLAY_PARAM(m_model);
DISPLAY_PARAM(m_model_compact);
@ -151,7 +150,6 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_progress_sampling_freq);
DISPLAY_PARAM(m_display_installed_theories);
DISPLAY_PARAM(m_core_validate);
DISPLAY_PARAM(m_preprocess);

4
src/smt/params/smt_params.h
View file

@ -181,7 +181,6 @@ struct smt_params : public preprocessor_params,
bool m_profile_res_sub;
bool m_display_bool_var2expr;
bool m_display_ll_bool_var2expr;
bool m_abort_after_preproc;
// -----------------------------------
//
@ -205,7 +204,6 @@ struct smt_params : public preprocessor_params,
// Debugging goodies
//
// -----------------------------------
bool m_display_installed_theories;
bool m_core_validate;
// -----------------------------------
@ -292,13 +290,11 @@ struct smt_params : public preprocessor_params,
m_profile_res_sub(false),
m_display_bool_var2expr(false),
m_display_ll_bool_var2expr(false),
m_abort_after_preproc(false),
m_model(true),
m_model_compact(false),
m_model_on_timeout(false),
m_model_on_final_check(false),
m_progress_sampling_freq(0),
m_display_installed_theories(false),
m_core_validate(false),
m_preprocess(true), // temporary hack for disabling all preprocessing..
m_user_theory_preprocess_axioms(false),

39
src/smt/smt_context.cpp
View file

@ -1091,10 +1091,9 @@ namespace smt {
tout << mk_ll_pp(r2->get_owner(), m_manager) << "\n";
);
#ifdef Z3DEBUG
push_trail(push_back_trail<context, enode_pair, false>(m_diseq_vector));
m_diseq_vector.push_back(enode_pair(n1, n2));
#endif
DEBUG_CODE(
push_trail(push_back_trail<context, enode_pair, false>(m_diseq_vector));
m_diseq_vector.push_back(enode_pair(n1, n2)););
if (r1 == r2) {
TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
@ -1299,7 +1298,7 @@ namespace smt {
enode * tmp = m_tmp_enode.set(f, num_args, args);
enode * r = m_cg_table.find(tmp);
#ifdef Z3DEBUG
if (r != 0) {
if (r != nullptr) {
SASSERT(r->get_owner()->get_decl() == f);
SASSERT(r->get_num_args() == num_args);
if (r->is_commutative()) {
@ -1592,9 +1591,7 @@ namespace smt {
}
}
TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";);
#ifndef SMTCOMP
m_case_split_queue->relevant_eh(n);
#endif
if (is_app(n)) {
if (e_internalized(n)) {
@ -1662,10 +1659,9 @@ namespace smt {
theory * th = get_theory(curr.m_th_id);
SASSERT(th);
th->new_eq_eh(curr.m_lhs, curr.m_rhs);
#ifdef Z3DEBUG
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_eqs));
m_propagated_th_eqs.push_back(curr);
#endif
DEBUG_CODE(
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_eqs));
m_propagated_th_eqs.push_back(curr););
}
m_th_eq_propagation_queue.reset();
}
@ -1676,10 +1672,9 @@ namespace smt {
theory * th = get_theory(curr.m_th_id);
SASSERT(th);
th->new_diseq_eh(curr.m_lhs, curr.m_rhs);
#ifdef Z3DEBUG
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_diseqs));
m_propagated_th_diseqs.push_back(curr);
#endif
DEBUG_CODE(
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_diseqs));
m_propagated_th_diseqs.push_back(curr););
}
m_th_diseq_propagation_queue.reset();
}
@ -3407,15 +3402,6 @@ namespace smt {
return;
m_setup(get_config_mode(use_static_features));
setup_components();
#ifndef _EXTERNAL_RELEASE
if (m_fparams.m_display_installed_theories) {
std::cout << "(theories";
for (theory* th : m_theory_set) {
std::cout << " " << th->get_name();
}
std::cout << ")" << std::endl;
}
#endif
}
void context::setup_components() {
@ -3542,11 +3528,6 @@ namespace smt {
lbool context::search() {
#ifndef _EXTERNAL_RELEASE
if (m_fparams.m_abort_after_preproc) {
exit(1);
}
#endif
if (m_asserted_formulas.inconsistent())
return l_false;
if (inconsistent()) {