projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: de0401e) | patch
Add output tags -o, --output. (#6826)
authorMathias Preiner <mathias.preiner@gmail.com>
Sat, 3 Jul 2021 17:44:30 +0000 (10:44 -0700)
committerGitHub <noreply@github.com>
Sat, 3 Jul 2021 17:44:30 +0000 (17:44 +0000)
commitc56eaf4423fbf65663a4e03c8a60ed937c99de7d
treec7b4d8d67f09441cac77a8100db49b6bf41e8230tree
parentde0401e53e4baab30a5e78d5bd51048348b1e1cecommit | diff
Add output tags -o, --output. (#6826)

Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.

Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.

Co-authored-by: Gereon Kremer <nafur42@gmail.com>
13 files changed:
src/base/output.cpp diff | blob | history
src/options/CMakeLists.txt diff | blob | history
src/options/base_options.toml diff | blob | history
src/options/mkoptions.py diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/options/options_handler.h diff | blob | history
src/options/outputc.cpp [new file with mode: 0644] blob
src/options/outputc.h [new file with mode: 0644] blob
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
test/regress/regress0/sygus/print-debug.sy diff | blob | history
test/regress/regress1/quantifiers/qid-debug-inst.smt2 diff | blob | history