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 unused code

Browse source
This commit is contained in:
Jakob Rath 2022-11-17 12:22:40 +01:00
parent 097454cf37
commit 00e8c53f9a
2 changed files with 3 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -491,13 +491,6 @@ namespace polysat {
clause_builder lemma(s);
#if 0
if (m_literals.size() == 1) {
auto c = *begin();
minimize_vars(c);
}
#endif
for (auto c : *this)
lemma.push(~c);
@ -533,6 +526,8 @@ namespace polysat {
return std::move(m_narrow_queue);
}
#if 0
// TODO: convert minimize_vars into a clause simplifier
bool conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())
return false;
@ -563,6 +558,7 @@ namespace polysat {
LOG("reduced " << m_vars);
return true;
}
#endif
std::ostream& conflict::display(std::ostream& out) const {
char const* sep = "";

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

@ -120,12 +120,6 @@ namespace polysat {
unsigned m_level = UINT_MAX;
void set_impl(signed_constraint c);
bool minimize_vars(signed_constraint c);
#if 0
void set_side_lemma(signed_constraint c, clause_ref lemma) { SASSERT(c); set_side_lemma(c.blit(), std::move(lemma)); }
void set_side_lemma(sat::literal lit, clause_ref lemma);
#endif
public:
conflict(solver& s);
@ -172,11 +166,6 @@ namespace polysat {
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
uint_set const& vars_occurring_in_constraints() const { return m_vars_occurring; }
#if 0
clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }
clause* side_lemma(sat::literal lit) const;
#endif
/**
* Insert constraint c into conflict state.
*
@ -196,16 +185,6 @@ namespace polysat {
void add_lemma(signed_constraint const* cs, size_t cs_len);
void add_lemma(clause_ref lemma);
#if 0
/**
* Derive new constraint c by bool-propagation from premises c1, ..., cn;
* as if c was unit-propagated by the lemma c1 /\ ... /\ cn ==> c.
* Does not add c to the conflict state.
*/
void bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len);
void bool_propagate(signed_constraint c, std::initializer_list<signed_constraint> premises);
#endif
/** Remove c from core */
void remove(signed_constraint c);
void remove_var(pvar v);