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

fixed vars are treated as scalars optionally

Browse source 
Signed-off-by: Lev Nachmanson <levnach@nachmanson.com>
This commit is contained in:
Lev Nachmanson 2019-10-19 15:54:40 -07:00 • committed by Lev Nachmanson
parent d77e9c444e
commit 538ad77019
5 changed files with 15 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/horner.cpp
View file

@ -25,7 +25,7 @@
namespace nla { namespace nla {
typedef intervals::interval interv; typedef intervals::interval interv;
horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} horner::horner(core * c) : common(c), m_intervals(c, c->reslim()), m_fixed_as_scalars(true) {}
template <typename T> template <typename T>
bool horner::row_has_monomial_to_refine(const T& row) const { bool horner::row_has_monomial_to_refine(const T& row) const {
@ -81,7 +81,7 @@ bool horner::check_cross_nested_expr(const nex* n) {
} }
auto interv_wd = interval_of_expr_with_deps(n, 1); auto interv_wd = interval_of_expr_with_deps(n, 1);
TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";); TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";);
ci_dependency* dep = get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()); ci_dependency* dep = m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()) : nullptr;
m_intervals.check_interval_for_conflict_on_zero(interv_wd, dep); m_intervals.check_interval_for_conflict_on_zero(interv_wd, dep);
m_intervals.reset(); // clean the memory allocated by the interval bound dependencies m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
return true; return true;
@ -96,7 +96,7 @@ bool horner::lemmas_on_row(const T& row) {
SASSERT (row_is_interesting(row)); SASSERT (row_is_interesting(row));
c().clear_and_resize_active_var_set(); c().clear_and_resize_active_var_set();
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars);
set_active_vars_weights(); // without this call the comparisons will be incorrect set_active_vars_weights(); // without this call the comparisons will be incorrect
nex* e = m_nex_creator.simplify(&m_row_sum); nex* e = m_nex_creator.simplify(&m_row_sum);
TRACE("nla_horner", tout << "e = " << * e << "\n";); TRACE("nla_horner", tout << "e = " << * e << "\n";);

5
src/math/lp/horner.h
View file

@ -30,9 +30,10 @@ class core;
class horner : common { class horner : common {
intervals m_intervals; intervals m_intervals;
nex_sum m_row_sum; nex_sum m_row_sum;
unsigned m_row_index; unsigned m_row_index;
bool m_fixed_as_scalars;
public: public:
typedef intervals::interval interv; typedef intervals::interval interv;
horner(core *core); horner(core *core);

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

@ -124,9 +124,9 @@ unsigned common::random() {
// creates a nex expression for the coeff and var, // creates a nex expression for the coeff and var,
// replaces the fixed vars with scalars // replaces the fixed vars with scalars
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) {
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
if (c().var_is_fixed(j)) { if (fixed_as_scalars && c().var_is_fixed(j)) {
return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x);
} }
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
@ -135,7 +135,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
const monic& m = c().emons()[j]; const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
for (lpvar k : m.vars()) { for (lpvar k : m.vars()) {
if (c().var_is_fixed(k)) { if (fixed_as_scalars && c().var_is_fixed(k)) {
e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; e->coeff() *= c().m_lar_solver.get_lower_bound(k).x;
continue; continue;
} }
@ -149,14 +149,14 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
template <typename T> void common::create_sum_from_row(const T& row, template <typename T> void common::create_sum_from_row(const T& row,
nex_creator& cn, nex_creator& cn,
nex_sum& sum) { nex_sum& sum, bool fixed_as_scalars) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
SASSERT(row.size() > 1); SASSERT(row.size() > 1);
sum.children().clear(); sum.children().clear();
for (const auto &p : row) { for (const auto &p : row) {
nex* e = nexvar(p.coeff(), p.var(), cn); nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars);
sum.add_child(e); sum.add_child(e);
} }
TRACE("nla_horner", tout << "sum =" << sum << "\n";); TRACE("nla_horner", tout << "sum =" << sum << "\n";);
@ -229,6 +229,6 @@ var_weight common::get_var_weight(lpvar j) const {
} }
template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&); template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool);
template dependency_manager<nla::common::ci_dependency_config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, dependency_manager<nla::common::ci_dependency_config>&); template dependency_manager<nla::common::ci_dependency_config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, dependency_manager<nla::common::ci_dependency_config>&);

4
src/math/lp/nla_common.h
View file

@ -118,9 +118,9 @@ struct common {
typedef ci_dependency_manager::dependency ci_dependency; typedef ci_dependency_manager::dependency ci_dependency;
// nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints); // nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
nex* nexvar(const rational& coeff, lpvar j, nex_creator&); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool);
template <typename T> template <typename T>
void create_sum_from_row(const T&, nex_creator&, nex_sum&); void create_sum_from_row(const T&, nex_creator&, nex_sum&, bool);
template <typename T> template <typename T>
ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager);
void set_active_vars_weights(); void set_active_vars_weights();

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

@ -183,7 +183,7 @@ void nla_grobner::add_row(unsigned i) {
nex_sum * ns = m_nex_creator.mk_sum(); nex_sum * ns = m_nex_creator.mk_sum();
svector<lp::constraint_index> fixed_vars_constraints; svector<lp::constraint_index> fixed_vars_constraints;
create_sum_from_row(row, m_nex_creator, *ns); create_sum_from_row(row, m_nex_creator, *ns, true); // true to treat fixed vars as scalars
TRACE("nla_grobner", tout << "ns = " << *ns << "\n";); TRACE("nla_grobner", tout << "ns = " << *ns << "\n";);
m_tmp_var_set.clear(); m_tmp_var_set.clear();
assert_eq_0(ns, get_fixed_vars_dep_from_row(row, m_dep_manager)); assert_eq_0(ns, get_fixed_vars_dep_from_row(row, m_dep_manager));