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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-09 08:25:52 -08:00
parent 98a0f37eec
commit f3ac879fa4
4 changed files with 6 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/forbidden_intervals.cpp
View file

@ -73,9 +73,9 @@ namespace polysat {
if (p.is_val())
return;
else if (is_zero)
side_cond.push_back(s.m_constraints.eq(p));
side_cond.push_back(s.eq(p));
else
side_cond.push_back(~s.m_constraints.eq(p));
side_cond.push_back(~s.eq(p));
}
std::tuple<bool, rational, pdd, pdd> forbidden_intervals::linear_decompose(pvar v, pdd const& p, vector<signed_constraint>& out_side_cond) {

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

@ -393,7 +393,7 @@ namespace polysat {
void solver::decide() {
LOG_H2("Decide");
SASSERT(can_decide());
if (m_bvars.can_decide() && m_branch_bool)
if (m_branch_bool && m_bvars.can_decide())
bdecide(m_bvars.next_var());
else
pdecide(m_free_pvars.next_var());
@ -446,19 +446,6 @@ namespace polysat {
/**
* Conflict resolution.
* - m_conflict are constraints that are infeasible in the current assignment.
* 1. walk m_search from top down until last variable in m_conflict.
* 2. resolve constraints in m_cjust to isolate lowest degree polynomials
* using variable.
* Use Olm-Seidl division by powers of 2 to preserve invertibility.
* 3. resolve conflict with result of resolution.
* 4. If the resulting lemma is still infeasible continue, otherwise bail out
* and undo the last assignment by accumulating conflict trail (but without resolution).
* 5. When hitting the last decision, determine whether conflict polynomial is asserting,
* If so, apply propagation.
* 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune
* viable solutions by excluding the previous guess.
*
*/
void solver::resolve_conflict() {
LOG_H2("Resolve conflict");
@ -472,9 +459,7 @@ namespace polysat {
if (m_conflict.conflict_var() != null_var) {
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));
// TBD: make sure last value decision is blocked by this conflict.
// A conflict in test_l5 reverts v1 = 2 more than once.
VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));
}
search_iterator search_it(m_search);
@ -491,8 +476,7 @@ namespace polysat {
continue;
}
justification& j = m_justification[v];
LOG("Justification: " << j);
if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) {
if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
revert_decision(v);
return;
}
@ -520,11 +504,6 @@ namespace polysat {
report_unsat();
}
/** Conflict resolution case where propagation 'v := ...' is on top of the stack */
bool solver::resolve_value(pvar v) {
return m_conflict.resolve_value(v);
}
/**
* Variable activity accounting.
* As a placeholder we increment activity

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

@ -184,7 +184,6 @@ namespace polysat {
unsigned base_level() const;
void resolve_conflict();
bool resolve_value(pvar v);
void resolve_bool(sat::literal lit);
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);

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

@ -187,7 +187,7 @@ namespace polysat {
// pass
}
else if (e->interval.lo_val() <= coeff_val) {
rational lambda_u = floor((max_value - coeff_val - 1) / e->coeff);
rational lambda_u = floor((max_value - coeff_val) / e->coeff);
hi = val + lambda_u + 1;
if (hi > max_value)
hi = 0;