mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

work on niil_solver base case

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-15 14:54:20 +08:00
parent 134ebb5712
commit 406a021310
2 changed files with 111 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -12,6 +12,7 @@ namespace nra {
lp::var_index m_v;
svector<lp::var_index> m_vs;
unsigned var() const { return m_v; }
unsigned size() const { return m_vs.size(); }
};
typedef std::unordered_map<lp::var_index, rational> variable_map_type;

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

@ -20,23 +20,75 @@ Revision History:
#include "util/lp/niil_solver.h"
#include "util/map.h"
#include "util/lp/mon_eq.h"
#include "util/lp/lp_utils.h"
namespace niil {
typedef nra::mon_eq mon_eq;
typedef lp::var_index lpvar;
struct solver::imp {
struct vars_equivalence {
typedef std::pair<lpvar, lpvar> lppair;
std::unordered_map<lppair,
int,
std::hash<lppair>
> m_map;
void add_equivalence_maybe(const lp::lar_term *t) {
if (t->size() != 2)
return;
bool seen_minus = false;
bool seen_plus = false;
lpvar i = -1, j;
for(const auto & p : *t) {
const auto & c = p.coeff();
if (c == 1) {
seen_plus = true;
} else if (c == - 1) {
seen_minus = true;
} else {
return;
}
if (i == static_cast<lpvar>(-1))
i = p.var();
else
j = p.var();
}
SASSERT(i != j && i != static_cast<lpvar>(-1));
if (i < j) { // swap if i > j ordered
lpvar tmp = i;
i = j;
j = tmp;
}
if (seen_minus && seen_plus)
m_map[lppair(i, j)] = -1; // we have x_i == - x_j
else
m_map[lppair(i, j)] = 1; // we have an equality
}
vars_equivalence(const lp::lar_solver& s) {
for (const lp::lar_term *t : s.terms())
add_equivalence_maybe(t);
}
lpvar get_equivalent_var(lpvar j, bool & sign) {
SASSERT(false);
return false;
}
bool empty() const {
return m_map.empty();
}
};
vars_equivalence m_vars_equivalence;
vector<mon_eq> m_monomials;
unsigned_vector m_monomials_lim;
lp::lar_solver& m_lar_solver;
std::unordered_map<lp::var_index, svector<unsigned>> m_var_to_monomials;
std::unordered_map<lpvar, svector<unsigned>> m_var_to_monomials;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
: m_lar_solver(s)
: m_vars_equivalence(s), m_lar_solver(s)
// m_limit(lim),
// m_params(p)
{
}
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
void add(lpvar v, unsigned sz, lpvar const* vs) {
m_monomials.push_back(mon_eq(v, sz, vs));
}
@ -59,39 +111,77 @@ struct solver::imp {
return r == model_val;
}
bool generate_basic_lemma_for_mon_sign(const mon_eq& m, lemma& l) {
bool generate_basic_lemma_for_mon_sign_var_other_mon( unsigned j_var,
const svector<unsigned> & mon_vars,
const mon_eq& om, bool sign, lemma& l) {
if (mon_vars.size() != om.size())
return false;
SASSERT(false);
return false;
}
bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon,
unsigned j_var, const svector<lpvar>& mon_vars, lemma& l, bool sign) {
auto it = m_var_to_monomials.find(j_var);
for (auto other_i_mon : it->second) {
if (other_i_mon == i_mon) continue;
if (generate_basic_lemma_for_mon_sign_var_other_mon(j_var, mon_vars,
m_monomials[other_i_mon], sign, l))
return true;
}
return false;
}
bool generate_basic_lemma_for_mon_zero(const mon_eq& m, lemma& l) {
// replaces each variable by a smaller one and flips the sing if the var comes with a minus
void reduce_monomial_to_minimal(svector<lpvar> & vars, int & sign) {
}
bool generate_basic_lemma_for_mon_sign(unsigned i_mon, lemma& l) {
if (m_vars_equivalence.empty()) {
std::cout << "empty m_vars_equivalence\n";
return false;
}
const mon_eq& m_of_i = m_monomials[i_mon];
int sign = 1;
auto mon_vars = m_of_i.m_vs;
reduce_monomial_to_minimal(mon_vars, sign);
for (unsigned j_var : mon_vars)
if (generate_basic_lemma_for_mon_sign_var(i_mon, j_var, mon_vars, l, sign))
return true;
return false;
}
bool generate_basic_lemma_for_mon_neutral(const mon_eq& m, lemma& l) {
bool generate_basic_lemma_for_mon_zero(unsigned i_mon, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon_proportionality(const mon_eq& m, lemma& l) {
bool generate_basic_lemma_for_mon_neutral(unsigned i_mon, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon(const mon_eq& m, lemma & l) {
return generate_basic_lemma_for_mon_sign(m, l)
|| generate_basic_lemma_for_mon_zero(m, l)
|| generate_basic_lemma_for_mon_neutral(m, l)
|| generate_basic_lemma_for_mon_proportionality(m, l);
bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon(unsigned i_mon, lemma & l) {
return generate_basic_lemma_for_mon_sign(i_mon, l)
|| generate_basic_lemma_for_mon_zero(i_mon, l)
|| generate_basic_lemma_for_mon_neutral(i_mon, l)
|| generate_basic_lemma_for_mon_proportionality(i_mon, l);
}
bool generate_basic_lemma(lemma & l, svector<unsigned> & to_refine) {
for (unsigned i : to_refine)
if (generate_basic_lemma_for_mon(m_monomials[i], l))
if (generate_basic_lemma_for_mon(i, l))
return true;
return false;
}
void map_monominals_vars(unsigned i) {
const mon_eq& m = m_monomials[i];
for (lp::var_index j : m.m_vs) {
for (lpvar j : m.m_vs) {
auto it = m_var_to_monomials.find(j);
if (it == m_var_to_monomials.end()) {
auto vect = svector<unsigned>();
@ -131,10 +221,12 @@ struct solver::imp {
return l_undef;
}
};
void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
std::cout << "called add_monomial\n";
void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
m_imp->add(v, sz, vs);
}
bool solver::need_check() { return true; }