mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

work on niil_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-29 14:24:45 +08:00
parent e3ff457af5
commit ee6e21c614
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/niil_solver.cpp
View file

@ -865,7 +865,7 @@ struct solver::imp {
}
// we derive a lemma from |x| >= 1 => |xy| >= |y|
bool large_basic_lemma_for_mon_proportionality_from_factors_to_product(unsigned i_mon) {
bool basic_lemma_for_mon_proportionality_from_factors_to_product(unsigned i_mon) {
const mon_eq & m = m_monomials[i_mon];
svector<unsigned> large;
svector<unsigned> _small;
@ -888,7 +888,7 @@ struct solver::imp {
bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
if (large_basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon))
if (basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon))
return true;
return large_basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon);