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:17:21 +08:00
parent efee734ec9
commit e3ff457af5
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -864,8 +864,8 @@ struct solver::imp {
return false;
}
bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
// we derive a lemma from |x| >= 1 => |xy| >= |y|
bool large_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;
@ -884,7 +884,19 @@ struct solver::imp {
return true;
return false;
}
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))
return true;
return large_basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon);
}
// we derive a lemma from |xy| > |y| => |x| >= 1 || |y| = 0
bool large_basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) {
SASSERT(false);
return false;
}
bool generate_basic_lemma_for_mon(unsigned i_mon) {