From bdf46b42d6bd66121a5b5175a81408cd64d7ecfa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Jul 2021 10:07:39 -0500 Subject: Add option to limit the number of instantiation rounds (#6818) This adds an option to limit the number of instantiation rounds used by quantifiers engine. This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions. This PR also makes minor improvements to the quantifier utility infrastructure. --- src/options/quantifiers_options.toml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/options/quantifiers_options.toml') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 20376c053..45341a6a6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -474,6 +474,14 @@ name = "Quantifiers" default = "true" help = "only input terms are assigned instantiation level zero" +[[option]] + name = "instMaxRounds" + category = "regular" + long = "inst-max-rounds=N" + type = "int" + default = "-1" + help = "maximum number of instantiation rounds (-1 == no limit, default)" + [[option]] name = "quantRepMode" category = "regular" -- cgit v1.2.3