mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
debugging nra
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b18dc7d052
commit
1086eaaa1f
|
@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
|
||||
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
|
||||
|
||||
|
||||
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
|
||||
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
|
||||
// increment reference counters
|
||||
|
|
|
@ -738,9 +738,54 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
|
|||
result = m_util.mk_idiv0(arg1);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
expr_ref quot(m());
|
||||
if (divides(arg1, arg2, quot)) {
|
||||
result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
|
||||
if (d == n) {
|
||||
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
|
||||
return true;
|
||||
}
|
||||
if (m_util.is_mul(n)) {
|
||||
expr_ref_vector muls(m());
|
||||
muls.push_back(n);
|
||||
expr* n1, *n2;
|
||||
rational r1, r2;
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_mul(muls[i].get(), n1, n2)) {
|
||||
muls[i] = n1;
|
||||
muls.push_back(n2);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
|
||||
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (d == muls[i].get()) {
|
||||
muls[i] = muls.back();
|
||||
muls.pop_back();
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(m().get_sort(arg1));
|
||||
numeral v1, v2;
|
||||
|
|
|
@ -90,6 +90,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
|
|||
bool is_pi_integer_offset(expr * t, expr * & m);
|
||||
expr * mk_sin_value(rational const & k);
|
||||
app * mk_sqrt(rational const & k);
|
||||
bool divides(expr* d, expr* n, expr_ref& quot);
|
||||
|
||||
public:
|
||||
arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):
|
||||
|
|
|
@ -267,10 +267,55 @@ void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & resul
|
|||
bool is_int;
|
||||
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
|
||||
result = m_util.mk_numeral(div(v1, v2), is_int);
|
||||
else if (divides(arg2, arg1, result)) {
|
||||
result = m_util.mk_mul(result, m_util.mk_idiv(arg2, arg2));
|
||||
}
|
||||
else
|
||||
result = m_util.mk_idiv(arg1, arg2);
|
||||
}
|
||||
|
||||
bool arith_simplifier_plugin::divides(expr* d, expr* n, expr_ref& quot) {
|
||||
ast_manager& m = m_manager;
|
||||
if (d == n) {
|
||||
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
|
||||
return true;
|
||||
}
|
||||
if (m_util.is_mul(n)) {
|
||||
expr_ref_vector muls(m);
|
||||
muls.push_back(n);
|
||||
expr* n1, *n2;
|
||||
rational r1, r2;
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_mul(muls[i].get(), n1, n2)) {
|
||||
muls[i] = n1;
|
||||
muls.push_back(n2);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
|
||||
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (d == muls[i].get()) {
|
||||
muls[i] = muls.back();
|
||||
muls.pop_back();
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
|
||||
SASSERT(m_util.is_int(e));
|
||||
SASSERT(k.is_int() && k.is_pos());
|
||||
|
|
|
@ -48,6 +48,7 @@ protected:
|
|||
|
||||
void div_monomial(expr_ref_vector& monomials, numeral const& g);
|
||||
void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
|
||||
bool divides(expr* d, expr* n, expr_ref& quot);
|
||||
|
||||
public:
|
||||
arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);
|
||||
|
|
|
@ -388,6 +388,7 @@ namespace smt {
|
|||
enode * n = *it3;
|
||||
if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
|
||||
func_decl * d = n->get_owner()->get_decl();
|
||||
TRACE("mg_top_sort", tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";);
|
||||
if (m_hidden_ufs.contains(d)) continue;
|
||||
expr * val = get_value(n);
|
||||
m_model->register_decl(d, val);
|
||||
|
|
|
@ -425,8 +425,11 @@ namespace smt {
|
|||
|
||||
void internalize_mul(app* t, theory_var& v, rational& r) {
|
||||
SASSERT(a.is_mul(t));
|
||||
internalize_args(t);
|
||||
mk_enode(t);
|
||||
bool _has_var = has_var(t);
|
||||
if (!_has_var) {
|
||||
internalize_args(t);
|
||||
mk_enode(t);
|
||||
}
|
||||
r = rational::one();
|
||||
rational r1;
|
||||
v = mk_var(t);
|
||||
|
@ -451,7 +454,10 @@ namespace smt {
|
|||
vars.push_back(get_var_index(mk_var(n)));
|
||||
}
|
||||
}
|
||||
m_solver->add_monomial(get_var_index(v), vars);
|
||||
TRACE("arith", tout << mk_pp(t, m) << "\n";);
|
||||
if (!_has_var) {
|
||||
m_solver->add_monomial(get_var_index(v), vars);
|
||||
}
|
||||
}
|
||||
|
||||
enode * mk_enode(app * n) {
|
||||
|
@ -498,6 +504,14 @@ namespace smt {
|
|||
return m_arith_params.m_arith_reflect || is_underspecified(n);
|
||||
}
|
||||
|
||||
bool has_var(expr* n) {
|
||||
if (!ctx().e_internalized(n)) {
|
||||
return false;
|
||||
}
|
||||
enode* e = get_enode(n);
|
||||
return th.is_attached_to_var(e);
|
||||
}
|
||||
|
||||
theory_var mk_var(expr* n, bool internalize = true) {
|
||||
if (!ctx().e_internalized(n)) {
|
||||
ctx().internalize(n, false);
|
||||
|
@ -2281,6 +2295,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void set_conflict() {
|
||||
m_explanation.clear();
|
||||
m_solver->get_infeasibility_explanation(m_explanation);
|
||||
set_conflict1();
|
||||
}
|
||||
|
@ -2289,7 +2304,6 @@ namespace smt {
|
|||
m_eqs.reset();
|
||||
m_core.reset();
|
||||
m_params.reset();
|
||||
m_explanation.clear();
|
||||
// m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
|
||||
/*
|
||||
static unsigned cn = 0;
|
||||
|
@ -2340,7 +2354,10 @@ namespace smt {
|
|||
|
||||
model_value_proc * mk_value(enode * n, model_generator & mg) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
return alloc(expr_wrapper_proc, m_factory->mk_value(get_value(v), m.get_sort(n->get_owner())));
|
||||
expr* o = n->get_owner();
|
||||
rational r = get_value(v);
|
||||
if (a.is_int(o) && !r.is_int()) r = floor(r);
|
||||
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
|
||||
}
|
||||
|
||||
bool get_value(enode* n, expr_ref& r) {
|
||||
|
@ -2366,6 +2383,7 @@ namespace smt {
|
|||
if (dump_lemmas()) {
|
||||
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
|
||||
}
|
||||
if (m_arith_params.m_arith_mode == AS_LRA) return true;
|
||||
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
||||
add_background(nctx);
|
||||
bool result = l_true != nctx.check();
|
||||
|
@ -2378,6 +2396,7 @@ namespace smt {
|
|||
if (dump_lemmas()) {
|
||||
ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
|
||||
}
|
||||
if (m_arith_params.m_arith_mode == AS_LRA) return true;
|
||||
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
||||
m_core.push_back(~lit);
|
||||
add_background(nctx);
|
||||
|
@ -2389,6 +2408,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool validate_eq(enode* x, enode* y) {
|
||||
if (m_arith_params.m_arith_mode == AS_LRA) return true;
|
||||
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
||||
add_background(nctx);
|
||||
nctx.assert_expr(m.mk_not(m.mk_eq(x->get_owner(), y->get_owner())));
|
||||
|
|
Loading…
Reference in a new issue