mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

refactor

Browse source
This commit is contained in:
Jakob Rath 2022-12-16 14:22:50 +01:00
parent 9f05f645c1
commit 06e6f27614
6 changed files with 41 additions and 77 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/math/polysat/conflict.cpp
View file

@ -186,13 +186,6 @@ namespace polysat {
// TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
}
void conflict::init_empty() {
SASSERT(empty());
m_level = s.m_level;
SASSERT(!empty());
// TODO: logger().begin_conflict???
}
void conflict::init(signed_constraint c) {
LOG("Conflict: constraint " << lit_pp(s, c));
SASSERT(empty());
@ -241,32 +234,24 @@ namespace polysat {
logger().begin_conflict();
}
void conflict::init(pvar v, bool by_viable_fallback) {
LOG("Conflict: viable v" << v);
void conflict::init_by_viable_interval(pvar v) {
LOG("Conflict: viable_interval v" << v);
SASSERT(empty());
SASSERT(!s.is_assigned(v));
m_level = s.m_level;
if (by_viable_fallback) {
logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v));
// Conflict detected by viable fallback:
// initial conflict is the unsat core of the univariate solver,
// and the assignment (under which the constraints are univariate in v)
// TODO:
// - currently we add variables directly, which is sound:
// e.g.: v^2 + w^2 == 0; w := 1
// - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
// e.g.: v^2 + w^2 == 0; w^2 == 1
signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
for (auto c : unsat_core) {
insert(c);
insert_vars(c);
}
SASSERT(!m_vars.contains(v));
}
else {
logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
VERIFY(s.m_viable.resolve(v, *this));
}
logger().begin_conflict(header_with_var("viable_interval v", v));
VERIFY(s.m_viable.resolve_interval(v, *this));
SASSERT(!empty());
revert_pvar(v); // at this point, v is not assigned
}
void conflict::init_by_viable_fallback(pvar v, univariate_solver& us) {
LOG("Conflict: viable_fallback v" << v);
SASSERT(empty());
SASSERT(!s.is_assigned(v));
m_level = s.m_level;
logger().begin_conflict(header_with_var("viable_fallback v", v));
VERIFY(s.m_viable.resolve_fallback(v, us, *this));
SASSERT(!empty());
revert_pvar(v); // at this point, v is not assigned
}

8
src/math/polysat/conflict.h
View file

