mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

more viable scaffolding

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-22 20:55:56 -07:00
parent 8f0c408c0a
commit b9719768a0
2 changed files with 17 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -157,7 +157,7 @@ namespace polysat {
#if POLYSAT_LOGGING_ENABLED #if POLYSAT_LOGGING_ENABLED
void viable::log() { void viable::log() {
// only for small problems // only for small problems
for (pvar v = 0; v < std::min(10u, m_viable.size()); ++v) for (pvar v = 0; v < std::min(10u, m_viable_bdd.size()); ++v)
log(v); log(v);
} }

21
src/math/polysat/viable.h
View file

@ -30,6 +30,9 @@ namespace polysat {
// replace BDDs by viable sets that emulate affine relations. // replace BDDs by viable sets that emulate affine relations.
// viable_set has an interval of feasible values. // viable_set has an interval of feasible values.
// it also can use ternary bit-vectors. // it also can use ternary bit-vectors.
// or we could also just use a vector of lbool instead of ternary bit-vectors
// updating them at individual positions is relatively cheap instead of copying the
// vectors every time a range is narrowed.
// //
class viable_set : public mod_interval<rational> { class viable_set : public mod_interval<rational> {
unsigned m_num_bits; unsigned m_num_bits;
@ -49,16 +52,17 @@ namespace polysat {
}; };
class viable { class viable {
typedef dd::bdd bdd;
solver& s; solver& s;
#if NEW_VIABLE
vector<viable_set> m_viable; // future representation of viable values
#else
typedef dd::bdd bdd;
dd::bdd_manager m_bdd; dd::bdd_manager m_bdd;
scoped_ptr_vector<dd::fdd> m_bits; scoped_ptr_vector<dd::fdd> m_bits;
vector<bdd> m_viable_bdd; // set of viable values. vector<bdd> m_viable_bdd; // set of viable values.
vector<std::pair<pvar, bdd>> m_viable_trail; vector<std::pair<pvar, bdd>> m_viable_trail;
vector<viable_set> m_viable; // future representation of viable values
/** /**
* Register all values that are not contained in vals as non-viable. * Register all values that are not contained in vals as non-viable.
*/ */
@ -67,18 +71,25 @@ namespace polysat {
dd::bdd_manager& get_bdd() { return m_bdd; } dd::bdd_manager& get_bdd() { return m_bdd; }
dd::fdd const& sz2bits(unsigned sz); dd::fdd const& sz2bits(unsigned sz);
dd::fdd const& var2bits(pvar v); dd::fdd const& var2bits(pvar v);
#endif
public: public:
viable(solver& s); viable(solver& s);
void push(unsigned num_bits) { void push(unsigned num_bits) {
m_viable_bdd.push_back(m_bdd.mk_true()); #if NEW_VIABLE
m_viable.push_back(viable_set(num_bits)); m_viable.push_back(viable_set(num_bits));
#else
m_viable_bdd.push_back(m_bdd.mk_true());
#endif
} }
void pop() { void pop() {
m_viable_bdd.pop_back(); #if NEW_VIABLE
m_viable.pop_back(); m_viable.pop_back();
#else
m_viable_bdd.pop_back();
#endif
} }
void push_viable(pvar v); void push_viable(pvar v);