mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

port Grobner: do not derive intervals from common

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-28 14:29:51 -07:00
parent 738165f0e7
commit 033d8a332f
3 changed files with 20 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_grobner.cpp
View file

@ -21,13 +21,11 @@
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h" #include "math/lp/factorization_factory_imp.h"
namespace nla { namespace nla {
nla_grobner::nla_grobner(core *c nla_grobner::nla_grobner(core *c)
) : : common(c),
common(c),
m_nl_gb_exhausted(false), m_nl_gb_exhausted(false),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
m_changed_leading_term(false) m_changed_leading_term(false) {}
{}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed, // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue // then assert bounds for x, and continue
@ -301,7 +299,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j); simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
} }
target->exp() = m_nex_creator.simplify(targ_sum); target->exp() = m_nex_creator.simplify(targ_sum);
target->dep = m_dep_manager.mk_join(source->dep, target->dep); target->dep() = m_dep_manager.mk_join(source->dep(), target->dep());
TRACE("grobner", tout << "target = "; display_equation(tout, *target);); TRACE("grobner", tout << "target = "; display_equation(tout, *target););
return true; return true;
} }

12
src/math/lp/nla_intervals.cpp
View file

@ -113,24 +113,24 @@ bool intervals::check_interval_for_conflict_on_zero_upper(
if (!separated_from_zero_on_upper(i)) if (!separated_from_zero_on_upper(i))
return false; return false;
add_empty_lemma(); m_core->add_empty_lemma();
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
dep = m_dep_manager.mk_join(dep, i.m_upper_dep); dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
m_dep_manager.linearize(dep, expl); m_dep_manager.linearize(dep, expl);
_().current_expl().add_expl(expl); m_core->current_expl().add_expl(expl);
TRACE("nla_solver", print_lemma(tout);); TRACE("nla_solver", m_core->print_lemma(tout););
return true; return true;
} }
bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) { bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) {
if (!separated_from_zero_on_lower(i)) if (!separated_from_zero_on_lower(i))
return false; return false;
add_empty_lemma(); m_core->add_empty_lemma();
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
dep = m_dep_manager.mk_join(dep, i.m_lower_dep); dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
m_dep_manager.linearize(dep, expl); m_dep_manager.linearize(dep, expl);
_().current_expl().add_expl(expl); m_core->current_expl().add_expl(expl);
TRACE("nla_solver", print_lemma(tout);); TRACE("nla_solver", m_core->print_lemma(tout););
return true; return true;
} }

13
src/math/lp/nla_intervals.h
View file

@ -28,11 +28,13 @@
namespace nla { namespace nla {
class core; class core;
class intervals : common { class intervals {
typedef common::ci_dependency_manager ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
class im_config { class im_config {
unsynch_mpq_manager& m_manager; unsynch_mpq_manager& m_manager;
ci_dependency_manager& m_dep_manager; common::ci_dependency_manager& m_dep_manager;
public: public:
typedef unsynch_mpq_manager numeral_manager; typedef unsynch_mpq_manager numeral_manager;
@ -135,11 +137,12 @@ class intervals : common {
}; };
region m_alloc; region m_alloc;
ci_value_manager m_val_manager; common::ci_value_manager m_val_manager;
mutable unsynch_mpq_manager m_num_manager; mutable unsynch_mpq_manager m_num_manager;
mutable ci_dependency_manager m_dep_manager; mutable ci_dependency_manager m_dep_manager;
im_config m_config; im_config m_config;
mutable interval_manager<im_config> m_imanager; mutable interval_manager<im_config> m_imanager;
core * m_core;
public: public:
ci_dependency_manager& dep_manager() { return m_dep_manager; } ci_dependency_manager& dep_manager() { return m_dep_manager; }
@ -151,11 +154,11 @@ private:
const lp::lar_solver& ls() const; const lp::lar_solver& ls() const;
public: public:
intervals(core* c, reslimit& lim) : intervals(core* c, reslimit& lim) :
common(c),
m_alloc(), m_alloc(),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager), m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager)) m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
m_core(c)
{} {}
ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b);} ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b);}
ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci);} ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci);}