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

Option to dump SMT queries as benchmarks during Spacer run

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 10:42:25 -07:00
parent bebfac047e
commit e2e1411707
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/base/fixedpoint_params.pyg
View file

@ -203,4 +203,6 @@ def_module_params('fixedpoint',
('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file'), ('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file'),
('spacer.ctp', BOOL, False, 'enable counterexample-to-pushing technique'), ('spacer.ctp', BOOL, False, 'enable counterexample-to-pushing technique'),
('spacer.use_inc_clause', BOOL, False, 'Use incremental clause to represent trans'), ('spacer.use_inc_clause', BOOL, False, 'Use incremental clause to represent trans'),
('spacer.dump_benchmarks', BOOL, False, 'Dump SMT queries as benchmarks'),
('spacer.dump_threshold', DOUBLE, 5.0, 'Threshold in seconds on dumping benchmarks'),
)) ))

7
src/muz/spacer/spacer_context.cpp
View file

@ -2342,13 +2342,12 @@ void context::init_global_smt_params() {
} }
p.set_uint("random_seed", m_params.spacer_random_seed()); p.set_uint("random_seed", m_params.spacer_random_seed());
// fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks(); p.set_bool("dump_benchmarks", m_params.spacer_dump_benchmarks());
// fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time(); p.set_double("dump_threshold", m_params.spacer_dump_threshold());
// fparams.m_dump_recheck = m_params.spacer_vs_recheck();
// mbqi // mbqi
p.set_bool("mbqi", m_params.spacer_mbqi()); p.set_bool("mbqi", m_params.spacer_mbqi());
if (!m_params.spacer_ground_cti()) { if (!m_params.spacer_ground_cti()) {
p.set_uint("phase_selection", PS_CACHING_CONSERVATIVE2); p.set_uint("phase_selection", PS_CACHING_CONSERVATIVE2);
p.set_uint("restart_strategy", RS_GEOMETRIC); p.set_uint("restart_strategy", RS_GEOMETRIC);