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

set a throttle on ala

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-10 13:38:45 -08:00
parent 7fc349b622
commit b12c1b1cba
1 changed files with 2 additions and 3 deletions

5
src/sat/sat_simplifier.cpp
View file

@ -1272,7 +1272,8 @@ namespace sat {
* unless C contains lit, and it is a tautology.
*/
bool add_ala() {
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
unsigned init_size = m_covered_clause.size();
for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
literal l = m_covered_clause[m_ala_qhead];
for (watched & w : s.get_wlist(~l)) {
if (w.is_binary_non_learned_clause()) {
@ -1282,7 +1283,6 @@ namespace sat {
return true;
}
if (!s.is_marked(~lit)) {
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n");
m_covered_clause.push_back(~lit);
m_covered_antecedent.push_back(clause_ante(l, false));
s.mark_visited(~lit);
@ -1312,7 +1312,6 @@ namespace sat {
if (lit1 == null_literal) {
return true;
}
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n");
m_covered_clause.push_back(~lit1);
m_covered_antecedent.push_back(clause_ante(c));
s.mark_visited(~lit1);