mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

avoid empty lemmas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-15 16:44:27 -07:00
parent 40cc8c31e5
commit b2b4193afa
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/nla_core.cpp
View file

@ -1625,6 +1625,7 @@ bool core::find_bfc_to_refine(const monomial* & m, factorization & bf){
} }
void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) { void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
add_empty_lemma();
SASSERT(sign == nla::rat_sign(product_value(m.vars()))); SASSERT(sign == nla::rat_sign(product_value(m.vars())));
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
if (val(j).is_pos()) { if (val(j).is_pos()) {

2
src/util/lp/nla_tangent_lemmas.cpp
View file

@ -104,7 +104,6 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
if (m.size() != 2) if (m.size() != 2)
return; return;
TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;); TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
c().add_empty_lemma();
const rational v = c().product_value(m.vars()); const rational v = c().product_value(m.vars());
const rational mv = val(m); const rational mv = val(m);
SASSERT(mv != v); SASSERT(mv != v);
@ -115,6 +114,7 @@ void tangents::generate_simple_tangent_lemma(const monomial& m) {
return; return;
} }
/* /*
c().add_empty_lemma();
bool gt = abs(mv) > abs(v); bool gt = abs(mv) > abs(v);
if (gt) { if (gt) {
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {