mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fixes in order lemmas and printing terms

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-23 11:18:56 -07:00
parent 4b8a063996
commit 38eca3b66a
9 changed files with 83 additions and 89 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -289,7 +289,7 @@ public:
lia_move cut() {
TRACE("gomory_cut", dump(tout););
// gomory will be t <= k and the current solution has a property t > k
// gomory will be t >= k and the current solution has a property t < k
m_k = 1;
m_t.clear();
mpq m_lcm_den(1);

4
src/math/lp/lar_solver.cpp
View file

@ -60,7 +60,7 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr
out << "implied bound\n";
unsigned v = be.m_j;
if (tv::is_term(v)) {
out << "it is a term number " << be.m_j << std::endl;
out << "it is a term number " << tv::unmask_term(be.m_j) << std::endl;
print_term(*m_terms[tv::unmask_term(v)], out);
}
else {
@ -1259,7 +1259,7 @@ void lar_solver::set_variable_name(var_index vi, std::string name) {
std::string lar_solver::get_variable_name(var_index j) const {
if (tv::is_term(j))
return std::string("_t") + T_to_string(j);
return std::string("_t") + T_to_string(tv::unmask_term(j));
if (j >= m_var_register.size())
return std::string("_s") + T_to_string(j);

9
src/math/lp/lp_utils.h
View file

@ -20,6 +20,7 @@ Revision History:
#pragma once
#include <string>
#include "math/lp/numeric_pair.h"
#include "math/lp/lp_types.h"
#include "util/debug.h"
#include <unordered_map>
#include <unordered_set>
@ -115,7 +116,13 @@ template <typename T>
std::ostream& print_linear_combination_of_column_indices_only(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) {
return print_linear_combination_customized(
coeffs,
[](unsigned j) {std::stringstream ss; ss << "v" << j; return ss.str();},
[](unsigned j) {std::stringstream ss;
if (tv::is_term(j)) {
ss << "t" << tv::unmask_term(j);
} else {
ss << "v" << j;
}
return ss.str();},
out);
}
template <typename T, typename K>

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

@ -1027,6 +1027,15 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const {
return true;
}
void core::negate_var_relation_strictly(lpvar a, lpvar b) {
SASSERT(val(a) != val(b));
if (val(a) < val(b)) {
mk_ineq(a, -rational(1), b, llc::GT);
} else {
mk_ineq(a, -rational(1), b, llc::LT);
}
}
void core::negate_factor_equality(const factor& c,
const factor& d) {
if (c == d)

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

@ -363,6 +363,8 @@ public:
void negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
void negate_var_relation_strictly(lpvar a, lpvar b);
std::unordered_set<lpvar> collect_vars(const lemma& l) const;
bool rm_check(const monic&) const;

44
src/math/lp/nla_monotone_lemmas.cpp
View file

@ -32,50 +32,6 @@ void monotone::monotonicity_lemma() {
monotonicity_lemma(c().emons()[v]);
}
}
void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
rational av = val(a);
rational as = rational(nla::rat_sign(av));
rational bv = val(b);
rational bs = rational(nla::rat_sign(bv));
TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
SASSERT(as*av <= bs*bv);
llc mod_s = strict? (llc::LE): (llc::LT);
mk_ineq(as, a, mod_s); // |a| <= 0 || |a| < 0
if (a != b) {
mk_ineq(bs, b, mod_s); // |b| <= 0 || |b| < 0
mk_ineq(as, a, -bs, b, llc::GT); // negate |aj| <= |bj|
}
}
void monotone::assert_abs_val_a_le_abs_var_b(
const monic& a,
const monic& b,
bool strict) {
lpvar aj = var(a);
lpvar bj = var(b);
rational av = val(aj);
rational as = rational(nla::rat_sign(av));
rational bv = val(bj);
rational bs = rational(nla::rat_sign(bv));
// TRACE("nla_solver", tout << "rmv = " << rmv << ", jv = " << jv << "\n";);
mk_ineq(as, aj, llc::LT); // |aj| < 0
mk_ineq(bs, bj, llc::LT); // |bj| < 0
mk_ineq(as, aj, -bs, bj, strict? llc::LT : llc::LE); // |aj| < |bj|
}
void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
rational av = val(a);
rational as = rational(nla::rat_sign(av));
rational bv = val(b);
rational bs = rational(nla::rat_sign(bv));
TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";);
SASSERT(as*av < bs*bv);
mk_ineq(as, a, llc::LT); // |aj| < 0
mk_ineq(bs, b, llc::LT); // |bj| < 0
mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj|
}
void monotone::monotonicity_lemma(monic const& m) {
SASSERT(!check_monic(m));

3
src/math/lp/nla_monotone_lemmas.h
View file

@ -30,8 +30,5 @@ private:
void monotonicity_lemma_lt(const monic& m, const rational& prod_val);
std::vector<rational> get_sorted_key(const monic& rm) const;
vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
void negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict);
void negate_abs_a_lt_abs_b(lpvar a, lpvar b);
void assert_abs_val_a_le_abs_var_b(const monic& a, const monic& b, bool strict);
};
}

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

