mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

reimplement lemmas on rooted monomials

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-26 16:02:31 -08:00 • committed by Lev Nachmanson
parent 7e03e900b8
commit d3c9cdab4a
1 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/lp/nla_solver.cpp
View file

@ -599,9 +599,9 @@ struct solver::imp {
// |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1
bool basic_lemma_for_mon_neutral_monomial_to_factor(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_neutral_monomial_to_factor(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
/*
// todo : consider the case of just two factors // todo : consider the case of just two factors
lpvar mon_var = m_monomials[i_mon].var(); lpvar mon_var = m_monomials[rm.orig_index()].var();
const auto & mv = vvr(mon_var); const auto & mv = vvr(mon_var);
const auto abs_mv = abs(mv); const auto abs_mv = abs(mv);
@ -645,10 +645,9 @@ struct solver::imp {
// not_one_j = -1 // not_one_j = -1
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1)); mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1));
expl_set e; expl_set e;
add_explanation_of_factorization_and_set_explanation(i_mon, f, e); add_explanation_of_factorization_and_set_explanation(rm, f, e);
TRACE("nla_solver", print_lemma(tout); ); TRACE("nla_solver", print_lemma(tout); );
return true;*/ return true;
return false;
} }
// use the fact // use the fact