mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 03:42:04 +00:00
Code Activity

throttle number of rounds of ba simplification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-22 18:12:39 -08:00
parent f9195c77a7
commit 412eee0dac
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/ba_solver.cpp
View file

@ -2837,7 +2837,7 @@ namespace sat {
void ba_solver::simplify() { void ba_solver::simplify() {
if (!s().at_base_lvl()) s().pop_to_base_level(); if (!s().at_base_lvl()) s().pop_to_base_level();
unsigned trail_sz; unsigned trail_sz, count = 0;
do { do {
trail_sz = s().init_trail_size(); trail_sz = s().init_trail_size();
m_simplify_change = false; m_simplify_change = false;
@ -2855,8 +2855,9 @@ namespace sat {
cleanup_clauses(); cleanup_clauses();
cleanup_constraints(); cleanup_constraints();
update_pure(); update_pure();
++count;
} }
while (m_simplify_change || trail_sz < s().init_trail_size()); while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
IF_VERBOSE(1, verbose_stream() << "(ba.simplify" IF_VERBOSE(1, verbose_stream() << "(ba.simplify"
<< " :vars " << s().num_vars() - trail_sz << " :vars " << s().num_vars() - trail_sz