mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

unused for now

Browse source
This commit is contained in:
Jakob Rath 2022-08-04 13:50:35 +02:00
parent a3e8124245
commit c67024d88b
2 changed files with 0 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -927,7 +927,6 @@ namespace polysat {
m_conflict.reset(); m_conflict.reset();
backjump(get_level(v) - 1); backjump(get_level(v) - 1);
learn_lemma(*lemma); learn_lemma(*lemma);
narrow(v);
} }
} }
@ -1052,15 +1051,6 @@ namespace polysat {
pop_levels(m_level - new_level); pop_levels(m_level - new_level);
} }
/**
* placeholder for factoring/gcd common factors
*/
void solver::narrow(pvar v) {
if (is_conflict())
return;
// TODO
}
// Add lemma to storage // Add lemma to storage
void solver::add_clause(clause& clause) { void solver::add_clause(clause& clause) {
LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);

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

@ -198,7 +198,6 @@ namespace polysat {
void decide(); void decide();
void pdecide(pvar v); void pdecide(pvar v);
void narrow(pvar v);
void linear_propagate(); void linear_propagate();