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

handle unsorted monomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-22 11:03:32 +08:00
parent 237db5cb3d
commit 08d891891e
5 changed files with 32 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -430,7 +430,7 @@ class theory_lra::imp {
} }
void ensure_niil() { void ensure_niil() {
if (!m_niil) { if (!m_niil) {
m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params()); m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params(), false);
m_switcher.m_niil = &m_niil; m_switcher.m_niil = &m_niil;
for (auto const& _s : m_scopes) { for (auto const& _s : m_scopes) {
(void)_s; (void)_s;

8
src/util/lp/lp_utils.h
View file

@ -29,6 +29,14 @@ void print_vector(const C & t, std::ostream & out) {
out << std::endl; out << std::endl;
} }
template <typename C>
void print_vector(const C * t, unsigned size, std::ostream & out) {
for (unsigned i = 0; i < size; i++ )
out << t[i] << " ";
out << std::endl;
}
template <typename A, typename B> template <typename A, typename B>
bool try_get_value(const std::unordered_map<A,B> & map, const A& key, B & val) { bool try_get_value(const std::unordered_map<A,B> & map, const A& key, B & val) {
const auto it = map.find(key); const auto it = map.find(key);

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

@ -9,6 +9,8 @@ namespace nra {
struct mon_eq { struct mon_eq {
mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs): mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
m_v(v), m_vs(sz, vs) {} m_v(v), m_vs(sz, vs) {}
mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
m_v(v), m_vs(vs) {}
lp::var_index m_v; lp::var_index m_v;
svector<lp::var_index> m_vs; svector<lp::var_index> m_vs;
unsigned var() const { return m_v; } unsigned var() const { return m_v; }

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

@ -33,9 +33,8 @@ struct solver::imp {
lpvar m_i; lpvar m_i;
lpvar m_j; lpvar m_j;
int m_sign; int m_sign;
lpci m_c0; lpci m_c0;
lpci m_c1; lpci m_c1;
equiv(lpvar i, lpvar j, int sign, lpci c0, lpci c1) : equiv(lpvar i, lpvar j, int sign, lpci c0, lpci c1) :
m_i(i), m_i(i),
m_j(j), m_j(j),
@ -196,17 +195,29 @@ struct solver::imp {
std::unordered_map<lpvar, var_lists> m_var_lists; std::unordered_map<lpvar, var_lists> m_var_lists;
lp::explanation * m_expl; lp::explanation * m_expl;
lemma * m_lemma; lemma * m_lemma;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) bool m_monomials_are_presorted;
: m_lar_solver(s) imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_presorted)
: m_lar_solver(s), m_monomials_are_presorted(monomials_are_presorted)
// m_limit(lim), // m_limit(lim),
// m_params(p) // m_params(p)
{ {
} }
void add(lpvar v, unsigned sz, lpvar const* vs) { void add(lpvar v, unsigned sz, lpvar const* vs) {
m_monomials.push_back(mon_eq(v, sz, vs)); if (m_monomials_are_presorted) {
m_monomials.push_back(mon_eq(v, sz, vs));
}
else {
svector<lpvar> sorted_vs;
for (unsigned i = 0; i < sz; i++)
sorted_vs.push_back(vs[i]);
std::sort(sorted_vs.begin(), sorted_vs.end());
std::cout << "sorted_vs = ";
print_vector(sorted_vs, std::cout);
m_monomials.push_back(mon_eq(v, sorted_vs));
}
} }
void push() { void push() {
m_monomials_lim.push_back(m_monomials.size()); m_monomials_lim.push_back(m_monomials.size());
} }
@ -640,8 +651,8 @@ void solver::pop(unsigned n) {
} }
solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) { solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_sorted) {
m_imp = alloc(imp, s, lim, p); m_imp = alloc(imp, s, lim, p, monomials_are_sorted);
} }

3
src/util/lp/niil_solver.h
View file

@ -40,8 +40,7 @@ public:
struct imp; struct imp;
imp* m_imp; imp* m_imp;
void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs); void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
solver(lp::lar_solver& s, reslimit& lim, params_ref const& p); solver(lp::lar_solver& s, reslimit& lim, params_ref const& p, bool monomials_are_presorted);
imp* get_imp(); imp* get_imp();
void push(); void push();
void pop(unsigned scopes); void pop(unsigned scopes);