mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

deps

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-05 07:44:36 -07:00
parent 9d5349ff10
commit 40027df32f
2 changed files with 28 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/math/polysat/fixplex.h
View file

@ -26,13 +26,15 @@ Author:
#include "util/rational.h"
#include "util/lbool.h"
#include "util/uint_set.h"
#include "util/dependency.h"
#include "util/ref.h"
inline rational to_rational(uint64_t n) { return rational(n, rational::ui64()); }
namespace polysat {
typedef unsigned var_t;
struct fixplex_base {
virtual ~fixplex_base() {}
virtual lbool make_feasible() = 0;
@ -93,12 +95,20 @@ namespace polysat {
S_DEFAULT
};
#if 0
struct dep_config {
static const bool ref_count = true;
typedef unsigned value;
};
typedef dependency_manager<dep_config> dep_manager;
#endif
struct var_info : public mod_interval<numeral> {
unsigned m_base2row:29;
unsigned m_is_base:1;
numeral m_value = 0;
unsigned m_lo_dep = UINT_MAX;
unsigned m_hi_dep = UINT_MAX;
unsigned m_base2row:29;
unsigned m_is_base:1;
numeral m_value = 0;
u_dependency* m_lo_dep = nullptr;
u_dependency* m_hi_dep = nullptr;
var_info():
m_base2row(0),
m_is_base(false)
@ -164,6 +174,7 @@ namespace polysat {
unsigned_vector m_base_vars;
stats m_stats;
vector<stashed_bound> m_stashed_bounds;
u_dependency_manager m_deps;
map<numeral, fix_entry, typename manager::hash, typename manager::eq> m_value2fixed_var;
// inequalities

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

@ -490,9 +490,9 @@ namespace polysat {
auto hi0 = m_vars[v].hi;
m_vars[v] &= mod_interval(l, h);
if (lo0 != m_vars[v].lo)
m_vars[v].m_lo_dep = dep;
m_vars[v].m_lo_dep = nullptr; // TODO set_atom(dep);
if (hi0 != m_vars[v].hi)
m_vars[v].m_hi_dep = dep;
m_vars[v].m_hi_dep = nullptr; // TODO .set_atom(dep);
if (in_bounds(v))
return;
if (is_base(v))
@ -523,11 +523,15 @@ namespace polysat {
template<typename Ext>
void fixplex<Ext>::restore_bound() {
auto const& b = m_stashed_bounds.back();
auto& b = m_stashed_bounds.back();
auto* lo = m_vars[b.m_var].m_lo_dep;
auto* hi = m_vars[b.m_var].m_hi_dep;
m_vars[b.m_var].lo = b.lo;
m_vars[b.m_var].hi = b.hi;
m_vars[b.m_var].m_lo_dep = b.m_lo_dep;
m_vars[b.m_var].m_hi_dep = b.m_hi_dep;
// m_deps.dec_ref(lo);
// m_deps.dec_ref(hi);
m_stashed_bounds.pop_back();
}
@ -799,15 +803,13 @@ namespace polysat {
m_unsat_core.reset();
SASSERT(is_base(v));
auto row = base2row(v);
ptr_vector<u_dependency> todo;
for (auto const& e : M.row_entries(row)) {
var_t v = e.var();
auto lo = m_vars[v].m_lo_dep;
auto hi = m_vars[v].m_hi_dep;
if (lo != UINT_MAX)
m_unsat_core.push_back(lo);
if (hi != UINT_MAX)
m_unsat_core.push_back(hi);
todo.push_back(m_vars[v].m_lo_dep);
todo.push_back(m_vars[v].m_hi_dep);
}
m_deps.linearize(todo, m_unsat_core);
}
/**