mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

rename niil to nla

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-19 11:48:42 -07:00 committed by Lev Nachmanson
parent 56ae577c97
commit 96aaa8638e
4 changed files with 51 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
src/smt/theory_lra.cpp
View file

@ -258,23 +258,23 @@ class theory_lra::imp {
// non-linear arithmetic
scoped_ptr<nra::solver> m_nra;
bool m_use_niil;
scoped_ptr<niil::solver> m_niil;
bool m_use_nla;
scoped_ptr<nla::solver> m_nla;
bool m_use_nra_model;
scoped_ptr<scoped_anum> m_a1, m_a2;
struct switcher {
theory_lra::imp& m_th_imp;
scoped_ptr<nra::solver>* m_nra;
scoped_ptr<niil::solver>* m_niil;
bool m_use_niil;
switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_niil(nullptr) {
scoped_ptr<nla::solver>* m_nla;
bool m_use_nla;
switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_nla(nullptr) {
}
bool need_check() {
if (m_use_niil) {
if (m_niil != nullptr)
return (*m_niil)->need_check();
if (m_use_nla) {
if (m_nla != nullptr)
return (*m_nla)->need_check();
}
else {
if (m_nra != nullptr)
@ -284,9 +284,9 @@ class theory_lra::imp {
}
void push() {
if (m_use_niil) {
if (m_niil != nullptr)
(*m_niil)->push();
if (m_use_nla) {
if (m_nla != nullptr)
(*m_nla)->push();
}
else {
if (m_nra != nullptr)
@ -295,9 +295,9 @@ class theory_lra::imp {
}
void pop(unsigned scopes) {
if (m_use_niil) {
if (m_niil != nullptr)
(*m_niil)->pop(scopes);
if (m_use_nla) {
if (m_nla != nullptr)
(*m_nla)->pop(scopes);
}
else {
if (m_nra != nullptr)
@ -307,9 +307,9 @@ class theory_lra::imp {
void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
if (m_use_niil) {
m_th_imp.ensure_niil();
(*m_niil)->add_monomial(v, sz, vs);
if (m_use_nla) {
m_th_imp.ensure_nla();
(*m_nla)->add_monomial(v, sz, vs);
}
else {
m_th_imp.ensure_nra();
@ -383,7 +383,7 @@ class theory_lra::imp {
m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_switcher.m_use_niil = m_use_niil = lp.niil();
m_switcher.m_use_nla = m_use_nla = lp.nla();
m_lia = alloc(lp::int_solver, m_solver.get());
get_one(true);
get_zero(true);
@ -431,9 +431,14 @@ class theory_lra::imp {
if (!m_niil) {
m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params());
m_switcher.m_niil = &m_niil;
void ensure_nla() {
if (!m_nla) {
m_nla = alloc(nla::solver, *m_solver.get(), m.limit(), ctx().get_params());
m_switcher.m_nla = &m_nla;
for (auto const& _s : m_scopes) {
(void)_s;
m_niil->push();
m_nla->push();
}
}
}
@ -1600,7 +1605,7 @@ public:
bool is_eq(theory_var v1, theory_var v2) {
if (m_use_nra_model) {
lp_assert(!m_use_niil);
lp_assert(!m_use_nla);
return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
}
else {
@ -2097,9 +2102,9 @@ public:
return r;
}
niil::lemma m_lemma;
nla::lemma m_lemma;
lbool check_aftermath_niil(lbool r) {
lbool check_aftermath_nla(lbool r) {
switch (r) {
case l_false: {
literal_vector core;
@ -2147,12 +2152,12 @@ public:
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
if (!m_nra && !m_niil) return l_true;
if (!m_nra && !m_nla) return l_true;
if (!m_switcher.need_check()) return l_true;
m_a1 = nullptr; m_a2 = nullptr;
m_explanation.reset();
lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, m_lemma);
return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
lbool r = m_nra? m_nra->check(m_explanation): m_nla->check(m_explanation, m_lemma);
return m_nra? check_aftermath_nra(r) : check_aftermath_nla(r);
}
/**

2
src/util/lp/lp_params.pyg
View file

@ -7,7 +7,7 @@ def_module_params('lp',
('simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
('enable_hnf', BOOL, True, 'enable hnf cuts'),
('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
('niil', BOOL, False, 'call nonlinear integer solver with incremental linearization')
('nla', BOOL, False, 'call nonlinear integer solver with incremental linearization')
))

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

@ -21,7 +21,7 @@
#include "util/map.h"
#include "util/lp/mon_eq.h"
#include "util/lp/lp_utils.h"
namespace niil {
namespace nla {
typedef lp::constraint_index lpci;
typedef std::unordered_set<lpci> expl_set;
typedef nra::mon_eq mon_eq;
@ -251,7 +251,7 @@ struct solver::imp {
fill_explanation_and_lemma_sign(m_monomials[i_mon],
other_m,
sign * other_sign);
TRACE("niil_solver", tout << "lemma generated\n";);
TRACE("nla_solver", tout << "lemma generated\n";);
return true;
}
@ -291,7 +291,7 @@ struct solver::imp {
add_explanation_of_reducing_to_mininal_monomial(b, expl);
m_expl->clear();
m_expl->add(expl);
TRACE("niil_solver",
TRACE("nla_solver",
tout << "used constraints: ";
for (auto &p : *m_expl)
m_lar_solver.print_constraint(p.second, tout); tout << "\n";
@ -299,7 +299,7 @@ struct solver::imp {
lp::lar_term t;
t.add_coeff_var(rational(1), a.var());
t.add_coeff_var(rational(- sign), b.var());
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
ineq in(lp::lconstraint_kind::NE, t);
m_lemma->push_back(in);
}
@ -465,7 +465,7 @@ struct solver::imp {
default:
if (mon_val.is_zero() && var_is_fixed_to_zero(mon.var())) {
create_lemma_one_of_the_factors_is_zero(mon);
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
return true;
}
return false;
@ -475,7 +475,7 @@ struct solver::imp {
t.m_v = -rs;
ineq in(kind, t);
m_lemma->push_back(in);
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
return true;
}
@ -590,7 +590,7 @@ struct solver::imp {
}
vector<mono_index_with_sign> get_ones_of_monomimal(const svector<lpvar> & vars) {
TRACE("niil_solver", tout << "get_ones_of_monomimal";);
TRACE("nla_solver", tout << "get_ones_of_monomimal";);
vector<mono_index_with_sign> ret;
for (unsigned i = 0; i < vars.size(); i++) {
mono_index_with_sign mi;
@ -722,7 +722,7 @@ struct solver::imp {
t.add_coeff_var(rational(- sign), j);
ineq in(lp::lconstraint_kind::EQ, t);
m_lemma->push_back(in);
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
}
// vars here are minimal vars for m.vs
@ -738,7 +738,7 @@ struct solver::imp {
if (mask[k] == 0) {
mask[k] = 1;
sign *= ones_of_monomial[k].m_sign;
TRACE("niil_solver", tout << "index m_i = " << ones_of_monomial[k].m_i;);
TRACE("nla_solver", tout << "index m_i = " << ones_of_monomial[k].m_i;);
vars.erase(vars.begin() + ones_of_monomial[k].m_i);
std::sort(vars.begin(), vars.end());
// now the value of vars has to be v*sign
@ -811,7 +811,7 @@ struct solver::imp {
bool large_lemma_for_proportion_case(const mon_eq& m, const unsigned_vector & mask,
const unsigned_vector & large, unsigned j) {
TRACE("niil_solver", );
TRACE("nla_solver", );
const rational j_val = m_lar_solver.get_column_value_rational(j);
const rational m_val = m_lar_solver.get_column_value_rational(m.m_v);
const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v));
@ -835,7 +835,7 @@ struct solver::imp {
bool small_lemma_for_proportion_case(const mon_eq& m, const unsigned_vector & mask,
const unsigned_vector & _small, unsigned j) {
TRACE("niil_solver", );
TRACE("nla_solver", );
const rational j_val = m_lar_solver.get_column_value_rational(j);
const rational m_val = m_lar_solver.get_column_value_rational(m.m_v);
const rational m_abs_val = lp::abs(m_lar_solver.get_column_value_rational(m.m_v));
@ -891,7 +891,7 @@ struct solver::imp {
for (unsigned k = 0; k < mask.size(); k++) {
if (mask[k] == 0) {
mask[k] = 1;
TRACE("niil_solver", tout << "large[" << k << "] = " << large[k];);
TRACE("nla_solver", tout << "large[" << k << "] = " << large[k];);
SASSERT(std::find(vars.begin(), vars.end(), vars_copy[large[k]]) != vars.end());
vars.erase(vars_copy[large[k]]);
std::sort(vars.begin(), vars.end());
@ -899,7 +899,7 @@ struct solver::imp {
lpvar j;
if (find_compimenting_monomial(vars, j) &&
large_lemma_for_proportion_case(m, mask, large, j)) {
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
return true;
}
} else {
@ -922,7 +922,7 @@ struct solver::imp {
for (unsigned k = 0; k < mask.size(); k++) {
if (mask[k] == 0) {
mask[k] = 1;
TRACE("niil_solver", tout << "_small[" << k << "] = " << _small[k];);
TRACE("nla_solver", tout << "_small[" << k << "] = " << _small[k];);
SASSERT(std::find(vars.begin(), vars.end(), vars_copy[_small[k]]) != vars.end());
vars.erase(vars_copy[_small[k]]);
std::sort(vars.begin(), vars.end());
@ -930,7 +930,7 @@ struct solver::imp {
lpvar j;
if (find_compimenting_monomial(vars, j) &&
small_lemma_for_proportion_case(m, mask, _small, j)) {
TRACE("niil_solver", print_explanation_and_lemma(tout););
TRACE("nla_solver", print_explanation_and_lemma(tout););
return true;
}
} else {
@ -949,7 +949,7 @@ struct solver::imp {
unsigned_vector large;
unsigned_vector _small;
get_large_and_small_indices_of_monomimal(m, large, _small);
TRACE("niil_solver", tout << "large size = " << large.size() << ", _small size = " << _small.size(););
TRACE("nla_solver", tout << "large size = " << large.size() << ", _small size = " << _small.size(););
if (large.empty() && _small.empty())
return false;
@ -966,7 +966,7 @@ struct solver::imp {
}
bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon) {
TRACE("niil_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
TRACE("nla_solver", tout << "generate_basic_lemma_for_mon_proportionality";);
if (basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon))
return true;
@ -1172,7 +1172,7 @@ struct solver::imp {
}
lbool check(lp::explanation & exp, lemma& l) {
TRACE("niil_solver", tout << "check of niil";);
TRACE("nla_solver", tout << "check of nla";);
m_expl = &exp;
m_lemma = &l;
lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
@ -1185,7 +1185,7 @@ struct solver::imp {
if (to_refine.empty())
return l_true;
TRACE("niil_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);
TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);
init_search();

2
src/util/lp/nla_solver.h
View file

@ -24,7 +24,7 @@ Revision History:
#include "util/params.h"
#include "nlsat/nlsat_solver.h"
#include "util/lp/lar_solver.h"
namespace niil {
namespace nla {
struct ineq {
lp::lconstraint_kind m_cmp;
lp::lar_term m_term;