mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-25 16:37:25 -08:00
parent 4f60dd7f3a
commit f51e200dd8
2 changed files with 45 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/sat/smt/polysat/viable.cpp
View file

@ -93,14 +93,6 @@ namespace polysat {
} }
} }
void viable::init_fixed_bits(pvar v) {
#if 0
if (!collect_bit_information(v, true, fbi))
return; // conflict already added
#endif
}
void viable::init_overlaps(pvar v) { void viable::init_overlaps(pvar v) {
m_widths.reset(); m_widths.reset();
m_overlaps.reset(); m_overlaps.reset();
@ -121,19 +113,17 @@ namespace polysat {
LOG("widths: " << m_widths); LOG("widths: " << m_widths);
} }
lbool viable::next_viable(pvar, rational& val1) {
return l_undef;
}
lbool viable::find_viable(pvar v, rational& val1, rational& val2) { lbool viable::find_viable(pvar v, rational& val1, rational& val2) {
m_explain.reset(); m_explain.reset();
m_var = v;
m_num_bits = c.size(v);
m_fixed_bits.reset(v); m_fixed_bits.reset(v);
init_overlaps(v); init_overlaps(v);
rational const& max_value = c.var2pdd(v).max_value(); rational const& max_value = c.var2pdd(v).max_value();
val1 = 0; val1 = 0;
lbool r = next_viable(v, val1); lbool r = next_viable(val1);
if (r != l_true) if (r != l_true)
return r; return r;
@ -143,7 +133,7 @@ namespace polysat {
} }
val2 = val1 + 1; val2 = val1 + 1;
r = next_viable(v, val2); r = next_viable(val2);
if (r != l_false) if (r != l_false)
return r; return r;
@ -151,6 +141,42 @@ namespace polysat {
return l_true; return l_true;
} }
//
// Alternate next viable unit and next fixed until convergence.
// Check the non-units
// Refine?
//
lbool viable::next_viable(rational& val) {
rational val0;
do {
auto r = next_viable_unit(val);
if (r != l_true)
return r;
val0 = val;
if (!m_fixed_bits.next(val))
return l_false;
}
while (val0 != val);
NOT_IMPLEMENTED_YET();
// non-units
return l_undef;
}
//
// iterate over smallest layers to largest
// iterate over smallest overlap to largest
//
lbool viable::next_viable_unit(rational& val) {
return l_undef;
}
// By layer:
// var, width := w layer-width := k
// layer entry means: 2^{w-k}* x not in [lo, hi[
// check if 2^{w-k}* val in [lo, hi[
// if so, then increment val such that 2^{w-k}* val' not in [lo, hi[
//
/* /*
* Explain why the current variable is not viable or signleton. * Explain why the current variable is not viable or signleton.
*/ */

8
src/sat/smt/polysat/viable.h
View file

@ -133,11 +133,13 @@ namespace polysat {
lbool find_viable(pvar v, rational& val1, rational& val2); lbool find_viable(pvar v, rational& val1, rational& val2);
lbool next_viable(pvar, rational& val1); lbool next_viable(rational& val);
fixed_bits m_fixed_bits; lbool next_viable_unit(rational& val);
void init_fixed_bits(pvar v);
pvar m_var = null_var;
unsigned m_num_bits = 0;
fixed_bits m_fixed_bits;
unsigned_vector m_widths; unsigned_vector m_widths;
offset_slices m_overlaps; offset_slices m_overlaps;
void init_overlaps(pvar v); void init_overlaps(pvar v);