mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

refactor mon_eq out or nra_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-12 20:34:26 +08:00
parent b6f07e2a23
commit 07c9e22303
3 changed files with 14 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/CMakeLists.txt
View file

@ -21,6 +21,7 @@ z3_add_component(lp
lu.cpp lu.cpp
lp_utils.cpp lp_utils.cpp
matrix.cpp matrix.cpp
mon_eq.cpp
niil_solver.cpp niil_solver.cpp
nra_solver.cpp nra_solver.cpp
permutation_matrix.cpp permutation_matrix.cpp

4
src/util/lp/niil_solver.cpp
View file

@ -19,7 +19,11 @@ Revision History:
--*/ --*/
#include "util/lp/niil_solver.h" #include "util/lp/niil_solver.h"
#include "util/map.h" #include "util/map.h"
#include "util/lp/mon_eq.h"
namespace niil { namespace niil {
typedef nra::mon_eq mon_eq;
struct solver::imp { struct solver::imp {
vector<mon_eq> m_monomials; vector<mon_eq> m_monomials;

24
src/util/lp/nra_solver.cpp
View file

@ -9,27 +9,21 @@
#include "math/polynomial/polynomial.h" #include "math/polynomial/polynomial.h"
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
#include "util/map.h" #include "util/map.h"
#include "util/lp/mon_eq.h"
namespace nra { namespace nra {
struct mon_eq {
mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) {}
lp::var_index m_v;
svector<lp::var_index> m_vs;
};
struct solver::imp { struct solver::imp {
lp::lar_solver& s; lp::lar_solver& s;
reslimit& m_limit; reslimit& m_limit;
params_ref m_params; params_ref m_params;
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
scoped_ptr<nlsat::solver> m_nlsat; scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum> m_zero; scoped_ptr<scoped_anum> m_zero;
vector<mon_eq> m_monomials; vector<mon_eq> m_monomials;
unsigned_vector m_monomials_lim; unsigned_vector m_monomials_lim;
mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model mutable variable_map_type m_variable_values; // current model
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): imp(lp::lar_solver& s, reslimit& lim, params_ref const& p):
s(s), s(s),
@ -38,7 +32,7 @@ namespace nra {
} }
bool need_check() { bool need_check() {
return !m_monomials.empty() && !check_assignments(); return !m_monomials.empty() && !check_assignments(m_monomials, s, m_variable_values);
} }
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) { void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
@ -60,7 +54,7 @@ namespace nra {
multiply values for vs and check if they are equal to value for v. multiply values for vs and check if they are equal to value for v.
epsilon has been computed. epsilon has been computed.
*/ */
bool check_assignment(mon_eq const& m) const { /* bool check_assignment(mon_eq const& m) const {
rational r1 = m_variable_values[m.m_v]; rational r1 = m_variable_values[m.m_v];
rational r2(1); rational r2(1);
for (auto w : m.m_vs) { for (auto w : m.m_vs) {
@ -76,7 +70,7 @@ namespace nra {
} }
return true; return true;
} }
*/
/** /**
\brief one-shot nlsat check. \brief one-shot nlsat check.
A one shot checker is the least functionality that can A one shot checker is the least functionality that can