From de28e57deea98d5406d6317b26c616917b8c2419 Mon Sep 17 00:00:00 2001 From: mikolas Date: Fri, 29 Jan 2016 17:21:21 +0000 Subject: [PATCH] Adding parameters to Ackermannization in qfbv_tactic. --- src/tactic/smtlogics/qfbv_tactic_params.pyg | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 src/tactic/smtlogics/qfbv_tactic_params.pyg diff --git a/src/tactic/smtlogics/qfbv_tactic_params.pyg b/src/tactic/smtlogics/qfbv_tactic_params.pyg new file mode 100644 index 000000000..8dccfc650 --- /dev/null +++ b/src/tactic/smtlogics/qfbv_tactic_params.pyg @@ -0,0 +1,6 @@ +def_module_params(class_name='qfbv_tactic_params', + module_name="smtlogic_tactic", + export=True, + params=(('div0ackermann', BOOL, False, "if true, then try to Ackermannize div etc functions."), + ("div0_ackermann_limit", UINT, 1000, "a bound for number of congregants Ackerman lemmas") + ))