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

use m_rm_table.to_refine() when applying tangent lemma

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-23 08:09:30 -10:00
parent 1507f54fe3
commit 8018e27643
2 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/main.cpp
View file

@ -301,7 +301,7 @@ static void parse_cmd_line_args(int argc, char ** argv) {
int STD_CALL main(int argc, char ** argv) {
#ifdef DUMP_ARGS
#ifdef DUMP_ARGS_
std::cout << "args are: ";
for (int i = 0; i < argc; i++)
std::cout << argv[i] <<" ";

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

@ -2554,10 +2554,9 @@ struct solver::imp {
}
bool find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_mon*& rm_found){
// todo : run on m_rm_table.to_refine()
for (const auto& rm : m_rm_table.vec()) {
if (check_monomial(m_monomials[rm.orig_index()]))
continue;
for (unsigned i: m_rm_table.to_refine()) {
const auto& rm = m_rm_table.vec()[i];
SASSERT (!check_monomial(m_monomials[rm.orig_index()]));
rm_found = &rm;
if (find_bfc_on_monomial(rm, bf)) {
j = m_monomials[rm.orig_index()].var();
@ -2567,7 +2566,6 @@ struct solver::imp {
print_bfc(bf, tout);
tout << ", product = " << vvr(rm) << ", but should be =" << vvr(bf.m_x)*vvr(bf.m_y);
tout << ", j == "; print_var(j, tout) << "\n";);
rm_found = &rm;
return true;
}
}