mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

port Grobner: still producing sat lemmas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-31 20:14:43 -07:00
parent 7416a8cbb9
commit ede4310b32
2 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nex_creator.cpp
View file

@ -671,7 +671,7 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
for (auto& p : map) { for (auto& p : map) {
process_map_pair(p.first, p.second, children, allocated_nexs); process_map_pair(p.first, p.second, children, allocated_nexs);
} }
if (common_scalar) { if (common_scalar && !common_scalar->value().is_zero()) {
children.push_back(common_scalar); children.push_back(common_scalar);
} }
TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});

14
src/math/lp/nla_common.cpp
View file

@ -125,9 +125,13 @@ unsigned common::random() {
// creates a nex expression for the coeff and var, // creates a nex expression for the coeff and var,
// replaces the fixed vars with scalars // replaces the fixed vars with scalars
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) { nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) {
SASSERT(!coeff.is_zero());
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
if (fixed_as_scalars && c().var_is_fixed(j)) { if (fixed_as_scalars && c().var_is_fixed(j)) {
return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); auto & b = c().m_lar_solver.get_lower_bound(j).x;
if (b.is_zero())
return nullptr;
return cn.mk_scalar(coeff * b);
} }
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
@ -136,7 +140,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
for (lpvar k : m.vars()) { for (lpvar k : m.vars()) {
if (fixed_as_scalars && c().var_is_fixed(k)) { if (fixed_as_scalars && c().var_is_fixed(k)) {
e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; auto & b = c().m_lar_solver.get_lower_bound(j).x;
if (b.is_zero())
return nullptr;
e->coeff() *= b;
continue; continue;
} }
c().insert_to_active_var_set(k); c().insert_to_active_var_set(k);
@ -157,7 +164,8 @@ template <typename T> void common::create_sum_from_row(const T& row,
sum.children().clear(); sum.children().clear();
for (const auto &p : row) { for (const auto &p : row) {
nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars); nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars);
sum.add_child(e); if (e)
sum.add_child(e);
} }
TRACE("nla_horner", tout << "sum =" << sum << "\n";); TRACE("nla_horner", tout << "sum =" << sum << "\n";);
} }