From e2e1411707e4a7968caffca511b6289b73a18939 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 31 May 2018 10:42:25 -0700 Subject: [PATCH] Option to dump SMT queries as benchmarks during Spacer run --- src/muz/base/fixedpoint_params.pyg | 2 ++ src/muz/spacer/spacer_context.cpp | 7 +++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 7b8f8fb72..9d3ee864d 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -203,4 +203,6 @@ def_module_params('fixedpoint', ('spacer.print_json', SYMBOL, '', 'print pobs tree in JSON format to a given file'), ('spacer.ctp', BOOL, False, 'enable counterexample-to-pushing technique'), ('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'), )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 5f8951ecb..c9fa7f72b 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2342,13 +2342,12 @@ void context::init_global_smt_params() { } p.set_uint("random_seed", m_params.spacer_random_seed()); - // fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks(); - // fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time(); - // fparams.m_dump_recheck = m_params.spacer_vs_recheck(); + p.set_bool("dump_benchmarks", m_params.spacer_dump_benchmarks()); + p.set_double("dump_threshold", m_params.spacer_dump_threshold()); + // mbqi p.set_bool("mbqi", m_params.spacer_mbqi()); - if (!m_params.spacer_ground_cti()) { p.set_uint("phase_selection", PS_CACHING_CONSERVATIVE2); p.set_uint("restart_strategy", RS_GEOMETRIC);