mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

slicing interface

Browse source
This commit is contained in:
Jakob Rath 2023-07-12 15:56:27 +02:00
parent 1d3a31c323
commit d8d8c67a3b
3 changed files with 25 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/slicing.cpp
View file

@ -652,7 +652,7 @@ namespace polysat {
return m_solver.var(v); return m_solver.var(v);
} }
void slicing::propagate(signed_constraint c) { void slicing::add_constraint(signed_constraint c) {
// TODO: evaluate under current assignment? // TODO: evaluate under current assignment?
if (!c->is_eq()) if (!c->is_eq())
return; return;
@ -691,7 +691,7 @@ namespace polysat {
} }
} }
void slicing::propagate(pvar v) { void slicing::add_value(pvar v, rational const& value) {
// go through all existing nodes, and evaluate v? // go through all existing nodes, and evaluate v?
// can do that externally // can do that externally
} }

20
src/math/polysat/slicing.h
View file

@ -222,6 +222,9 @@ namespace polysat {
bool invariant() const; bool invariant() const;
/** Get variable representing x[hi:lo] */
pvar mk_extract_var(pvar x, unsigned hi, unsigned lo);
public: public:
slicing(solver& s); slicing(solver& s);
@ -230,9 +233,6 @@ namespace polysat {
void add_var(unsigned bit_width); void add_var(unsigned bit_width);
/** Get variable representing x[hi:lo] */
pvar mk_extract_var(pvar x, unsigned hi, unsigned lo);
/** Create expression for x[hi:lo] */ /** Create expression for x[hi:lo] */
pdd mk_extract(pvar x, unsigned hi, unsigned lo); pdd mk_extract(pvar x, unsigned hi, unsigned lo);
@ -242,12 +242,14 @@ namespace polysat {
/** Create expression for p ++ q */ /** Create expression for p ++ q */
pdd mk_concat(pdd const& p, pdd const& q); pdd mk_concat(pdd const& p, pdd const& q);
// propagate: // Track value assignments to variables (and propagate to subslices)
// - value assignments // (could generalize to fixed bits, then we need a way to merge interpreted enodes)
// - fixed bits void add_value(pvar v, rational const& value);
// - intervals ????? -- that will also need changes in the viable algorithm void add_constraint(signed_constraint c);
void propagate(pvar v);
void propagate(signed_constraint c); // TODO:
// Query for a given variable v:
// - set of variables that share at least one slice with v (need variable, offset/width relative to v)
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display(std::ostream& out, slice s) const; std::ostream& display(std::ostream& out, slice s) const;

12
src/math/polysat/solver.cpp
View file

@ -305,6 +305,18 @@ namespace polysat {
set_conflict(c); set_conflict(c);
} }
} }
else if (slicing_qhead < m_search.size()) {
auto const& item = m_search[slicing_qhead++];
if (item.is_assignment()) {
pvar const v = item.var();
m_slicing.add_value(v, get_value(v));
}
else {
SASSERT(item.is_boolean());
signed_constraint const c = lit2cnstr(item.lit());
m_slicing.add_constraint(c);
}
}
else { else {
// Third priority: activate/narrow // Third priority: activate/narrow
auto const& item = m_search[m_qhead++]; auto const& item = m_search[m_qhead++];