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

undo unnecessary change

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-03-06 21:39:46 -08:00
parent 5c7506306b
commit b84f9694cd
4 changed files with 3 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -167,7 +167,6 @@ namespace polysat {
void conflict::reset() {
m_literals.reset();
m_vars.reset();
m_dep_literal = sat::null_literal;
m_var_occurrences.reset();
m_vars_occurring.reset();
m_lemmas.reset();
@ -185,21 +184,16 @@ namespace polysat {
return contains(lit) || contains(~lit);
}
void conflict::init_at_base_level(dependency dep, sat::literal lit) {
void conflict::init_at_base_level(dependency dep) {
SASSERT(empty());
SASSERT(s.at_base_level());
m_level = s.m_level;
m_dep = dep;
m_dep_literal = lit;
SASSERT(!empty());
// TODO: logger().begin_conflict???
// TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
}
void conflict::init_at_base_level(dependency dep) {
init_at_base_level(dep, sat::null_literal);
}
void conflict::init(signed_constraint c) {
LOG("Conflict: constraint " << lit_pp(s, c));
SASSERT(empty());
@ -590,9 +584,6 @@ namespace polysat {
}
}
}
if (m_dep_literal != sat::null_literal)
enqueue_lit(m_dep_literal);
for (unsigned d : deps)
out_deps.push_back(dependency(d));

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

@ -102,7 +102,6 @@ namespace polysat {
// Level at which the conflict was discovered
unsigned m_level = UINT_MAX;
dependency m_dep = null_dependency;
sat::literal m_dep_literal = sat::null_literal;
public:
conflict(solver& s);
@ -129,8 +128,6 @@ namespace polysat {
/** conflict due to obvious input inconsistency */
void init_at_base_level(dependency dep);
/** conflict due to obvious input inconsistency with literal */
void init_at_base_level(dependency dep, sat::literal lit);
/** conflict because the constraint c is false under current variable assignment */
void init(signed_constraint c);
/** boolean conflict with the given clause */

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

@ -180,7 +180,8 @@ namespace polysat {
if (m_bvars.is_false(lit)) {
// Input literal contradicts current boolean state (e.g., opposite literals in the input)
// => conflict only flags the inconsistency
set_conflict_at_base_level(dep, ~lit);
set_conflict_at_base_level(dep);
m_conflict.insert(~c);
return;
}
m_bvars.assumption(lit, m_level, dep);

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

@ -263,7 +263,6 @@ namespace polysat {
void propagate_clause(clause& cl);
void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
void set_conflict_at_base_level(dependency dep, sat::literal lit) { m_conflict.init_at_base_level(dep, lit); }
void set_conflict(signed_constraint c) { m_conflict.init(c); }
void set_conflict(clause& cl) { m_conflict.init(cl); }
void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }