mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Remove unnecessary argument

Browse source
This commit is contained in:
Jakob Rath 2022-11-07 14:04:28 +01:00
parent a1736473a4
commit 586ffdf402
4 changed files with 19 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -600,7 +600,7 @@ namespace polysat {
if (needs_side_lemma(lit2))
todo.push_back(lit2);
// Store and bool-propagate the lemma
s.m_constraints.store(lemma, s, false);
s.m_constraints.store(lemma, false);
SASSERT(s.m_bvars.value(lit) != l_undef);
}
m_lemmas.reset();

20
src/math/polysat/constraint_manager.cpp
View file

@ -68,15 +68,15 @@ namespace polysat {
}
void constraint_manager::register_clause(clause* cl, solver& s) {
void constraint_manager::register_clause(clause* cl) {
while (m_clauses.size() <= s.base_level())
m_clauses.push_back({});
m_clauses[s.base_level()].push_back(cl);
}
void constraint_manager::store(clause* cl, solver& s, bool value_propagate) {
register_clause(cl, s);
watch(*cl, s, value_propagate);
void constraint_manager::store(clause* cl, bool value_propagate) {
register_clause(cl);
watch(*cl, value_propagate);
}
// Release constraints at the given level and above.
@ -94,7 +94,7 @@ namespace polysat {
// if clause is unsat then assign arbitrary
// solver handles unsat clauses by creating a conflict.
// solver also can propagate, but need to check that it does indeed.
void constraint_manager::watch(clause& cl, solver& s, bool value_propagate) {
void constraint_manager::watch(clause& cl, bool value_propagate) {
if (cl.empty())
return;
@ -168,18 +168,18 @@ namespace polysat {
}
}
void constraint_manager::gc(solver& s) {
void constraint_manager::gc() {
LOG_H1("gc");
gc_clauses(s);
gc_constraints(s);
gc_clauses();
gc_constraints();
}
void constraint_manager::gc_clauses(solver& s) {
void constraint_manager::gc_clauses() {
LOG_H3("gc_clauses");
// place to gc redundant clauses
}
void constraint_manager::gc_constraints(solver& s) {
void constraint_manager::gc_constraints() {
LOG_H3("gc_constraints");
uint_set used_vars;
for (auto const& cls : m_clauses)

12
src/math/polysat/constraint_manager.h
View file

@ -63,13 +63,13 @@ namespace polysat {
constraint* dedup(constraint* c);
void gc_constraints(solver& s);
void gc_clauses(solver& s);
void gc_constraints();
void gc_clauses();
void watch(clause& cl, solver& s, bool value_propagate);
void watch(clause& cl, bool value_propagate);
void unwatch(clause& cl);
void register_clause(clause* cl, solver& s);
void register_clause(clause* cl);
void ensure_bvar(constraint* c);
void erase_bvar(constraint* c);
@ -78,13 +78,13 @@ namespace polysat {
constraint_manager(solver& s);
~constraint_manager();
void store(clause* cl, solver& s, bool value_propagate);
void store(clause* cl, bool value_propagate);
/// Release clauses at the given level and above.
void release_level(unsigned lvl);
/// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable).
void gc(solver& s);
void gc();
bool should_gc();
constraint* lookup(sat::bool_var var) const;

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

@ -73,7 +73,7 @@ namespace polysat {
else if (is_conflict()) resolve_conflict();
else if (can_propagate()) propagate();
else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
else if (m_constraints.should_gc()) m_constraints.gc(*this);
else if (m_constraints.should_gc()) m_constraints.gc();
else if (m_simplify.should_apply()) m_simplify();
else if (m_restart.should_apply()) m_restart();
else decide();
@ -1006,7 +1006,7 @@ namespace polysat {
}
}
SASSERT(!clause.empty());
m_constraints.store(&clause, *this, true);
m_constraints.store(&clause, true);
if (!clause.is_redundant()) {
// for (at least) non-redundant clauses, we also need to watch the constraints