diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/main_options.toml | 1 | ||||
| -rw-r--r-- | src/options/mkoptions.py | 3 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 18 |
3 files changed, 18 insertions, 4 deletions
diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 974bdd155..0e3f63072 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -6,6 +6,7 @@ name = "Driver" short = "V" long = "version" type = "void" + handler = "showVersion" help = "identify this cvc5 binary" [[option]] diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index badfd59f0..7288ede51 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -1047,6 +1047,9 @@ def mkoptions_main(): codegen_module(module, dst_dir, module_tpls) codegen_all_modules(modules, build_dir, dst_dir, global_tpls) + # Generate output file to signal cmake when this script was run last + open(os.path.join(dst_dir, 'options/options.stamp'), 'w').write('') + if __name__ == "__main__": mkoptions_main() diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index f3c89fd74..b15ed49a6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1448,10 +1448,20 @@ name = "Quantifiers" [[option]] name = "sygusQueryGen" category = "regular" - long = "sygus-query-gen" - type = "bool" - default = "false" - help = "use sygus to enumerate interesting satisfiability queries" + long = "sygus-query-gen=MODE" + type = "SygusQueryGenMode" + default = "NONE" + help = "mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing" + help_mode = "Modes for generating interesting satisfiability queries using SyGuS." +[[option.mode.NONE]] + name = "none" + help = "Do not generate queries with SyGuS." +[[option.mode.SAT]] + name = "sat" + help = "Generate interesting SAT queries, for e.g. soundness testing." +[[option.mode.UNSAT]] + name = "unsat" + help = "Generate interesting UNSAT queries, for e.g. proof testing." [[option]] name = "sygusQueryGenThresh" |