diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-21 15:17:16 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-21 15:17:16 -0300 |
| commit | 8592fa1e2226e2c8b301ad9ed8caa13fad4c5913 (patch) | |
| tree | 90164414130605600162cbd24115c20d71d51eea /src/options | |
| parent | 0e5655c7d1fddde55bfeba9f59bf9af79e8b5f0a (diff) | |
hard limit for rec-fun eval (#3485)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 338f5544f..b3c1ffd4d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1221,6 +1221,14 @@ header = "options/quantifiers_options.h" default = "false" help = "enable efficient support for recursive functions in sygus grammars" +[[option]] + name = "sygusRecFunEvalLimit" + category = "regular" + long = "sygus-rec-fun-eval-limit=N" + type = "int" + default = "1000" + help = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)" + # Internal uses of sygus [[option]] @@ -1359,7 +1367,7 @@ header = "options/quantifiers_options.h" long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" - + [[option]] name = "sygusRewSynthRec" category = "regular" @@ -1420,7 +1428,7 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" - + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" |