mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

Remove conflict::set

Browse source
This commit is contained in:
Jakob Rath 2022-12-16 14:25:41 +01:00
parent 06e6f27614
commit 3b3636b30e
2 changed files with 1 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -191,19 +191,6 @@ namespace polysat {
SASSERT(empty()); SASSERT(empty());
m_level = s.m_level; m_level = s.m_level;
m_narrow_queue.push_back(c.blit()); // if the conflict is only due to a missed propagation of c m_narrow_queue.push_back(c.blit()); // if the conflict is only due to a missed propagation of c
set_impl(c);
logger().begin_conflict();
}
#if 0
void conflict::set(signed_constraint c) {
SASSERT(!empty());
remove_all();
set_impl(c);
}
#endif
void conflict::set_impl(signed_constraint c) {
if (c.bvalue(s) == l_false) { if (c.bvalue(s) == l_false) {
// boolean conflict // boolean conflict
// This case should not happen: // This case should not happen:
@ -219,6 +206,7 @@ namespace polysat {
insert_vars(c); insert_vars(c);
} }
SASSERT(!empty()); SASSERT(!empty());
logger().begin_conflict();
} }
void conflict::init(clause const& cl) { void conflict::init(clause const& cl) {

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

@ -102,8 +102,6 @@ namespace polysat {
// Level at which the conflict was discovered // Level at which the conflict was discovered
unsigned m_level = UINT_MAX; unsigned m_level = UINT_MAX;
void set_impl(signed_constraint c);
public: public:
conflict(solver& s); conflict(solver& s);
~conflict(); ~conflict();
@ -138,11 +136,6 @@ namespace polysat {
/** conflict because there is no viable value for the variable v, by fallback solver */ /** conflict because there is no viable value for the variable v, by fallback solver */
void init_by_viable_fallback(pvar v, univariate_solver& us); void init_by_viable_fallback(pvar v, univariate_solver& us);
#if 0
/** replace the current conflict by a single constraint */
void set(signed_constraint c);
#endif
bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); } bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
bool contains(sat::literal lit) const; bool contains(sat::literal lit) const;
bool contains_pvar(pvar v) const { return m_vars.contains(v); } bool contains_pvar(pvar v) const { return m_vars.contains(v); }