@ -133,10 +133,10 @@ namespace polysat {
void init(signed_constraint c);
/** boolean conflict with the given clause */
void init(clause const& cl);
/** conflict because there is no viable value for the variable v */
void init(pvar v, bool by_viable_fallback);
/** start empty conflict, constraints to be added by caller */
void init_empty(); // TODO: remove... rather have all types of conflicts explicitly listed here.
/** conflict because there is no viable value for the variable v, by interval reasoning */
void init_by_viable_interval(pvar v);
/** conflict because there is no viable value for the variable v, by fallback solver */
void init_by_viable_fallback(pvar v, univariate_solver& us);
#if 0
/** replace the current conflict by a single constraint */

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

@ -751,7 +751,7 @@ namespace polysat {
case find_t::empty:
LOG("Fallback solver: unsat");
m_free_pvars.unassign_var_eh(v);
set_conflict(v, true);
SASSERT(is_conflict());
return;
case find_t::resource_out:
UNREACHABLE(); // TODO: abort solving

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

@ -247,7 +247,8 @@ namespace polysat {
void set_conflict_at_base_level() { m_conflict.init_at_base_level(); }
void set_conflict(signed_constraint c) { m_conflict.init(c); }
void set_conflict(clause& cl) { m_conflict.init(cl); }
void set_conflict(pvar v, bool by_viable_fallback) { m_conflict.init(v, by_viable_fallback); }
void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }
void set_conflict_by_viable_fallback(pvar v, univariate_solver& us) { m_conflict.init_by_viable_fallback(v, us); }
bool can_decide() const;
bool can_bdecide() const;

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

@ -622,7 +622,7 @@ namespace polysat {
if (!e)
return l_true;
if (e->interval.is_full()) {
set_interval_conflict(v);
s.set_conflict_by_viable_interval(v);
return l_false;
}
@ -653,7 +653,7 @@ namespace polysat {
while (e != first);
if (e->interval.currently_contains(lo)) {
set_interval_conflict(v);
s.set_conflict_by_viable_interval(v);
return l_false;
}
@ -748,7 +748,7 @@ namespace polysat {
switch (us->check()) {
case l_false:
set_fallback_conflict(v, *us);
s.set_conflict_by_viable_fallback(v, *us);
return l_false;
case l_true:
// At this point we don't know much because we did not add all relevant constraints
@ -770,7 +770,7 @@ namespace polysat {
switch (us->check()) {
case l_false:
set_fallback_conflict(v, *us);
s.set_conflict_by_viable_fallback(v, *us);
return l_false;
case l_true:
// pass solver to mode-specific query
@ -814,11 +814,7 @@ namespace polysat {
return us.find_max(hi) ? l_true : l_undef;
}
void viable::set_fallback_conflict(pvar v, univariate_solver& us) {
SASSERT(!s.is_assigned(v));
conflict& core = s.m_conflict;
core.init_empty();
core.logger().begin_conflict(); //header_with_var("unsat core from viable fallback for v", v)); // TODO: begin_conflict before or after adding constraints?
bool viable::resolve_fallback(pvar v, univariate_solver& us, conflict& core) {
// The conflict is the unsat core of the univariate solver,
// and the current assignment (under which the constraints are univariate in v)
// TODO:
@ -834,19 +830,10 @@ namespace polysat {
}
SASSERT(!core.vars().contains(v));
core.add_lemma("viable unsat core", core.build_lemma());
core.revert_pvar(v); // at this point, v is not assigned
return true;
}
void viable::set_interval_conflict(pvar v) {
SASSERT(!s.is_assigned(v));
conflict& core = s.m_conflict;
core.init_empty();
core.logger().begin_conflict(); //header_with_var("forbidden interval lemma for v", v));
VERIFY(resolve(v, core)); // TODO: merge?
core.revert_pvar(v); // at this point, v is not assigned
}
bool viable::resolve(pvar v, conflict& core) {
bool viable::resolve_interval(pvar v, conflict& core) {
DEBUG_CODE( log(v); );
if (has_viable(v))
return false;
@ -1075,8 +1062,9 @@ namespace polysat {
auto const& cs = m_constraints[v];
for (unsigned i = cs.size(); i-- > 0; ) {
LOG("Univariate constraint: " << cs[i]);
cs[i].add_to_univariate_solver(s, *us, i);
signed_constraint const c = cs[i];
LOG("Univariate constraint: " << c);
c.add_to_univariate_solver(s, *us, c.blit().to_uint());
}
switch (us->check()) {
@ -1085,22 +1073,13 @@ namespace polysat {
// we don't know whether the SMT instance has a unique solution
return find_t::multiple;
case l_false:
s.set_conflict_by_viable_fallback(v, *us);
return find_t::empty;
default:
return find_t::resource_out;
}
}
signed_constraints viable_fallback::unsat_core(pvar v) {
unsigned bit_width = s.m_size[v];
SASSERT(m_usolver[bit_width]);
signed_constraints cs;
for (unsigned dep : m_usolver[bit_width]->unsat_core()) {
cs.push_back(m_constraints[v][dep]);
}
return cs;
}
std::ostream& operator<<(std::ostream& out, find_t x) {
switch (x) {
case find_t::empty:

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

@ -136,12 +136,6 @@ namespace polysat {
template <viable_query::query_t mode>
lbool query_fallback(pvar v, typename viable_query::query_result<mode>::result_t& out_result);
/** Set viable conflict due to interval cover */
void set_interval_conflict(pvar v);
/** Set viable conflict due to fallback solver */
void set_fallback_conflict(pvar v, univariate_solver& us);
public:
viable(solver& s);
@ -204,9 +198,15 @@ namespace polysat {
/**
* Retrieve the unsat core for v,
* and add the forbidden interval lemma for v (which eliminates v from the unsat core).
* \pre there are no viable values for v
* \pre there are no viable values for v (determined by interval reasoning)
*/
bool resolve(pvar v, conflict& core);
bool resolve_interval(pvar v, conflict& core);
/**
* Retrieve the unsat core for v.
* \pre there are no viable values for v (determined by fallback solver)
*/
bool resolve_fallback(pvar v, univariate_solver& us, conflict& core);
/** Log all viable values for the given variable.
* (Inefficient, but useful for debugging small instances.)
@ -347,7 +347,6 @@ namespace polysat {
signed_constraint find_violated_constraint(assignment const& a, pvar v);
find_t find_viable(pvar v, rational& out_val);
signed_constraints unsat_core(pvar v);
};
}