diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-04 18:50:55 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-04 18:50:55 -0500 |
| commit | f9d59828ebd150797682f1fbf5267aca7d15bb54 (patch) | |
| tree | 846371c0f52cb9749aaff333ab31ed7cb2fd81fd /src/options/base_options.toml | |
| parent | be6f9c2ee9201cc5181ce7ba27b6fe992ab3fff6 (diff) | |
Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)
Fixes #5341.
Diffstat (limited to 'src/options/base_options.toml')
| -rw-r--r-- | src/options/base_options.toml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/options/base_options.toml b/src/options/base_options.toml index ec3bd870d..8255da027 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -169,6 +169,11 @@ name = "Base" help = "print enumerated terms and candidates generated by the sygus solver" description = "With ``-o sygus``, cvc5 prints information about the internal SyGuS solver including enumerated terms and generated candidates." example-file = "regress0/sygus/print-debug.sy" +[[option.mode.SYGUS_GRAMMAR]] + name = "sygus-grammar" + help = "print grammars automatically generated by the sygus solver" + description = "With ``-o sygus-grammar``, cvc5 prints the grammar it generates for a function-to-synthesize when no grammar was provided." + example-file = "regress0/sygus/print-grammar.sy" [[option.mode.TRIGGER]] name = "trigger" help = "print selected triggers for quantified formulas" @@ -242,4 +247,4 @@ name = "Base" [[option]] name = "resourceWeightHolder" category = "undocumented" - type = "std::vector<std::string>"
\ No newline at end of file + type = "std::vector<std::string>" |