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

start on test nla

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-09 11:28:08 -07:00 committed by Lev Nachmanson
parent 095fdae457
commit 0a86bd14f7
3 changed files with 31 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/test/lp/lp.cpp
View file

@ -1896,7 +1896,7 @@ void test_replace_column() {
void setup_args_parser(argument_parser & parser) { void setup_args_parser(argument_parser & parser) {
parser.add_option_with_help_string("-nla", "test nla_solver"); parser.add_option_with_help_string("-nla_fact", "test nla_solver");
parser.add_option_with_help_string("-hnf", "test hermite normal form"); parser.add_option_with_help_string("-hnf", "test hermite normal form");
parser.add_option_with_help_string("-gomory", "gomory"); parser.add_option_with_help_string("-gomory", "gomory");
parser.add_option_with_help_string("-intd", "test integer_domain"); parser.add_option_with_help_string("-intd", "test integer_domain");
@ -3548,8 +3548,8 @@ void test_gomory_cut() {
test_gomory_cut_1(); test_gomory_cut_1();
} }
void test_nla() { void test_nla_factorization() {
nla::solver::test(); nla::solver::test_factorization();
} }
void test_lp_local(int argn, char**argv) { void test_lp_local(int argn, char**argv) {
@ -3568,9 +3568,9 @@ void test_lp_local(int argn, char**argv) {
args_parser.print(); args_parser.print();
if (args_parser.option_is_used("-nla")) { if (args_parser.option_is_used("-nla_fact")) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
test_nla(); test_nla_factorization();
#endif #endif
return finalize(0); return finalize(0);
} }

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

@ -38,13 +38,16 @@ struct solver::imp {
}; };
vars_equivalence m_vars_equivalence; vars_equivalence m_vars_equivalence;
vector<monomial> m_monomials; vector<monomial> m_monomials;
// maps the vector of the rooted monomial vars to the list of the indices of monomials having the same rooted monomial // maps the vector of the rooted monomial vars to the list of the indices of monomials having the same rooted monomial
std::unordered_map<svector<lpvar>, vector<mono_index_with_sign>, hash_svector> std::unordered_map<svector<lpvar>,
m_rooted_monomials; vector<mono_index_with_sign>,
unsigned_vector m_monomials_lim; hash_svector>
m_rooted_monomials;
// this field is used for push/pop operations
unsigned_vector m_monomials_counts;
lp::lar_solver& m_lar_solver; lp::lar_solver& m_lar_solver;
std::unordered_map<lpvar, unsigned_vector> m_var_containing_monomials; std::unordered_map<lpvar, unsigned_vector> m_monomials_containing_var;
// monomial.var() -> monomial index // monomial.var() -> monomial index
u_map<unsigned> m_var_to_its_monomial; u_map<unsigned> m_var_to_its_monomial;
@ -67,16 +70,16 @@ struct solver::imp {
} }
void push() { void push() {
m_monomials_lim.push_back(m_monomials.size()); m_monomials_counts.push_back(m_monomials.size());
} }
void pop(unsigned n) { void pop(unsigned n) {
if (n == 0) return; if (n == 0) return;
m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]); m_monomials.shrink(m_monomials_counts[m_monomials_counts.size() - n]);
m_monomials_lim.shrink(m_monomials_lim.size() - n); m_monomials_counts.shrink(m_monomials_counts.size() - n);
} }
// make sure that the monomial value is the product of the values of the factors // return true if the monomial value is equal to the product of the values of the factors
bool check_monomial(const monomial& m) { bool check_monomial(const monomial& m) {
SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
const rational & model_val = m_lar_solver.get_column_value_rational(m.var()); const rational & model_val = m_lar_solver.get_column_value_rational(m.var());
@ -147,8 +150,9 @@ struct solver::imp {
} }
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus. // Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
// Also sorts the result.
// //
svector<lpvar> reduce_monomial_to_canonical(const svector<lpvar> & vars, rational & sign) const { svector<lpvar> reduce_monomial_to_rooted(const svector<lpvar> & vars, rational & sign) const {
svector<lpvar> ret; svector<lpvar> ret;
sign = 1; sign = 1;
for (lpvar v : vars) { for (lpvar v : vars) {
@ -167,7 +171,7 @@ struct solver::imp {
// //
monomial_coeff canonize_monomial(monomial const& m) const { monomial_coeff canonize_monomial(monomial const& m) const {
rational sign = rational(1); rational sign = rational(1);
svector<lpvar> vars = reduce_monomial_to_canonical(m.vars(), sign); svector<lpvar> vars = reduce_monomial_to_rooted(m.vars(), sign);
return monomial_coeff(m.var(), vars, sign); return monomial_coeff(m.var(), vars, sign);
} }
@ -226,7 +230,7 @@ struct solver::imp {
// otherwise it remains false // otherwise it remains false
// Returns 2 if the sign is not defined. // Returns 2 if the sign is not defined.
int get_mon_sign_zero_var(unsigned j, bool & strict) { int get_mon_sign_zero_var(unsigned j, bool & strict) {
if (m_var_containing_monomials.find(j) == m_var_containing_monomials.end()) if (m_monomials_containing_var.find(j) == m_monomials_containing_var.end())
return 2; return 2;
lpci lci = -1; lpci lci = -1;
lpci uci = -1; lpci uci = -1;
@ -518,7 +522,7 @@ struct solver::imp {
bool basic_lemma_for_mon_neutral(unsigned i_mon) { bool basic_lemma_for_mon_neutral(unsigned i_mon) {
const monomial & m = m_monomials[i_mon]; const monomial & m = m_monomials[i_mon];
rational sign; rational sign;
svector<lpvar> reduced_vars = reduce_monomial_to_canonical(m.vars(), sign); svector<lpvar> reduced_vars = reduce_monomial_to_rooted(m.vars(), sign);
rational v = m_lar_solver.get_column_value_rational(m.var()); rational v = m_lar_solver.get_column_value_rational(m.var());
if (sign == -1) if (sign == -1)
v = -v; v = -v;
@ -753,7 +757,7 @@ struct solver::imp {
svector<bool> mask(large.size(), false); // init mask by false svector<bool> mask(large.size(), false); // init mask by false
const auto & m = m_monomials[i_mon]; const auto & m = m_monomials[i_mon];
rational sign; rational sign;
auto vars = reduce_monomial_to_canonical(m.vars(), sign); auto vars = reduce_monomial_to_rooted(m.vars(), sign);
auto vars_copy = vars; auto vars_copy = vars;
auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var()));
// We cross out from vars the "large" variables represented by the mask // We cross out from vars the "large" variables represented by the mask
@ -784,7 +788,7 @@ struct solver::imp {
svector<bool> mask(_small.size(), false); // init mask by false svector<bool> mask(_small.size(), false); // init mask by false
const auto & m = m_monomials[i_mon]; const auto & m = m_monomials[i_mon];
rational sign; rational sign;
auto vars = reduce_monomial_to_canonical(m.vars(), sign); auto vars = reduce_monomial_to_rooted(m.vars(), sign);
auto vars_copy = vars; auto vars_copy = vars;
auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var()));
// We cross out from vars the "large" variables represented by the mask // We cross out from vars the "large" variables represented by the mask
@ -1114,11 +1118,11 @@ struct solver::imp {
void map_monomial_vars_to_monomial_indices(unsigned i) { void map_monomial_vars_to_monomial_indices(unsigned i) {
const monomial& m = m_monomials[i]; const monomial& m = m_monomials[i];
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
auto it = m_var_containing_monomials.find(j); auto it = m_monomials_containing_var.find(j);
if (it == m_var_containing_monomials.end()) { if (it == m_monomials_containing_var.end()) {
unsigned_vector v; unsigned_vector ms;
v.push_back(i); ms.push_back(i);
m_var_containing_monomials[j] = v; m_monomials_containing_var[j] = ms;
} }
else { else {
it->second.push_back(i); it->second.push_back(i);
@ -1289,7 +1293,7 @@ solver::~solver() {
dealloc(m_imp); dealloc(m_imp);
} }
void solver::test() { void solver::test_factorization() {
lp::lar_solver s; lp::lar_solver s;
unsigned a = 0, b = 1, c = 2, d = 3, e = 4, unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9; abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;

2
src/util/lp/nla_solver.h
View file

@ -46,6 +46,6 @@ public:
void pop(unsigned scopes); void pop(unsigned scopes);
bool need_check(); bool need_check();
lbool check(lp::explanation&, lemma&); lbool check(lp::explanation&, lemma&);
static void test(); static void test_factorization();
}; };
} }