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

debug refactor of smon

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-23 10:43:05 -07:00
parent 53cc8048f7
commit 9411911cf3
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -575,7 +575,7 @@ public:
} }
std::ostream& print_column_info(unsigned j, std::ostream & out) const { std::ostream& print_column_info(unsigned j, std::ostream & out) const {
out << "j = " << j << ",\tname = "<< column_name(j) << "\t"; out << "[" << j << "],\tname = "<< column_name(j) << "\t";
switch (m_column_types[j]) { switch (m_column_types[j]) {
case column_type::fixed: case column_type::fixed:
case column_type::boxed: case column_type::boxed:

10
src/util/lp/nla_basics_lemmas.cpp
View file

@ -57,7 +57,7 @@ void basics::generate_zero_lemmas(const monomial& m) {
TRACE("nla_solver_details", tout << "zero_j = " << zero_j << ", sign = " << sign << "\n";); TRACE("nla_solver_details", tout << "zero_j = " << zero_j << ", sign = " << sign << "\n";);
if (sign == 0) { // have to generate a non-convex lemma if (sign == 0) { // have to generate a non-convex lemma
add_trival_zero_lemma(zero_j, m); add_trival_zero_lemma(zero_j, m);
} else { } else { // here we know the sign of zero_j
generate_strict_case_zero_lemma(m, zero_j, sign); generate_strict_case_zero_lemma(m, zero_j, sign);
} }
for (lpvar j : fixed_zeros) for (lpvar j : fixed_zeros)
@ -88,7 +88,7 @@ void basics::get_non_strict_sign(lpvar j, int& sign) const {
void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) { void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
if (product_sign == 0) { if (product_sign == 0) {
TRACE("nla_solver_bl", tout << "zero product sign\n";); TRACE("nla_solver_bl", tout << "zero product sign: " << pp_mon(_(), m)<< "\n"; );
generate_zero_lemmas(m); generate_zero_lemmas(m);
} else { } else {
add_empty_lemma(); add_empty_lemma();
@ -188,7 +188,7 @@ void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j,
// we know all the signs // we know all the signs
add_empty_lemma(); add_empty_lemma();
c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT)); c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
for (unsigned j : m.rvars()){ for (unsigned j : m.vars()){
if (j != zero_j) { if (j != zero_j) {
negate_strict_sign(j); negate_strict_sign(j);
} }
@ -203,7 +203,7 @@ void basics::add_fixed_zero_lemma(const monomial& m, lpvar j) {
TRACE("nla_solver", c().print_lemma(tout);); TRACE("nla_solver", c().print_lemma(tout););
} }
void basics::negate_strict_sign(lpvar j) { void basics::negate_strict_sign(lpvar j) {
TRACE("nla_solver_details", c().print_var(j, tout);); TRACE("nla_solver_details", tout << pp_var(c(), j) << "\n";);
if (!vvr(j).is_zero()) { if (!vvr(j).is_zero()) {
int sign = nla::rat_sign(vvr(j)); int sign = nla::rat_sign(vvr(j));
c().mk_ineq(j, (sign == 1? llc::LE : llc::GE)); c().mk_ineq(j, (sign == 1? llc::LE : llc::GE));
@ -494,7 +494,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monomial& rm, const fact
} }
void basics::basic_lemma_for_mon_model_based(const monomial& rm) { void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
TRACE("nla_solver_bl", tout << "rm = " << rm;); TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
if (vvr(rm).is_zero()) { if (vvr(rm).is_zero()) {
for (auto factorization : factorization_factory_imp(rm, c())) { for (auto factorization : factorization_factory_imp(rm, c())) {
if (factorization.is_empty()) if (factorization.is_empty())

2
src/util/lp/nla_order_lemmas.cpp
View file

@ -108,7 +108,7 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) { void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
TRACE("nla_solver", TRACE("nla_solver",
tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";); tout << "ac=" << pp_mon(_(), ac) << "\nrm= " << pp_mon(_(), bd) << ", b= " << pp_fac(_(), b) << ", d= " << pp_var(_(), d) << "\n";);
bool p = !k; bool p = !k;
lpvar a = ac.vars()[p]; lpvar a = ac.vars()[p];
lpvar c = ac.vars()[k]; lpvar c = ac.vars()[k];