mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-03 19:52:06 -08:00 • committed by Lev Nachmanson
parent cebee656bd
commit fc277f5648
2 changed files with 34 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/lp/factorization.h
View file

@ -18,6 +18,7 @@
--*/
#pragma once
#include "util/rational.h"
#include "util/lp/monomial.h"
@ -41,6 +42,15 @@ public:
bool is_var() const { return m_type == factor_type::VAR; }
};
inline bool operator==(const factor& a, const factor& b) {
return a.index() == b.index() && a.type() == b.type();
}
inline bool operator!=(const factor& a, const factor& b) {
return ! (a == b);
}
class factorization {
vector<factor> m_vars;
public:

33
src/util/lp/nla_solver.cpp
View file

@ -1034,16 +1034,31 @@ struct solver::imp {
return true;
}
void generate_ol() {
NOT_IMPLEMENTED_YET();
void generate_ol(const rooted_mon& ac,
const factor& a,
const factor& c,
const rooted_mon& bd,
const factor& b,
const factor& d) {
if (c != d) {
lpvar i = var(c);
lpvar j = var(d);
auto iv = vvr(i), jv = vvr(j);
SASSERT(abs(iv) == abs(jv));
if (iv == jv) {
mk_ineq(i, -rational(1), j, lp::lconstraint_kind::NE);
} else { // iv == -jv
mk_ineq(i, j, lp::lconstraint_kind::NE);
}
}
}
bool order_lemma_on_ac_and_bd_and_factors(const rooted_mon& ac,
const factor& a,
const factor& c,
const rooted_mon& bd,
const factor& b,
const factor& d) {
const factor& a,
const factor& c,
const rooted_mon& bd,
const factor& b,
const factor& d) {
auto ac_m = vvr(a) * vvr(c);
auto bd_m = vvr(b) * vvr(d);
@ -1052,11 +1067,11 @@ struct solver::imp {
auto bd_v = vvr(bd);
if (ac_m < bd_m && !(ac_v < bd_v)) {
generate_ol();
generate_ol(ac, a, c, bd, b, d);
return true;
}
else if (ac_m > bd_m && !(ac_v > bd_v)) {
generate_ol();
generate_ol(ac, a, c, bd, b, d);
return true;
}