mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

map term indices to columns when test checking lemmas

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-12 12:12:38 -08:00
parent c9a6d23897
commit b102710b2f
3 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/lar_solver.cpp
View file

@ -210,6 +210,11 @@ unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
unsigned ext_var_or_term = m_var_register.local_to_external(j);
return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term;
}
unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
SASSERT(is_term(j));
return m_var_register.external_to_local(j);
}
void lar_solver::propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) {
lp_assert(false); // not implemented

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

@ -271,6 +271,8 @@ public:
unsigned adjust_column_index_to_term_index(unsigned j) const;
unsigned map_term_index_to_column_index(unsigned j) const;
var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
unsigned number_of_vars() const { return m_var_register.size(); }

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

@ -142,8 +142,20 @@ struct solver::imp {
return ret;
}
lp::lar_term subs_terms_to_columns(const lp::lar_term& t) const {
lp::lar_term r;
for (const auto& p : t) {
lpvar j = p.var();
if (m_lar_solver.is_term(j))
j = m_lar_solver.map_term_index_to_column_index(j);
r.add_coeff_var(p.coeff(), j);
}
return r;
}
bool ineq_holds(const ineq& n) const {
return compare_holds(value(n.term()), n.cmp(), n.rs());
lp::lar_term t = subs_terms_to_columns(n.term());
return compare_holds(value(t), n.cmp(), n.rs());
}
bool an_ineq_holds(const lemma& l) const {