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

produce a lemma on a row when there is no cross nested form

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-24 07:41:36 -07:00
parent 2a02d04259
commit e0f1e3cc3e
1 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/cross_nested.h
View file

@ -30,7 +30,7 @@ public:
void run() { void run() {
vector<nex*> front; vector<nex*> front;
explore_expr_on_front_elem(&m_e, front, true); // true for trivial form - no change explore_expr_on_front_elem(&m_e, front); // true for trivial form - no change
} }
static nex* pop_back(vector<nex*>& front) { static nex* pop_back(vector<nex*>& front) {
@ -92,7 +92,7 @@ public:
f.simplify(); f.simplify();
* c = nex::mul(f, *c); * c = nex::mul(f, *c);
TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";); TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";);
explore_expr_on_front_elem(&(c->children()[1]), front, false); explore_expr_on_front_elem(&(c->children()[1]), front);
return true; return true;
} }
@ -142,21 +142,19 @@ public:
return out; return out;
} }
void explore_expr_on_front_elem(nex* c, vector<nex*>& front, bool trivial_form) { void explore_expr_on_front_elem(nex* c, vector<nex*>& front) {
SASSERT(c->is_sum()); SASSERT(c->is_sum());
auto occurences = get_mult_occurences(*c); auto occurences = get_mult_occurences(*c);
TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences="; TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences=";
dump_occurences(tout, occurences) << "; front:"; print_vector_of_ptrs(front, tout) << "\ntrivial_form=" << trivial_form << "\n";); dump_occurences(tout, occurences) << "; front:"; print_vector_of_ptrs(front, tout) << "\n";);
if (occurences.empty()) { if (occurences.empty()) {
if(front.empty()) { if(front.empty()) {
if (trivial_form)
return;
TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";); TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";);
m_call_on_result(m_e); m_call_on_result(m_e);
} else { } else {
nex* c = pop_back(front); nex* c = pop_back(front);
explore_expr_on_front_elem(c, front, trivial_form); explore_expr_on_front_elem(c, front);
} }
} else { } else {
explore_expr_on_front_elem_occs(c, front, occurences); explore_expr_on_front_elem_occs(c, front, occurences);
@ -173,7 +171,7 @@ public:
TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";); TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
SASSERT(front.size()); SASSERT(front.size());
nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";); nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";);
explore_expr_on_front_elem(n, front, false); // we got a non-trivial_form explore_expr_on_front_elem(n, front);
} }
static void process_var_occurences(lpvar j, std::unordered_map<lpvar, occ>& occurences) { static void process_var_occurences(lpvar j, std::unordered_map<lpvar, occ>& occurences) {
auto it = occurences.find(j); auto it = occurences.find(j);