mirror of
https://github.com/Z3Prover/z3
synced 2025-10-16 20:40:27 +00:00
Propagate assignment if all bits are assigned and use better justification if any found
This commit is contained in:
Clemens Eisenhofer
parent
52eefb6e85
commit
39a4bb025b
7 changed files with 460 additions and 313 deletions
|
|
@ -12,7 +12,8 @@ Abstract:
|
|||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "types.h"
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/types.h"
|
||||
#include "util/hash.h"
|
||||
#include "util/optional.h"
|
||||
#include "util/tbv.h"
|
||||
|
|
@ -23,7 +24,8 @@ namespace polysat {
|
|||
class solver;
|
||||
class constraint;
|
||||
class fixed_bits;
|
||||
|
||||
class bitvec_info;
|
||||
|
||||
struct bvpos {
|
||||
optional<pdd> m_pdd;
|
||||
unsigned m_bit_idx;
|
||||
|
|
@ -58,15 +60,19 @@ namespace polysat {
|
|||
|
||||
using bit_dependencies = vector<bvpos>;
|
||||
|
||||
class bit_justication {
|
||||
class bit_justification {
|
||||
protected:
|
||||
static bit_justication* get_other_justification(const fixed_bits& fixed, const pdd& p, unsigned idx);
|
||||
static bit_justification* get_justification(fixed_bits& fixed, const pdd& p, unsigned idx);
|
||||
static unsigned get_level(fixed_bits& fixed, const pdd& p, unsigned idx);
|
||||
static const tbv_ref* get_tbv(fixed_bits& fixed, const pdd& p);
|
||||
static bool fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication** j);
|
||||
static bool fix_bit(solver& s, fixed_bits& fixed, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j);
|
||||
|
||||
bit_justification() = default;
|
||||
public:
|
||||
|
||||
unsigned m_decision_level;
|
||||
|
||||
// if we reduce this value we would have to reduce some decision levels of justifications depending on it.
|
||||
// However, we don't do this for now. (Should be still correct but generate weaker justifications)
|
||||
// This value is used for comparing which of two justifications is better. Does not have to be 100% correct
|
||||
unsigned m_decision_level = UINT32_MAX; // maybe better "weight"?
|
||||
|
||||
virtual bool can_dealloc() { return true; } // we may not dealloc if the justification is used for multiple bits
|
||||
virtual bool has_constraint(constraint*& constr) { return false; }
|
||||
|
|
@ -75,14 +81,16 @@ namespace polysat {
|
|||
|
||||
// if multiple bits are justified by the same justification
|
||||
// All elements have to be in the same decision-level
|
||||
class bit_justication_shared : public bit_justication {
|
||||
bit_justication* m_justification;
|
||||
class bit_justification_shared : public bit_justification {
|
||||
bit_justification* m_justification;
|
||||
unsigned m_references = 0;
|
||||
public:
|
||||
bit_justication_shared() = default;
|
||||
bit_justication_shared(bit_justication* j) : m_justification(j), m_references(1) {}
|
||||
bit_justification_shared(bit_justification* j) : m_justification(j), m_references(1) {
|
||||
SASSERT(j);
|
||||
m_decision_level = j->m_decision_level;
|
||||
}
|
||||
|
||||
bit_justication* get_justification() { return m_justification; }
|
||||
bit_justification* get_justification() { return m_justification; }
|
||||
|
||||
virtual bool can_dealloc() {
|
||||
m_references = m_references == 0 ? 0 : m_references - 1;
|
||||
|
|
@ -103,52 +111,50 @@ namespace polysat {
|
|||
void inc_ref() { m_references++; }
|
||||
};
|
||||
|
||||
class bit_justication_constraint : public bit_justication {
|
||||
class bit_justification_constraint : public bit_justification {
|
||||
|
||||
constraint* m_constraint = nullptr;
|
||||
|
||||
// A pdd might occur multiple times if more bits of it are relevant
|
||||
bit_dependencies m_dependencies;
|
||||
|
||||
bit_justication_constraint(constraint* c) : m_constraint(c) {}
|
||||
bit_justication_constraint(constraint* c, const bit_dependencies& dep) : m_constraint(c), m_dependencies(dep) {}
|
||||
bit_justication_constraint(constraint* c, bit_dependencies&& dep) : m_constraint(c), m_dependencies(dep) {}
|
||||
|
||||
bit_justification_constraint(solver& s, constraint* c, bit_dependencies&& dep);
|
||||
bit_justification_constraint(solver& s, constraint* c, const bit_dependencies& dep) : bit_justification_constraint(s, c, bit_dependencies(dep)) {}
|
||||
bit_justification_constraint(solver& s, constraint* c) : bit_justification_constraint(s, c, bit_dependencies()) {}
|
||||
|
||||
public:
|
||||
|
||||
bit_justication_constraint() = default;
|
||||
|
||||
|
||||
bool has_constraint(constraint*& constr) {
|
||||
constr = m_constraint;
|
||||
return true;
|
||||
}
|
||||
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
|
||||
|
||||
static bit_justication_constraint* mk_assignment(constraint* c) { return alloc(bit_justication_constraint, c ); }
|
||||
static bit_justication_constraint* mk_unary(constraint* c, bvpos v) {
|
||||
static bit_justification_constraint* mk_assignment(solver& s, constraint* c) { return alloc(bit_justification_constraint, s, c); }
|
||||
static bit_justification_constraint* mk_unary(solver& s, constraint* c, bvpos v) {
|
||||
bit_dependencies dep;
|
||||
dep.push_back(std::move(v));
|
||||
return alloc(bit_justication_constraint, c, std::move(dep));
|
||||
return alloc(bit_justification_constraint, s, c, std::move(dep));
|
||||
}
|
||||
static bit_justication_constraint* mk_binary(constraint* c, bvpos v1, bvpos v2) {
|
||||
static bit_justification_constraint* mk_binary(solver& s, constraint* c, bvpos v1, bvpos v2) {
|
||||
bit_dependencies dep;
|
||||
dep.push_back(std::move(v1));
|
||||
dep.push_back(std::move(v2));
|
||||
return alloc(bit_justication_constraint, c, std::move(dep));
|
||||
return alloc(bit_justification_constraint, s, c, std::move(dep));
|
||||
}
|
||||
static bit_justication_constraint* mk(constraint* c, const bit_dependencies& dep) { return alloc(bit_justication_constraint, c, dep); }
|
||||
static bit_justification_constraint* mk(solver& s, constraint* c, const bit_dependencies& dep) { return alloc(bit_justification_constraint, s, c, dep); }
|
||||
|
||||
// gives the highest bits such that they already enforce a value of "tbv" that is at least "val"
|
||||
static bit_justication_constraint* mk_justify_at_least(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least);
|
||||
static bit_justification_constraint* mk_justify_at_least(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& least);
|
||||
// similar to mk_justify_at_least: gives the highest bits such that they already enforce a value of "tbv" that is at most "val"
|
||||
static bit_justication_constraint* mk_justify_at_most(constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most);
|
||||
static bit_justification_constraint* mk_justify_at_most(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, const rational& most);
|
||||
// a combination of mk_justify_at_least and mk_justify_at_most
|
||||
static bit_justication_constraint* mk_justify_between(constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most);
|
||||
static bit_justification_constraint* mk_justify_between(solver& s, constraint *c, const pdd& v, const tbv_ref& tbv, rational least, rational most);
|
||||
|
||||
};
|
||||
|
||||
// lazy generation of the justifications. Generating them eagerly can generate a huge overhead
|
||||
class bit_justication_mul : public bit_justication {
|
||||
class bit_justification_mul : public bit_justification {
|
||||
|
||||
unsigned m_idx;
|
||||
optional<pdd> m_p, m_q, m_r;
|
||||
|
|
@ -156,10 +162,15 @@ namespace polysat {
|
|||
|
||||
public:
|
||||
|
||||
bit_justication_mul() = default;
|
||||
bit_justication_mul(unsigned idx, const pdd& p, const pdd& q) : m_idx(idx), m_p(p), m_q(q) {}
|
||||
bit_justication_mul(unsigned idx, const pdd& p, const pdd& q, const pdd& r) : m_idx(idx), m_p(p), m_q(q), m_r(r) {}
|
||||
|
||||
bit_justification_mul(unsigned idx, const pdd& p, const pdd& q, const pdd& r) : m_idx(idx), m_p(p), m_q(q), m_r(r) {
|
||||
// we can also track the decision level but multiplications are unpleasant anyway.
|
||||
// We prefer any other justification (Othw. take the max of all coefficients that influence the result)
|
||||
m_decision_level = UINT32_MAX;
|
||||
}
|
||||
bit_justification_mul(unsigned idx, const pdd& p, const pdd& q) : m_idx(idx), m_p(p), m_q(q) {
|
||||
m_decision_level = UINT32_MAX;
|
||||
}
|
||||
|
||||
// propagates from p, q => r (forward) and r, p/q => q/p (backward)
|
||||
static void propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd &p, const pdd &q);
|
||||
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
|
||||
|
|
@ -167,91 +178,172 @@ namespace polysat {
|
|||
void get_dependencies_backward(fixed_bits& fixed, bit_dependencies& to_process, const tbv_ref& p_tbv, const tbv_ref& q_tbv, unsigned relevant_range);
|
||||
};
|
||||
|
||||
class bit_justication_add : public bit_justication {
|
||||
class bit_justification_add : public bit_justification {
|
||||
|
||||
unsigned m_idx;
|
||||
optional<pdd> m_c1, m_c2;
|
||||
|
||||
public:
|
||||
|
||||
bit_justication_add() = default;
|
||||
bit_justication_add(unsigned idx, const pdd& c1, const pdd& c2) : m_idx(idx), m_c1(c1), m_c2(c2) {}
|
||||
bit_justification_add(unsigned lvl, unsigned idx, const pdd& c1, const pdd& c2) : m_idx(idx), m_c1(c1), m_c2(c2) {
|
||||
m_decision_level = lvl;
|
||||
}
|
||||
|
||||
static void propagate(solver& s, fixed_bits& fixed, const pdd& r, const pdd& p, const pdd& q);
|
||||
void get_dependencies(fixed_bits& fixed, bit_dependencies& to_process) override;
|
||||
};
|
||||
|
||||
struct justified_bvpos : public bvpos {
|
||||
bit_justication* m_justification;
|
||||
unsigned m_trail_pos;
|
||||
bit_justification* m_justification;
|
||||
|
||||
justified_bvpos() = default;
|
||||
|
||||
justified_bvpos(const pdd & pdd, unsigned idx, bit_justication* jstfc, unsigned int trail_pos) :
|
||||
bvpos(pdd, idx), m_justification(jstfc), m_trail_pos(trail_pos) {}
|
||||
justified_bvpos(const pdd & pdd, unsigned idx, bit_justification* jstfc) :
|
||||
bvpos(pdd, idx), m_justification(jstfc) {}
|
||||
|
||||
justified_bvpos(const bvpos& pos, bit_justication* jstfc, unsigned int trail_pos) :
|
||||
bvpos(pos), m_justification(jstfc), m_trail_pos(trail_pos) {}
|
||||
justified_bvpos(const bvpos& pos, bit_justification* jstfc) :
|
||||
bvpos(pos), m_justification(jstfc) {}
|
||||
|
||||
void set(bit_justification* new_justification){
|
||||
if (m_justification && m_justification->can_dealloc())
|
||||
dealloc(m_justification);
|
||||
m_justification = new_justification;
|
||||
}
|
||||
};
|
||||
|
||||
class bitvec_info {
|
||||
tbv_ref* m_bits = nullptr;
|
||||
justified_bvpos* m_justifications = nullptr; // do not alter this pointer (except setting it 0 for moving - we refer to it in trail)
|
||||
unsigned m_unset = 0; // For constant pdds this value is completely ignored/not maintained
|
||||
|
||||
public:
|
||||
|
||||
bitvec_info() = default;
|
||||
bitvec_info(tbv_ref* bits) : m_bits(bits), m_justifications(alloc_vect<justified_bvpos>(bits->num_tbits())), m_unset(bits->num_tbits()) {}
|
||||
bitvec_info(bitvec_info&& other) : m_bits(other.m_bits), m_justifications(other.m_justifications), m_unset(other.m_unset) {
|
||||
other.m_bits = nullptr;
|
||||
other.m_justifications = nullptr;
|
||||
}
|
||||
|
||||
bitvec_info& operator=(bitvec_info&& other) {
|
||||
m_bits = other.m_bits;
|
||||
m_justifications = other.m_justifications;
|
||||
m_unset = other.m_unset;
|
||||
|
||||
other.m_bits = nullptr;
|
||||
other.m_justifications = nullptr;
|
||||
return *this;
|
||||
}
|
||||
|
||||
~bitvec_info() {
|
||||
SASSERT((bool)m_bits == (bool)m_justifications);
|
||||
if (!m_bits)
|
||||
return;
|
||||
|
||||
unsigned cnt = num_tbits();
|
||||
for (unsigned i = 0; i < cnt; i++) {
|
||||
if (m_justifications[i].m_justification->can_dealloc())
|
||||
dealloc(m_justifications[i].m_justification);
|
||||
}
|
||||
dealloc_svect(m_justifications);
|
||||
dealloc(m_bits);
|
||||
}
|
||||
|
||||
bool is_determined() const {
|
||||
return m_unset == 0;
|
||||
};
|
||||
|
||||
unsigned num_tbits() const {
|
||||
return m_bits->num_tbits();
|
||||
}
|
||||
|
||||
void inc_unset() {
|
||||
SASSERT(m_unset < num_tbits());
|
||||
m_unset++;
|
||||
}
|
||||
|
||||
void dec_unset() {
|
||||
SASSERT(m_unset > 0);
|
||||
m_unset--;
|
||||
}
|
||||
|
||||
rational get_value() const {
|
||||
SASSERT(is_determined());
|
||||
rational value(0);
|
||||
unsigned cnt = num_tbits();
|
||||
for (unsigned i = cnt; i > 0; i--) {
|
||||
SASSERT((*m_bits)[i - 1] == BIT_0 || (*m_bits)[i - 1] == BIT_1);
|
||||
value *= 2;
|
||||
value += (*m_bits)[i - 1] == BIT_1;
|
||||
}
|
||||
return value;
|
||||
}
|
||||
|
||||
void set_bit(unsigned idx, tbit v) {
|
||||
SASSERT(v != BIT_x); // We don't use don't-cares
|
||||
m_bits->manager().set(**m_bits, idx, v);
|
||||
}
|
||||
|
||||
tbit get_bit(unsigned idx) const {
|
||||
return (*m_bits)[idx];
|
||||
}
|
||||
|
||||
const tbv_ref* get_tbv() const {
|
||||
return m_bits;
|
||||
}
|
||||
|
||||
justified_bvpos& justification(unsigned idx) {
|
||||
return m_justifications[idx];
|
||||
}
|
||||
|
||||
const justified_bvpos& justification(unsigned idx) const {
|
||||
return m_justifications[idx];
|
||||
}
|
||||
};
|
||||
|
||||
class fixed_bits final {
|
||||
|
||||
friend bit_justication;
|
||||
friend bit_justification;
|
||||
|
||||
solver& m_solver;
|
||||
scoped_ptr_vector<tbv_manager> m_tbv_managers;
|
||||
|
||||
using pdd_to_tbv_key = optional<pdd>;
|
||||
using pdd_to_tbv_eq = default_eq<pdd_to_tbv_key>;
|
||||
struct pdd_to_tbv_hash {
|
||||
unsigned operator()(pdd_to_tbv_key const& args) const {
|
||||
return args ? args->hash() : 0;
|
||||
|
||||
using pdd_to_info_eq = default_eq<optional<pdd>>;
|
||||
struct pdd_to_info_hash {
|
||||
unsigned operator()(optional<pdd> const& args) const {
|
||||
return args->hash();
|
||||
}
|
||||
};
|
||||
using pdd_to_tbv_map = map<pdd_to_tbv_key, tbv_ref*, pdd_to_tbv_hash, pdd_to_tbv_eq>;
|
||||
|
||||
using bvpos_to_justification_eq = default_eq<bvpos>;
|
||||
struct bvpos_to_justification_hash {
|
||||
unsigned operator()(bvpos const& args) const {
|
||||
return combine_hash(args.get_pdd().hash(), args.get_idx());
|
||||
}
|
||||
};
|
||||
using bvpos_to_justification_map = map<bvpos, justified_bvpos, bvpos_to_justification_hash, bvpos_to_justification_eq>;
|
||||
using pdd_to_info_map = map<optional<pdd>, bitvec_info, pdd_to_info_hash, pdd_to_info_eq>;
|
||||
|
||||
//vector<optional<tbv_ref>> m_var_to_tbv;
|
||||
pdd_to_tbv_map m_var_to_tbv;
|
||||
bvpos_to_justification_map m_bvpos_to_justification;
|
||||
pdd_to_info_map m_pdd_to_info;
|
||||
|
||||
svector<justified_bvpos> m_trail;
|
||||
svector<justified_bvpos*> m_trail;
|
||||
unsigned_vector m_trail_size;
|
||||
|
||||
bool m_consistent = true; // in case evaluating results in a bit-conflict
|
||||
|
||||
tbv_manager& get_manager(const pdd& v);
|
||||
tbv_manager& get_manager(const pdd& p);
|
||||
tbv_manager& get_manager(unsigned sz);
|
||||
|
||||
clause_ref get_explanation(solver& s, bit_justication* j1, bit_justication* j2);
|
||||
bool fix_value_core(const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j);
|
||||
bool fix_bit(solver& s, const pdd& p, tbv_ref& tbv, unsigned idx, tbit val, bit_justication* j);
|
||||
|
||||
bitvec_info& get_bit_info(const pdd& p);
|
||||
|
||||
clause_ref get_explanation(solver& s, bit_justification** js, unsigned cnt, bool free, signed_constraint* consequence);
|
||||
clause_ref get_explanation_assignment(solver& s, const pdd& p);
|
||||
clause_ref get_explanation_conflict(solver& s, bit_justification* j1, bit_justification* j2);
|
||||
clause_ref get_explanation_conflict(solver& s, bit_justification* j); // Conflict with constant
|
||||
bool fix_value_core(const pdd& p, bitvec_info& info, unsigned idx, tbit val, bit_justification* j);
|
||||
void clear_value(const pdd& p, unsigned idx);
|
||||
void replace_justification(const justified_bvpos& old_j, bit_justication* new_j);
|
||||
void replace_justification(justified_bvpos& jstfc, bit_justification* new_j);
|
||||
|
||||
void propagate_to_subterm(solver& s, const pdd& p);
|
||||
|
||||
public:
|
||||
|
||||
fixed_bits(solver& s) : m_solver(s) {}
|
||||
|
||||
~fixed_bits() {
|
||||
for (auto& tbv : m_var_to_tbv)
|
||||
dealloc(tbv.m_value);
|
||||
for (justified_bvpos& just : m_trail) {
|
||||
if (just.m_justification->can_dealloc())
|
||||
dealloc(just.m_justification);
|
||||
}
|
||||
}
|
||||
|
||||
tbv_ref* get_tbv(const pdd& p);
|
||||
fixed_bits(solver& s) : m_solver(s) {}
|
||||
|
||||
const tbv_ref* get_tbv(const pdd& p);
|
||||
|
||||
// #count [min; max]
|
||||
static std::pair<unsigned, unsigned> leading_zeros(const tbv_ref& ref);
|
||||
|
|
@ -262,11 +354,12 @@ namespace polysat {
|
|||
|
||||
tbit get_value(const pdd& p, unsigned idx); // More efficient than calling "eval" and accessing the returned tbv elements
|
||||
// call this function also if we already know that the correct value is written there. We might decrease the decision level (for "replay")
|
||||
bool fix_value(solver& s, const pdd& p, unsigned idx, tbit val, bit_justication* j);
|
||||
bool fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification** j, bool recursive);
|
||||
bool fix_bit(solver& s, const pdd& p, unsigned idx, tbit val, bit_justification* j, bool recursive);
|
||||
void push();
|
||||
void pop(unsigned pop_cnt = 1);
|
||||
|
||||
tbv_ref* eval(solver& s, const pdd& p);
|
||||
const tbv_ref* eval(solver& s, const pdd& p);
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue