mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

rollback but leave the change with llc::NE

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-28 18:30:23 +14:00
parent 649d47d92c
commit 34262ae02c
2 changed files with 36 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -101,7 +101,7 @@ struct solver::imp {
std::unordered_map<unsigned_vector, unsigned, hash_svector> m_mkeys; // the key is the sorted vars of a monomial
unsigned find_monomial(const unsigned_vector& k) const {
TRACE("nla_solver", tout << "k = "; print_product_with_vars(k, tout););
TRACE("nla_solver_find", tout << "k = "; print_product_with_vars(k, tout););
auto it = m_mkeys.find(k);
if (it == m_mkeys.end()) {
TRACE("nla_solver", tout << "not found";);
@ -259,8 +259,7 @@ struct solver::imp {
// return true iff the monomial value is equal to the product of the values of the factors
bool check_monomial(const monomial& m) const {
SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
TRACE("nla_solver_check", tout << "m = "; print_monomial_with_vars(m, tout););
SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
return product_value(m) == m_lar_solver.get_column_value_rational(m.var());
}
@ -354,7 +353,6 @@ struct solver::imp {
print_var(m[k], out);
}
return out;
}
std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const {
@ -792,6 +790,10 @@ struct solver::imp {
return zero_j;
}
static bool is_set(unsigned j) {
return static_cast<int>(j) != -1;
}
bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
SASSERT(sign);
if (has_lower_bound(j) && get_lower_bound(j) >= rational(0))
@ -886,12 +888,14 @@ struct solver::imp {
return m_vars_equivalence.eq_vars(j);
}
void basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n= "; print_monomial_with_vars(n, tout); );
rational contr_sign;
if (sign_contradiction(m, n, contr_sign)) {
generate_sign_lemma(m, n, sign);
return true;
}
return false;
}
void init_abs_val_table() {
@ -967,9 +971,9 @@ struct solver::imp {
for (index_with_sign i_s : mons_to_explore) {
unsigned n = i_s.index();
if (n == i) continue;
basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign());
if(done())
return true;
if (basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign()))
if(done())
return true;
}
TRACE("nla_solver",);
return false;
@ -979,18 +983,16 @@ struct solver::imp {
* \brief <generate lemma by using the fact that -ab = (-a)b) and
-ab = a(-b)
*/
void basic_sign_lemma(bool derived) {
if (!derived) {
basic_sign_lemma_model_based();
} else {
std::unordered_set<unsigned> explored;
for (unsigned i : m_to_refine){
basic_sign_lemma_on_mon(i, explored);
if (done())
return;
}
bool basic_sign_lemma(bool derived) {
if (!derived)
return basic_sign_lemma_model_based();
std::unordered_set<unsigned> explored;
for (unsigned i : m_to_refine){
if (basic_sign_lemma_on_mon(i, explored))
return true;
}
return false;
}
bool var_is_fixed_to_zero(lpvar j) const {
@ -1660,10 +1662,11 @@ struct solver::imp {
unsigned random() {return settings().random_next();}
// use basic multiplication properties to create a lemma
void basic_lemma(bool derived) {
basic_sign_lemma(derived);
bool basic_lemma(bool derived) {
if (basic_sign_lemma(derived))
return true;
if (derived)
return;
return false;
init_rm_to_refine();
const auto& rm_ref = m_rm_table.to_refine();
TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
@ -1677,6 +1680,8 @@ struct solver::imp {
i = 0;
}
} while(i != start && !done());
return false;
}
void map_monomial_vars_to_monomial_indices(unsigned i) {
@ -1707,8 +1712,7 @@ struct solver::imp {
// we look for octagon constraints here, with a left part +-x +- y
void collect_equivs() {
const lp::lar_solver& s = m_lar_solver;
for (unsigned i = 0; i < s.terms().size(); i++) {
unsigned ti = i + s.terms_start_index();
if (!s.term_is_used_as_row(ti))
@ -1719,27 +1723,6 @@ struct solver::imp {
add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
}
}
std::unordered_map<rational, lpvar> fixed_vars;
for (unsigned j = 0; j < s.number_of_vars(); j++) {
if (!var_is_fixed_to_zero(j)) continue;
rational v = abs(vvr(j));
auto it = fixed_vars.find(v);
if (it == fixed_vars.end()){
fixed_vars[v] = j;
} else {
lpvar k = it->second;
TRACE("nla_solver", tout << "fixed vars eq: " << k << ", " << j << ", fixed to " << vvr(j) << "\n";);
add_equivalence_of_two_vars(k, j,
s.get_column_upper_bound_witness(k),
s.get_column_lower_bound_witness(k),
s.get_column_upper_bound_witness(j),
s.get_column_lower_bound_witness(j));
}
}
}
void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) {
@ -1766,11 +1749,6 @@ struct solver::imp {
rational sign((seen_minus && seen_plus)? 1 : -1);
m_vars_equivalence.add_equiv(i, j, sign, c0, c1);
}
void add_equivalence_of_two_vars(lpvar k, lpvar j, lpci c0, lpci c1, lpci c2, lpci c3) {
SASSERT(abs(vvr(k)) == abs(vvr(j)));
rational sign(vvr(k) == vvr(j)? 1 : -1);
m_vars_equivalence.add_equiv(k, j, sign, c0, c1, c2, c3);
}
// x is equivalent to y if x = +- y
void init_vars_equivalence() {
@ -2794,7 +2772,7 @@ struct solver::imp {
if (search_level == 0) {
basic_lemma(derived);
if (!m_lemma_vec->empty())
return l_false;
return l_false;
} else if (search_level == 1) {
order_lemma(derived);
} else { // search_level == 2

35
src/util/lp/vars_equivalence.h
View file

@ -19,8 +19,6 @@
--*/
namespace nla {
bool is_set(unsigned j) { return static_cast<int>(j) != -1; }
typedef lp::constraint_index lpci;
typedef lp::explanation expl_set;
@ -41,24 +39,15 @@ struct vars_equivalence {
rational m_sign;
lpci m_c0;
lpci m_c1;
lpci m_c2;
lpci m_c3;
equiv(lpvar i, lpvar j, rational const& sign,
lpci c0,
lpci c1,
lpci c2,
lpci c3
) :
equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) :
m_i(i),
m_j(j),
m_sign(sign),
m_c0(c0),
m_c1(c1),
m_c2(c2),
m_c3(c3) {
m_c1(c1) {
SASSERT(m_i != m_j);
}
};
struct node {
@ -150,13 +139,9 @@ struct vars_equivalence {
}
void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) {
m_equivs.push_back(equiv(i, j, sign, c0, c1, -1, -1));
m_equivs.push_back(equiv(i, j, sign, c0, c1));
}
void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1, lpci c2, lpci c3) {
m_equivs.push_back(equiv(i, j, sign, c0, c1, c2, c3));
}
void connect_equiv_to_tree(unsigned k) {
// m_tree is the tree with the edges formed by m_equivs
const equiv &e = m_equivs[k];
@ -262,14 +247,8 @@ struct vars_equivalence {
if (it->second.m_parent == static_cast<unsigned>(-1))
return;
const equiv & e = m_equivs[it->second.m_parent];
if (is_set(e.m_c0))
exp.add(e.m_c0);
if (is_set(e.m_c1))
exp.add(e.m_c1);
if (is_set(e.m_c2))
exp.add(e.m_c2);
if (is_set(e.m_c3))
exp.add(e.m_c3);
exp.add(e.m_c0);
exp.add(e.m_c1);
j = get_parent_node(j, e);
}
}