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

simplify

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-12 10:27:56 -07:00 • committed by Lev Nachmanson
parent 9db5b3d658
commit 5cdcfeecf2
1 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -45,7 +45,7 @@ struct solver::imp {
vector<mono_index_with_sign>, vector<mono_index_with_sign>,
hash_svector> hash_svector>
m_rooted_monomials; m_rooted_monomials;
// this field is used for push/pop operations // this field is used for the push/pop operations
unsigned_vector m_monomials_counts; unsigned_vector m_monomials_counts;
lp::lar_solver& m_lar_solver; lp::lar_solver& m_lar_solver;
std::unordered_map<lpvar, unsigned_vector> m_monomials_containing_var; std::unordered_map<lpvar, unsigned_vector> m_monomials_containing_var;
@ -127,7 +127,12 @@ struct solver::imp {
return out; return out;
} }
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, lp::lconstraint_kind cmp, const rational& rs) {
lp::lar_term t;
t.add_coeff_var(a, j);
t.add_coeff_var(b, k);
m_lemma->push_back(ineq(cmp, t, rs));
}
// the monomials should be equal by modulo sign, but they are not equal in the model by modulo sign // the monomials should be equal by modulo sign, but they are not equal in the model by modulo sign
void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) { void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) {
expl_set expl; expl_set expl;
@ -142,11 +147,7 @@ struct solver::imp {
m_lar_solver.print_constraint(p.second, tout); tout << "\n"; m_lar_solver.print_constraint(p.second, tout); tout << "\n";
); );
SASSERT(m_lemma->size() == 0); SASSERT(m_lemma->size() == 0);
lp::lar_term t; mk_ineq(rational(1), a.var(), -sign, b.var(), lp::lconstraint_kind::EQ, rational::zero());
t.add_coeff_var(rational(1), a.var());
t.add_coeff_var(-sign, b.var());
ineq in(lp::lconstraint_kind::EQ, t, rational::zero());
m_lemma->push_back(in);
TRACE("nla_solver", print_explanation_and_lemma(tout);); TRACE("nla_solver", print_explanation_and_lemma(tout););
} }
@ -369,7 +370,7 @@ struct solver::imp {
} }
} }
void ineq_j_is_equal_to_zero_add_to_lemma(lpvar j) { void mk_var_EQ_zero(lpvar j) {
m_lemma->push_back(ineq_j_is_equal_to_zero(j)); m_lemma->push_back(ineq_j_is_equal_to_zero(j));
} }
@ -1009,7 +1010,7 @@ struct solver::imp {
} }
ineq_j_is_nequal_to_zero_add_to_lemma(zero_j); ineq_j_is_nequal_to_zero_add_to_lemma(zero_j);
ineq_j_is_equal_to_zero_add_to_lemma(m_monomials[i_mon].var()); mk_var_EQ_zero(m_monomials[i_mon].var());
expl_set e; expl_set e;
add_explanation_of_factorization(i_mon, f, e); add_explanation_of_factorization(i_mon, f, e);