@ -255,20 +255,12 @@ bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac,
return false;
}
// |c_sign| = 1, and c*c_sign > 0
// ac > bc && ac/|c| > bc/|c| => a*c_sign > b*c_sign
void order::generate_ol(const monic& ac,
const factor& a,
int c_sign,
const factor& c,
const monic& bc,
const factor& b,
llc ab_cmp) {
rational rc_sign = rational(c_sign);
rational sign_a = rc_sign * sign_to_rat(canonize_sign(a));
rational sign_b = rc_sign * sign_to_rat(canonize_sign(b));
rational sign_c = rc_sign * sign_to_rat(canonize_sign(c));
void order::generate_ol_eq(const monic& ac,
const factor& a,
const factor& c,
const monic& bc,
const factor& b) {
add_empty_lemma();
#if 0
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
@ -276,10 +268,11 @@ void order::generate_ol(const monic& ac,
<< " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n"
<< " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n"
<< " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n");
#endif
mk_ineq(sign_c, var(c), llc::LE);
mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
mk_ineq(sign_a, var(a), - sign_b, var(b), negate(ab_cmp));
#endif
// ac == bc
mk_ineq(c.var(),llc::EQ); // c is not equal to zero
mk_ineq(ac.var(), -rational(1), bc.var(), llc::NE);
mk_ineq(canonize_sign(a), a.var(), !canonize_sign(b), b.var(), llc::EQ);
explain(ac);
explain(a);
explain(bc);
@ -288,27 +281,54 @@ void order::generate_ol(const monic& ac,
TRACE("nla_solver", _().print_lemma(tout););
}
void order::generate_ol(const monic& ac,
const factor& a,
const factor& c,
const monic& bc,
const factor& b) {
add_empty_lemma();
#if 0
IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac
<< " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
<< " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n"
<< " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n"
<< " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n");
#endif
// fix the sign of c
_().negate_relation(c.var(), rational(0));
_().negate_var_relation_strictly(ac.var(), bc.var());
_().negate_var_relation_strictly(a.var(), b.var());
explain(ac);
explain(a);
explain(bc);
explain(b);
explain(c);
TRACE("nla_solver", _().print_lemma(tout););
}
// We have ac = a*c and bc = b*c.
// Suppose ac >= bc, then ac/|c| >= bc/|b|
// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.//
bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
const factor& a,
const factor& c,
const monic& bc,
const factor& b) {
auto cv = val(c);
int c_sign = nla::rat_sign(cv);
SASSERT(c_sign != 0);
auto av_c_s = val(a)*rational(c_sign);
auto bv_c_s = val(b)*rational(c_sign);
auto acv = var_val(ac);
auto bcv = var_val(bc);
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
// Suppose ac >= bc, then ac/|c| >= bc/|c|.
// Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s
if (acv >= bcv && av_c_s < bv_c_s) {
generate_ol(ac, a, c_sign, c, bc, b, llc::LT);
return true;
} else if (acv <= bcv && av_c_s > bv_c_s) {
generate_ol(ac, a, c_sign, c, bc, b, llc::GT);
SASSERT(!val(c).is_zero());
rational c_sign = rational(nla::rat_sign(val(c)));
auto av_c_s = val(a) * c_sign;
auto bv_c_s = val(b) * c_sign;
if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s)
||
(var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) {
TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
generate_ol(ac, a, c, bc, b);
return true;
} else {
if((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) {
generate_ol_eq(ac, a, c, bc, b);
}
}
return false;
}

13
src/math/lp/nla_order_lemmas.h
View file

@ -68,15 +68,18 @@ private:
void order_lemma_on_binomial_sign(const monic& ac, lpvar x, lpvar y, int sign);
void order_lemma_on_binomial(const monic& ac);
void order_lemma_on_monic(const monic& rm);
// |c_sign| = 1, and c*c_sign > 0
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
void generate_ol(const monic& ac,
const factor& a,
int c_sign,
const factor& c,
const monic& bc,
const factor& b,
llc ab_cmp);
const factor& b);
void generate_ol_eq(const monic& ac,
const factor& a,
const factor& c,
const monic& bc,
const factor& b);
void generate_mon_ol(const monic& ac,
lpvar a,