From 28ef9ab9d14f220268df53db721969bea9e0458e Mon Sep 17 00:00:00 2001 From: Matteo Marescotti Date: Thu, 15 Mar 2018 16:30:42 -0400 Subject: [PATCH] User option to enable starting spacer from a given level --- src/muz/base/fixedpoint_params.pyg | 3 ++- src/muz/spacer/spacer_dl_interface.cpp | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 07b555095..dc051bd71 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -192,7 +192,8 @@ def_module_params('fixedpoint', ('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.share_lemmas', BOOL, False, "Share frame lemmas"), ('spacer.share_invariants', BOOL, False, "Share invariants lemmas"), -)) + ('spacer.from_level', UINT, 0, 'starting level to explore') + )) diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index 57c225b38..69e5d76ff 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -170,7 +170,7 @@ lbool dl_interface::query(expr * query) return l_false; } - return m_context->solve(); + return m_context->solve(m_ctx.get_params().spacer_from_level()); }