mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

cleanup nla_solver

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-08 16:37:10 -07:00 • committed by Lev Nachmanson
parent 6ce6922c5a
commit 540ea825b0
2 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/util/lp/factorization.cpp
View file

@ -2,7 +2,7 @@
#include "util/lp/factorization.h" #include "util/lp/factorization.h"
namespace nla { namespace nla {
void const_iterator::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const { void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const {
// the last element for m_factorization.m_rooted_vars goes to k_vars // the last element for m_factorization.m_rooted_vars goes to k_vars
SASSERT(m_mask.size() + 1 == m_ff->m_cmon.vars().size()); SASSERT(m_mask.size() + 1 == m_ff->m_cmon.vars().size());
k_vars.push_back(m_ff->m_cmon.vars().back()); k_vars.push_back(m_ff->m_cmon.vars().back());
@ -15,7 +15,7 @@ void const_iterator::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_ve
} }
} }
bool const_iterator::get_factors(unsigned& k, unsigned& j, rational& sign) const { bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) const {
unsigned_vector k_vars; unsigned_vector k_vars;
unsigned_vector j_vars; unsigned_vector j_vars;
init_vars_by_the_mask(k_vars, j_vars); init_vars_by_the_mask(k_vars, j_vars);
@ -47,7 +47,7 @@ bool const_iterator::get_factors(unsigned& k, unsigned& j, rational& sign) const
return true; return true;
} }
const_iterator::reference const_iterator::operator*() const { const_iterator_mon::reference const_iterator_mon::operator*() const {
if (m_full_factorization_returned == false) { if (m_full_factorization_returned == false) {
return create_full_factorization(); return create_full_factorization();
} }
@ -57,7 +57,7 @@ const_iterator::reference const_iterator::operator*() const {
return create_binary_factorization(j, k, m_ff->m_cmon.coeff() * sign); return create_binary_factorization(j, k, m_ff->m_cmon.coeff() * sign);
} }
void const_iterator::advance_mask() { void const_iterator_mon::advance_mask() {
if (!m_full_factorization_returned) { if (!m_full_factorization_returned) {
m_full_factorization_returned = true; m_full_factorization_returned = true;
return; return;
@ -74,23 +74,23 @@ void const_iterator::advance_mask() {
} }
const_iterator::self_type const_iterator::operator++() { self_type i = *this; operator++(1); return i; } const_iterator_mon::self_type const_iterator_mon::operator++() { self_type i = *this; operator++(1); return i; }
const_iterator::self_type const_iterator::operator++(int) { advance_mask(); return *this; } const_iterator_mon::self_type const_iterator_mon::operator++(int) { advance_mask(); return *this; }
const_iterator::const_iterator(const svector<bool>& mask, const factorization_factory *f) : const_iterator_mon::const_iterator_mon(const svector<bool>& mask, const factorization_factory *f) :
m_mask(mask), m_mask(mask),
m_ff(f) , m_ff(f) ,
m_full_factorization_returned(false) m_full_factorization_returned(false)
{} {}
bool const_iterator::operator==(const const_iterator::self_type &other) const { bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other) const {
return return
m_full_factorization_returned == other.m_full_factorization_returned && m_full_factorization_returned == other.m_full_factorization_returned &&
m_mask == other.m_mask; m_mask == other.m_mask;
} }
bool const_iterator::operator!=(const const_iterator::self_type &other) const { return !(*this == other); } bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); }
factorization const_iterator::create_binary_factorization(lpvar j, lpvar k, rational const& sign) const { factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k, rational const& sign) const {
// todo : the current explanation is an overkill // todo : the current explanation is an overkill
// std::function<void (expl_set&)> explain = [&](expl_set& exp){ // std::function<void (expl_set&)> explain = [&](expl_set& exp){
// const imp & impl = m_ff->m_impf; // const imp & impl = m_ff->m_impf;
@ -111,7 +111,7 @@ factorization const_iterator::create_binary_factorization(lpvar j, lpvar k, rati
return f; return f;
} }
factorization const_iterator::create_full_factorization() const { factorization const_iterator_mon::create_full_factorization() const {
factorization f; factorization f;
f.vars() = m_ff->m_mon.vars(); f.vars() = m_ff->m_mon.vars();
f.sign() = rational(1); f.sign() = rational(1);

14
src/util/lp/factorization.h
View file

@ -41,14 +41,14 @@ public:
const lpvar* end() const { return m_vars.end(); } const lpvar* end() const { return m_vars.end(); }
}; };
struct const_iterator { struct const_iterator_mon {
// fields // fields
svector<bool> m_mask; svector<bool> m_mask;
const factorization_factory * m_ff; const factorization_factory * m_ff;
bool m_full_factorization_returned; bool m_full_factorization_returned;
//typedefs //typedefs
typedef const_iterator self_type; typedef const_iterator_mon self_type;
typedef factorization value_type; typedef factorization value_type;
typedef const factorization reference; typedef const factorization reference;
typedef int difference_type; typedef int difference_type;
@ -64,7 +64,7 @@ struct const_iterator {
self_type operator++(); self_type operator++();
self_type operator++(int); self_type operator++(int);
const_iterator(const svector<bool>& mask, const factorization_factory *f); const_iterator_mon(const svector<bool>& mask, const factorization_factory *f);
bool operator==(const self_type &other) const; bool operator==(const self_type &other) const;
bool operator!=(const self_type &other) const; bool operator!=(const self_type &other) const;
@ -87,16 +87,16 @@ struct factorization_factory {
m_cmon(cmon) { m_cmon(cmon) {
} }
const_iterator begin() const { const_iterator_mon begin() const {
// we keep the last element always in the first factor to avoid // we keep the last element always in the first factor to avoid
// repeating a pair twice // repeating a pair twice
svector<bool> mask(m_mon.vars().size() - 1, false); svector<bool> mask(m_mon.vars().size() - 1, false);
return const_iterator(mask, this); return const_iterator_mon(mask, this);
} }
const_iterator end() const { const_iterator_mon end() const {
svector<bool> mask(m_mon.vars().size() - 1, true); svector<bool> mask(m_mon.vars().size() - 1, true);
auto it = const_iterator(mask, this); auto it = const_iterator_mon(mask, this);
it.m_full_factorization_returned = true; it.m_full_factorization_returned = true;
return it; return it;
} }