diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index 7e2478347..d5fc9af0c 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -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; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index da71891a4..732bde404 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -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 args1, args2; flat_mul(num, args1); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index bebe21420..fbcf87d65 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index f11b7ccd1..147453d54 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -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(); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index b5ad96fe7..c223922f5 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -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 } }