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

fix refcount issue

Browse source
This commit is contained in:
Jakob Rath 2022-03-19 04:19:16 +01:00
parent d41d3fa6ea
commit 613b0db4cc
3 changed files with 14 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/boolean.h
View file

@ -100,10 +100,11 @@ namespace polysat {
friend std::ostream& operator<<(std::ostream& out, kind_t const& k) { friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
switch (k) { switch (k) {
case kind_t::unassigned: return out << "unassigned"; case kind_t::unassigned: return out << "unassigned";
case kind_t::bool_propagation: return out << "bool propagation"; case kind_t::bool_propagation: return out << "bool propagation";
case kind_t::value_propagation: return out << "value propagation"; case kind_t::value_propagation: return out << "value propagation";
case kind_t::decision: return out << "decision"; case kind_t::decision: return out << "decision";
case kind_t::assumption: return out << "assumption";
default: UNREACHABLE(); return out; default: UNREACHABLE(); return out;
} }
} }

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

@ -513,15 +513,18 @@ namespace polysat {
m_search.pop(); m_search.pop();
m_justification[v] = justification::unassigned(); m_justification[v] = justification::unassigned();
if (!is_valid) { if (!is_valid) {
LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
// Try to find a valid replacement value // Try to find a valid replacement value
switch (m_viable_fallback.find_viable(v, val)) { switch (m_viable_fallback.find_viable(v, val)) {
case dd::find_t::singleton: case dd::find_t::singleton:
case dd::find_t::multiple: case dd::find_t::multiple:
LOG("Fallback solver: " << assignment_pp(*this, v, val));
// NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives. // NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives.
SASSERT(!j.is_propagation()); SASSERT(!j.is_propagation());
j = justification::decision(m_level + 1); j = justification::decision(m_level + 1);
break; break;
case dd::find_t::empty: case dd::find_t::empty:
LOG("Fallback solver: unsat");
m_free_pvars.unassign_var_eh(v); m_free_pvars.unassign_var_eh(v);
auto core = m_viable_fallback.unsat_core(v); // TODO: add constraints from unsat_core to conflict auto core = m_viable_fallback.unsat_core(v); // TODO: add constraints from unsat_core to conflict
set_conflict(v); set_conflict(v);

10
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -29,17 +29,19 @@ namespace polysat {
class univariate_bitblast_solver : public univariate_solver { class univariate_bitblast_solver : public univariate_solver {
// TODO: does it make sense to share m and bv between different solver instances? // TODO: does it make sense to share m and bv between different solver instances?
// TODO: consider pooling solvers to save setup overhead, see if solver/solver_pool.h can be used
ast_manager m; ast_manager m;
scoped_ptr<bv_util> bv; scoped_ptr<bv_util> bv;
scoped_ptr<solver> s; scoped_ptr<solver> s;
unsigned bit_width; unsigned bit_width;
func_decl* x_decl; func_decl_ref x_decl;
expr* x; expr_ref x;
public: public:
univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) : univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
bit_width(bit_width) bit_width(bit_width),
{ x_decl(m),
x(m) {
// m.register_plugin(symbol("bv"), alloc(bv_decl_plugin)); // this alone doesn't work // m.register_plugin(symbol("bv"), alloc(bv_decl_plugin)); // this alone doesn't work
reg_decl_plugins(m); reg_decl_plugins(m);
bv = alloc(bv_util, m); bv = alloc(bv_util, m);