mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

add filter cubes parameter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-13 17:03:49 -07:00
parent a3e651156a
commit c5a30285a8
2 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -443,8 +443,9 @@ private:
// extract cubes. // extract cubes.
cubes.reset(); cubes.reset();
s.set_cube_params(); s.set_cube_params();
unsigned cutoff = UINT_MAX;
while (true) { 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()) { if (c.empty()) {
report_undef(s); report_undef(s);
return; return;
@ -618,6 +619,11 @@ public:
return pp.conquer_batch_size(); return pp.conquer_batch_size();
} }
bool filter_cubes() const {
parallel_params pp(m_params);
return pp.filter_cubes();
}
void cleanup() { void cleanup() {
m_queue.reset(); m_queue.reset();
init(); init();

1
src/tactic/smtlogics/parallel_params.pyg
View file

@ -7,4 +7,5 @@ def_module_params('parallel',
('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'), ('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'), ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'), ('restart.max', UINT, 100, 'maximal number of restarts during conquer phase'),
('filter_cubes', BOOL, False, 'filter cubes using a short running check'),
)) ))