diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-13 16:33:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-13 21:33:07 +0000 |
| commit | 1c0d2738941e948d67c696e0c96e3463da9807d2 (patch) | |
| tree | 31e929bc26f3b01518b339ed0c9bef562bc6983c /src/options/quantifiers_options.toml | |
| parent | f7dcb4875bba33b7712732a874581639681926f8 (diff) | |
Add pool instantiation strategy (#6308)
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index db7100e9c..bbdf030a1 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -586,6 +586,14 @@ header = "options/quantifiers_options.h" name = "agg" help = "Consider the phase requirements aggressively for all triggers." +[[option]] + name = "poolInst" + category = "regular" + long = "pool-inst" + type = "bool" + default = "true" + help = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools" + ### Finite model finding options [[option]] |