mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
simplify the fixed var table
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
d09e6eccf0
commit
d13e584706
|
@ -1729,7 +1729,7 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c
|
|||
}
|
||||
|
||||
void lar_solver::remove_non_fixed_from_fixed_var_table() {
|
||||
vector<value_sort_pair> to_remove;
|
||||
vector<mpq> to_remove;
|
||||
for (const auto& p : m_fixed_var_table) {
|
||||
unsigned j = p.m_value;
|
||||
if (j >= column_count() || !column_is_fixed(j))
|
||||
|
@ -1746,7 +1746,7 @@ void lar_solver::register_in_fixed_var_table(unsigned j, unsigned & equal_to_j)
|
|||
if (!bound.y.is_zero())
|
||||
return;
|
||||
|
||||
value_sort_pair key(bound.x, column_is_int(j));
|
||||
const mpq& key = bound.x;
|
||||
unsigned k;
|
||||
if (!m_fixed_var_table.find(key, k)) {
|
||||
m_fixed_var_table.insert(key, j);
|
||||
|
|
|
@ -49,8 +49,6 @@ namespace lp {
|
|||
class int_branch;
|
||||
class int_solver;
|
||||
class lar_solver : public column_namer {
|
||||
typedef std::pair<mpq, bool> value_sort_pair;
|
||||
typedef pair_hash<obj_hash<mpq>, bool_hash> value_sort_pair_hash;
|
||||
struct term_hasher {
|
||||
std::size_t operator()(const lar_term &t) const
|
||||
{
|
||||
|
@ -105,10 +103,7 @@ class lar_solver : public column_namer {
|
|||
vector<impq> m_backup_x;
|
||||
stacked_vector<unsigned> m_usage_in_terms;
|
||||
// ((x[j], is_int(j))->j) for fixed j, used in equalities propagation
|
||||
map<value_sort_pair,
|
||||
unsigned,
|
||||
value_sort_pair_hash,
|
||||
default_eq<value_sort_pair>> m_fixed_var_table;
|
||||
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_fixed_var_table;
|
||||
// end of fields
|
||||
|
||||
////////////////// methods ////////////////////////////////
|
||||
|
@ -290,16 +285,10 @@ class lar_solver : public column_namer {
|
|||
void register_normalized_term(const lar_term&, lpvar);
|
||||
void deregister_normalized_term(const lar_term&);
|
||||
public:
|
||||
const map<value_sort_pair,
|
||||
unsigned,
|
||||
value_sort_pair_hash,
|
||||
default_eq<value_sort_pair>>& fixed_var_table() const {
|
||||
const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table() const {
|
||||
return m_fixed_var_table;
|
||||
}
|
||||
map<value_sort_pair,
|
||||
unsigned,
|
||||
value_sort_pair_hash,
|
||||
default_eq<value_sort_pair>>& fixed_var_table() {
|
||||
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table() {
|
||||
return m_fixed_var_table;
|
||||
}
|
||||
unsigned external_to_column_index(unsigned) const;
|
||||
|
|
|
@ -324,9 +324,8 @@ public:
|
|||
if (is_offset_row(rid, x, y, k)) {
|
||||
if (y == null_lpvar) {
|
||||
// x is an implied fixed var at k.
|
||||
value_sort_pair key(k, is_int(x));
|
||||
unsigned x2;
|
||||
if (lp().fixed_var_table().find(key, x2) && !is_equal(x, x2)) {
|
||||
if (lp().fixed_var_table().find(k, x2) && !is_equal(x, x2)) {
|
||||
SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k && is_int(x) == is_int(x2));
|
||||
explanation ex;
|
||||
constraint_index lc, uc;
|
||||
|
|
Loading…
Reference in a new issue