mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

start switching to rooted monomials if there is no sign lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-25 16:12:26 -08:00 committed by Lev Nachmanson
parent 2d144cd774
commit 667d1be8c3
2 changed files with 59 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,6 +28,13 @@ namespace nla {
struct solver::imp {
struct rooted_mon {
svector<lpvar> m_vars;
index_with_sign m_orig;
rooted_mon(const svector<lpvar>& vars, unsigned i, const rational& sign): m_vars(vars), m_orig(i, sign) {}
};
typedef lp::lar_base_constraint lpcon;
@ -40,7 +47,7 @@ struct solver::imp {
vector<index_with_sign>,
hash_svector>
m_rooted_monomials_map;
vector<svector<lpvar>> m_vector_of_rooted_monomials;
vector<rooted_mon> m_vector_of_rooted_monomials;
// this field is used for the push/pop operations
unsigned_vector m_monomials_counts;
@ -695,7 +702,8 @@ struct solver::imp {
// use basic multiplication properties to create a lemma
// for the given monomial
bool basic_lemma_for_mon(unsigned i_mon) {
bool basic_lemma_for_mon(const rooted_mon& rm) {
/*
for (auto factorization : factorization_factory_imp(i_mon, *this)) {
if (factorization.is_empty())
continue;
@ -703,17 +711,19 @@ struct solver::imp {
basic_lemma_for_mon_neutral(i_mon, factorization))
return true;
}
}*/
return false;
}
// use basic multiplication properties to create a lemma
bool basic_lemma(unsigned_vector & to_refine) {
bool basic_lemma() {
if (basic_sign_lemma())
return true;
for (unsigned i : to_refine) {
if (basic_lemma_for_mon(i)) {
for (const rooted_mon& r : m_vector_of_rooted_monomials) {
if (check_monomial(m_monomials[r.m_orig.m_i]))
continue;
if (basic_lemma_for_mon(r)) {
return true;
}
}
@ -791,7 +801,19 @@ struct solver::imp {
}
}
bool var_is_a_root(lpvar j) const { return m_vars_equivalence.is_root(j); }
template <typename T>
bool vars_are_roots(const T& v) const {
for (lpvar j: v) {
if (!var_is_a_root(j))
return false;
}
return true;
}
void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i) {
SASSERT(vars_are_roots(mc.vars()));
index_with_sign ms(i, mc.coeff());
auto it = m_rooted_monomials_map.find(mc.vars());
if (it == m_rooted_monomials_map.end()) {
@ -799,6 +821,7 @@ struct solver::imp {
v.push_back(ms);
// v is a vector containing a single index_with_sign
m_rooted_monomials_map.emplace(mc.vars(), v);
m_vector_of_rooted_monomials.push_back(rooted_mon(mc.vars(), i, mc.coeff()));
}
else {
it->second.push_back(ms);
@ -811,33 +834,6 @@ struct solver::imp {
register_key_mono_in_rooted_monomials(mc, i);
}
void fill_vector_of_rooted_monomials() {
SASSERT(m_vector_of_rooted_monomials.empty());
for (const auto& p : m_rooted_monomials_map) {
m_vector_of_rooted_monomials.push_back(p.first);
}
}
void register_rooted_monomial(unsigned i) {
for (unsigned j : m_vector_of_rooted_monomials[i]) {
auto it = m_rooted_monomials_containing_var.find(j);
if (it == m_rooted_monomials_containing_var.end()) {
std::unordered_set<unsigned> s;
s.insert(i);
m_rooted_monomials_containing_var[j] = s;
} else {
it->second.insert(i);
}
}
}
void create_rooted_tables() {
fill_vector_of_rooted_monomials();
for (unsigned i = 0; i < m_vector_of_rooted_monomials.size(); i++) {
register_rooted_monomial(i);
}
}
void intersect_set(std::unordered_set<unsigned>& p, const std::unordered_set<unsigned>& w) {
for (auto it = p.begin(); it != p.end(); ) {
auto iit = it;
@ -875,27 +871,30 @@ struct solver::imp {
void reduce_set_by_checking_actual_containment(std::unordered_set<unsigned>& p,
const svector<lpvar> & rm ) {
for (auto it = p.begin(); it != p.end();) {
if (is_factor(rm, m_vector_of_rooted_monomials[*it])) {
it++;
continue;
}
auto iit = it;
iit ++;
p.erase(it);
it = iit;
}
NOT_IMPLEMENTED_YET();
// for (auto it = p.begin(); it != p.end();) {
// if (is_factor(rm, m_vector_of_rooted_monomials[*it])) {
// it++;
// continue;
// }
// auto iit = it;
// iit ++;
// p.erase(it);
// it = iit;
// }
}
// here i is the index of a monomial in m_vector_of_rooted_monomials
void find_containing_rooted_monomials(unsigned i) {
const svector<lpvar> & rm = m_vector_of_rooted_monomials[i];
std::unordered_set<unsigned> p = m_rooted_monomials_containing_var[rm[0]];
for (unsigned k = 1; k < rm.size(); k++) {
intersect_set(p, m_rooted_monomials_containing_var[rm[k]]);
}
reduce_set_by_checking_actual_containment(p, rm);
m_rooted_factor_to_product[i] = p;
NOT_IMPLEMENTED_YET();
// const svector<lpvar> & rm = m_vector_of_rooted_monomials[i];
// std::unordered_set<unsigned> p = m_rooted_monomials_containing_var[rm[0]];
// for (unsigned k = 1; k < rm.size(); k++) {
// intersect_set(p, m_rooted_monomials_containing_var[rm[k]]);
// }
// reduce_set_by_checking_actual_containment(p, rm);
// m_rooted_factor_to_product[i] = p;
}
void fill_rooted_factor_to_product() {
@ -909,7 +908,6 @@ struct solver::imp {
for (unsigned i = 0; i < m_monomials.size(); i++)
register_monomial_in_tables(i);
create_rooted_tables();
fill_rooted_factor_to_product();
}
@ -1102,22 +1100,20 @@ struct solver::imp {
return l_undef;
}
unsigned_vector to_refine;
for (unsigned i = 0; i < m_monomials.size(); i++) {
bool to_refine = false;
for (unsigned i = 0; i < m_monomials.size() && !to_refine; i++) {
if (!check_monomial(m_monomials[i]))
to_refine.push_back(i);
to_refine = true;
}
if (to_refine.empty()) {
if (!to_refine) {
return l_true;
}
TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);
init_search();
for (int search_level = 0; search_level < 3; search_level++) {
if (search_level == 0) {
if (basic_lemma(to_refine)) {
if (basic_lemma()) {
return l_false;
}
} else if (search_level == 1) {

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

@ -76,16 +76,16 @@ struct vars_equivalence {
// The map from the variables to m_equivs indices
// m_tree is a spanning tree of the graph of equivs represented by m_equivs
std::unordered_map<unsigned, unsigned> m_tree;
std::unordered_map<unsigned, unsigned> m_tree;
// If m_tree[v] == -1 then the variable is a root.
// if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), that k is the parent of v
vector<equiv> m_equivs; // all equivalences extracted from constraints
std::unordered_map<rational,unsigned_vector> m_vars_by_abs_values;
vector<equiv> m_equivs; // all equivalences extracted from constraints
std::unordered_map<rational, unsigned_vector> m_vars_by_abs_values;
std::unordered_map<vector<rational>,
unsigned_vector,
hash_vector> m_monomials_by_abs_vals;
hash_vector> m_monomials_by_abs_vals;
std::function<rational(lpvar)> m_vvr;
std::function<rational(lpvar)> m_vvr;
// constructor