mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

limit the number of tactics in qfnia

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-21 11:20:14 -08:00 • committed by Lev Nachmanson
parent ca0ce579b1
commit e4cbe980e9
2 changed files with 46 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -119,10 +119,10 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
return and_then( return and_then(
mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_report_verbose_tactic("(qfnia-tactic)", 10),
mk_qfnia_preamble(m, p), mk_qfnia_preamble(m, p),
or_else(mk_qfnia_sat_solver(m, p), or_else(mk_qfnia_sat_solver(m, p),
try_for(mk_qfnia_smt_solver(m, p), 2000), try_for(mk_qfnia_smt_solver(m, p), 2000),
mk_qfnia_nlsat_solver(m, p), mk_qfnia_nlsat_solver(m, p),
mk_qfnia_smt_solver(m, p)) mk_qfnia_smt_solver(m, p))
); )
;
} }

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

@ -901,15 +901,52 @@ struct solver::imp {
m_lemma->clear(); m_lemma->clear();
} }
static svector<lpvar> extract_all_but(const svector<lpvar> & vars, unsigned k) {
static svector<lpvar> ret;
for (unsigned j = 0; j < vars.size(); j++) {
if (j == k)
continue;
ret.push_back(vars[j]);
}
return ret;
}
// a > b && c == d => ac > bd // a > b && c == d => ac > bd
// ac is a factorization of m_monomials[i_mon] // ac is a factorization of m_monomials[i_mon]
// ac[k] plays the role of c // ac[k] plays the role of c
// d = +-c // d = +-c
// i_bd_equiv is a candidate for bd
bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned b,
unsigned i_bd_equiv,
unsigned i_bd,
unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
}
bool order_lemma_on_factor_equiv_and_other_mon_factor(unsigned i_f,
unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k) { // a > b && c == d => ac > bd
TRACE("nla_solver", tout << "i_f = "; print_monomial_with_vars(i_f, tout); ); // ac is a factorization of m_monomials[i_mon]
NOT_IMPLEMENTED_YET(); // ac[k] plays the role of c
// d = +-c
// i_bd_equiv is a candidate for bd
bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned i_bd_equiv,
unsigned i_bd,
unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
TRACE("nla_solver", tout << "i_bd_equiv = "; print_monomial_with_vars(i_bd_equiv, tout); );
rational abs_d = abs(vvr(d));
for (unsigned k = 0; k < m_monomials[i_bd_equiv].size(); k++) {
if (abs(vvr(m_monomials[i_bd_equiv][k])) != abs_d)
continue;
svector<lpvar> b = extract_all_but(m_monomials[i_bd_equiv].vars(), k);
std::sort(b.begin(), b.end());
auto it = m_rooted_monomials_map.find(b);
if (it == m_rooted_monomials_map.end())
return false;
for (const index_with_sign& s : it->second) {
if (order_lemma_on_factor_equiv_and_other_mon_eq_b(s.var(), i_bd, d, i_bd, d, i_ac, ac, k))
return true;
}
}
return false; return false;
} }
@ -922,16 +959,15 @@ struct solver::imp {
if (i_bd == i_ac) { if (i_bd == i_ac) {
return false; return false;
} }
TRACE("nla_solver", );
const monomial & m_bd = m_monomials[i_bd]; const monomial & m_bd = m_monomials[i_bd];
monomial_coeff m_bd_rooted = canonize_monomial(m_bd); monomial_coeff m_bd_rooted = canonize_monomial(m_bd);
TRACE("nla_solver", tout << "i_bd monomial = "; print_monomial(m_bd, tout); ); TRACE("nla_solver", tout << "i_bd monomial = "; print_monomial(m_bd, tout); );
TRACE("nla_solver", );
auto it = m_rooted_monomials_map.find(m_bd_rooted.vars()); auto it = m_rooted_monomials_map.find(m_bd_rooted.vars());
if (it == m_rooted_monomials_map.end()) if (it == m_rooted_monomials_map.end())
return false; return false;
for (const index_with_sign& i_s : it->second) { for (const index_with_sign& s : it->second) {
if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), i_bd, d, i_ac, ac, k)) if (order_lemma_on_factor_equiv_and_other_mon_eq(s.var(), i_bd, d, i_ac, ac, k))
return true; return true;
} }
return false; return false;