mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

remove branch_bool

Browse source
This commit is contained in:
Jakob Rath 2022-01-17 15:57:05 +01:00
parent 3a34995b03
commit ebc4df1ece
5 changed files with 6 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/op_constraint.cpp
View file

@ -127,7 +127,6 @@ namespace polysat {
*
* We can assume that op_constraint is only asserted positive.
*/
void op_constraint::narrow(solver& s, bool is_positive) {
SASSERT(is_positive);

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

@ -51,7 +51,7 @@ namespace polysat {
m_assignment.push_back({p, r});
}
void search_state::pop_asssignment() {
void search_state::pop_assignment() {
m_assignment.pop_back();
}

2
src/math/polysat/search_state.h
View file

@ -66,7 +66,7 @@ namespace polysat {
void push_boolean(sat::literal lit);
void pop();
void pop_asssignment();
void pop_assignment();
void set_resolved(unsigned i) { m_items[i].set_resolved(); }

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

@ -48,7 +48,6 @@ namespace polysat {
void solver::updt_params(params_ref const& p) {
m_params.append(p);
m_branch_bool = m_params.get_bool("branch_bool", false);
m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
}
@ -394,10 +393,7 @@ namespace polysat {
void solver::decide() {
LOG_H2("Decide");
SASSERT(can_decide());
if (m_branch_bool && m_bvars.can_decide())
bdecide(m_bvars.next_var());
else
pdecide(m_free_pvars.next_var());
pdecide(m_free_pvars.next_var());
}
void solver::pdecide(pvar v) {
@ -423,10 +419,6 @@ namespace polysat {
}
}
void solver::bdecide(sat::bool_var b) {
decide_bool(sat::literal(b), nullptr);
}
void solver::assign_core(pvar v, rational const& val, justification const& j) {
if (j.is_decision())
++m_stats.m_num_decisions;
@ -485,7 +477,7 @@ namespace polysat {
// Resolve over variable assignment
pvar v = item.var();
if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
m_search.pop_asssignment();
m_search.pop_assignment();
continue;
}
inc_activity(v);
@ -494,7 +486,7 @@ namespace polysat {
revert_decision(v);
return;
}
m_search.pop_asssignment();
m_search.pop_assignment();
}
else {
// Resolve over boolean literal
@ -701,13 +693,6 @@ namespace polysat {
decide_bool(*lemma);
}
void solver::decide_bool(sat::literal lit, clause* lemma) {
SASSERT(!can_propagate());
SASSERT(!is_conflict());
push_level();
assign_decision(lit, lemma);
}
unsigned solver::level(sat::literal lit0, clause const& cl) {
unsigned lvl = base_level();
for (auto lit : cl) {

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

@ -94,9 +94,6 @@ namespace polysat {
uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max();
uint64_t m_max_decisions = std::numeric_limits<uint64_t>::max();
bool m_branch_bool = false;
// Per constraint state
constraint_manager m_constraints;
@ -177,7 +174,7 @@ namespace polysat {
void set_conflict(clause& cl) { m_conflict.set(cl); }
void set_conflict(pvar v) { m_conflict.set(v); }
bool can_decide() const { return !m_free_pvars.empty() || (m_branch_bool && m_bvars.can_decide()); }
bool can_decide() const { return !m_free_pvars.empty(); }
void decide();
void pdecide(pvar v);
void bdecide(sat::bool_var b);