diff options
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1bd29684a..106161305 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -941,14 +941,6 @@ name = "Quantifiers" name = "all" help = "Always use single invocation techniques." -[[option]] - name = "cegqiSingleInvPartial" - category = "regular" - long = "sygus-si-partial" - type = "bool" - default = "false" - help = "combined techniques for synthesis conjectures that are partially single invocation" - # Solution reconstruction modes for single invocation conjectures # # These modes indicate the policy when cvc5 solves a synthesis conjecture using @@ -985,14 +977,6 @@ name = "Quantifiers" help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" [[option]] - name = "cegqiSingleInvReconstructConst" - category = "regular" - long = "sygus-si-reconstruct-const" - type = "bool" - default = "true" - help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" - -[[option]] name = "cegqiSingleInvAbort" category = "regular" long = "sygus-si-abort" |