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

fix #3239

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-11 09:35:28 -07:00
parent e32020ba10
commit e45871d7c5
5 changed files with 51 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/ast_ll_pp.cpp
View file

@ -53,7 +53,8 @@ class ll_printer {
rational val;
bool is_int;
if (m_autil.is_numeral(n, val, is_int)) {
m_out << val << "::" << (is_int ? "Int" : "Real");
m_out << val;
if (!is_int && val.is_int()) m_out << ".0";
return true;
}
return false;

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

@ -869,11 +869,14 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
}
}
if (divides(arg1, arg2, result)) {
expr_ref zero(m_util.mk_int(0), m());
result = m().mk_ite(m().mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
return BR_REWRITE_FULL;
}
}
return BR_FAILED;
}
//
// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
//
@ -920,6 +923,7 @@ bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
return false;
}
expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
ptr_buffer<expr> args1, args2;
flat_mul(num, args1);

42
src/smt/smt_context.cpp
View file

@ -3370,7 +3370,7 @@ namespace smt {
for (theory* t : m_theory_set) {
t->validate_model(*mdl);
}
#if 0
#if 1
for (literal lit : m_assigned_literals) {
if (!is_relevant(lit)) continue;
expr* v = m_bool_var2expr[lit.var()];
@ -3382,6 +3382,7 @@ namespace smt {
}
for (clause* cls : m_aux_clauses) {
bool found = false;
IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "check:\n", *cls) << "\n");
for (literal lit : *cls) {
expr* v = m_bool_var2expr[lit.var()];
if (lit.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
@ -3393,6 +3394,45 @@ namespace smt {
IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");
}
}
for (clause* cls : m_lemmas) {
bool found = false;
IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "check:\n", *cls) << "\n");
for (literal lit : *cls) {
expr* v = m_bool_var2expr[lit.var()];
if (lit.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
found = true;
break;
}
}
if (!found) {
IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");
}
}
unsigned l_idx = 0;
for (watch_list const& wl : m_watches) {
literal l1 = to_literal(l_idx++);
literal neg_l1 = ~l1;
expr* v = m_bool_var2expr[l1.var()];
if (neg_l1.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
continue;
}
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
for (; it2 != end2; ++it2) {
literal l2 = *it2;
if (l1.index() >= l2.index()) {
continue;
}
literal lits[2] = { neg_l1, l2 };
IF_VERBOSE(10, display_literals_smt2(verbose_stream() << "check: ", 2, lits) << "\n";);
v = m_bool_var2expr[l2.var()];
if (l2.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
continue;
}
IF_VERBOSE(10, display_literals_smt2(verbose_stream() << "not satisfied: ", 2, lits) << "\n";);
}
}
#endif
}
return r;

6
src/smt/smt_theory.cpp
View file

@ -57,8 +57,7 @@ namespace smt {
std::ostream& theory::display_app(std::ostream & out, app * n) const {
func_decl * d = n->get_decl();
if (n->get_num_args() == 0) {
out << d->get_name();
display_parameters(out, d->get_num_parameters(), d->get_parameters());
out << mk_bounded_pp(n, get_manager(), 1);
}
else if (n->get_family_id() == get_family_id()) {
out << "(" << d->get_name();
@ -79,8 +78,7 @@ namespace smt {
std::ostream& theory::display_flat_app(std::ostream & out, app * n) const {
func_decl * d = n->get_decl();
if (n->get_num_args() == 0) {
out << d->get_name();
display_parameters(out, d->get_num_parameters(), d->get_parameters());
display_app(out, n);
}
else if (n->get_family_id() == get_family_id()) {
out << "(" << d->get_name();

51
src/smt/theory_arith_core.h
View file

@ -493,7 +493,7 @@ namespace smt {
literal l_conseq = ctx.get_literal(s_conseq);
if (negated) l_conseq.neg();
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
TRACE("arith", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
tout << s_ante << "\n" << s_conseq << "\n";
tout << l_ante << "\n" << l_conseq << "\n";);
@ -581,7 +581,6 @@ namespace smt {
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) {
rational j(0);
#if 1
literal_buffer lits;
expr_ref mod_j(m);
while(j < k) {
@ -595,55 +594,7 @@ namespace smt {
j += rational(1);
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.begin());
#else
// performs slightly worse.
literal_buffer lits;
expr_ref mod_j(m), div_j(m), num_j(m), n_mod_j(m), n_div_j(m);
context& ctx = get_context();
while(j < k) {
num_j = m_util.mk_numeral(j, true);
mod_j = m.mk_eq(mod, num_j);
div_j = m.mk_eq(dividend, m_util.mk_add(m_util.mk_mul(div, divisor), num_j));
n_mod_j = m.mk_not(mod_j);
n_div_j = m.mk_not(div_j);
mk_axiom(n_mod_j, div_j);
mk_axiom(n_div_j, mod_j);
j += rational(1);
}
#endif
}
#if 0
// e-matching is too restrictive for multiplication.
// also suffers from use-after free so formulas have to be pinned in solver.
//
if (!m_util.is_numeral(divisor)) {
//
// forall x . (or (= y 0) (= (div (* x y) y) x))
// forall x . (=> (= y 0) (= (div (* x y) y) (div 0 0)))
//
sort* intS = m_util.mk_int();
var_ref v(m.mk_var(0, intS), m);
app_ref mul(m_util.mk_mul(divisor, v), m);
app_ref div(m_util.mk_idiv(mul, divisor), m);
expr_ref divp1(m.mk_pattern(div), m);
app_ref mul2(m_util.mk_mul(v, divisor), m);
app_ref div2(m_util.mk_idiv(mul2, divisor), m);
expr_ref divp2(m.mk_pattern(div2), m);
expr_ref fml1(m.mk_or(m.mk_not(eqz), m.mk_eq(div, m_util.mk_idiv(zero, zero))), m);
expr_ref fml2(m.mk_or(eqz, m.mk_eq(div, v)), m);
symbol name("?x");
expr* pats[2] = { divp1, divp2 };
expr_ref fml(m);
fml = m.mk_forall(1, &intS, &name, fml1, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
proof_ref pr(m.mk_asserted(fml), m);
ctx.internalize_assertion(fml, pr, 0);
fml = m.mk_forall(1, &intS, &name, fml2, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
pr = m.mk_asserted(fml);
ctx.internalize_assertion(fml, pr, 0);
}
#endif
}
}