mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

port Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-22 13:27:22 -07:00
parent 5a2ce93ed7
commit 47bb9b2689
1 changed files with 24 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/math/lp/nla_grobner.cpp
View file

@ -499,13 +499,13 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
if (!find_b_c(ab, ac, b, c)) {
return;
}
NOT_IMPLEMENTED_YET();
}
bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) {
if (!find_b_c_check(ab, ac))
return false;
unsigned i = 0, j = 0; // i points to ab, j points to ac
b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul();
nex_pow* bp = ab->begin();
nex_pow* cp = ac->begin();
@ -519,12 +519,30 @@ bool nla_grobner::find_b_c(nex_mul*ab, nex_mul* ac, nex_mul*& b, nex_mul*& c) {
if (++cp == ac->end())
break;
} else {
NOT_IMPLEMENTED_YET();
unsigned b_pow = bp->pow();
unsigned c_pow = cp->pow();
if (b_pow > c_pow) {
b->add_child_in_power(bp->e(), b_pow - c_pow);
} else if (c_pow > b_pow) {
c->add_child_in_power(cp->e(), c_pow - b_pow);
} // otherwise the power are equal and no child added to either b or c
bp++; cp++;
if (bp == ab->end() || cp == ac->end()) {
break;
}
}
}
NOT_IMPLEMENTED_YET();
return true;
while (cp != ac->end()) {
c->add_child_in_power(*cp);
cp++;
}
while (bp != ab->end()) {
b->add_child_in_power(*bp);
bp++;
}
TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";);
}
bool nla_grobner::find_b_c_check(const nex_mul*ab, const nex_mul* ac) const {