diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 999dbc2e0..bc28a7b37 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -443,8 +443,9 @@ private: // extract cubes. cubes.reset(); s.set_cube_params(); + unsigned cutoff = UINT_MAX; while (true) { - expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this + expr_ref_vector c = s.get_solver().cube(vars, cutoff); if (c.empty()) { report_undef(s); return; @@ -618,6 +619,11 @@ public: return pp.conquer_batch_size(); } + bool filter_cubes() const { + parallel_params pp(m_params); + return pp.filter_cubes(); + } + void cleanup() { m_queue.reset(); init(); diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg index 70c4ccdd0..58da305f4 100644 --- a/src/tactic/smtlogics/parallel_params.pyg +++ b/src/tactic/smtlogics/parallel_params.pyg @@ -7,4 +7,5 @@ def_module_params('parallel', ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'), ('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'), + ('filter_cubes', BOOL, False, 'filter cubes using a short running check'), ))