mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix order lemma bug see 30ce6f20f2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-15 15:38:55 -07:00
parent 31a96b3afa
commit 90f5595067
2 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1396,7 +1396,7 @@ lbool core::check(vector<lemma>& l_vec) {
set_use_nra_model(false);
if (l_vec.empty() && !done())
if (false && l_vec.empty() && !done())
m_monomial_bounds();
if (l_vec.empty() && !done() && need_to_call_algebraic_methods())

6
src/math/lp/nla_order_lemmas.cpp
View file

@ -213,7 +213,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
tout << "ab.size()=" << ab.size() << "\n";
tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";);
TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
if (mv != fv) {
if (mv != fv && !c().has_real(m)) {
bool gt = mv > fv;
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
new_lemma lemma(_(), __FUNCTION__);
@ -326,8 +326,6 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
lemma b != val(b) || sign*m <= a*val(b)
*/
void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
if (!c().var_is_int(b) && val(b).is_big())
return;
SASSERT(sign * var_val(m) > val(a) * val(b));
// negate b == val(b)
lemma |= ineq(b, llc::NE, val(b));
@ -339,8 +337,6 @@ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rationa
lemma b != val(b) || sign*m >= a*val(b)
*/
void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
if (!c().var_is_int(b) && val(b).is_big())
return;
TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) <<
", b = "; c().print_var(b, tout) << "\n";);
SASSERT(sign * var_val(m) < val(a) * val(b));