Start refactoring of `-o` and `-v` (#7449)
authorGereon Kremer <nafur42@gmail.com>
Thu, 4 Nov 2021 19:15:28 +0000 (12:15 -0700)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 19:15:28 +0000 (19:15 +0000)
commit67559f3b3e42dc1937f809e56ee57daa4bd8bd89
tree037d2a4202c2adef7940bbd1230875247f173bc6
parente1f69a43e9ee7e4a63f3c4a1881001bc650c9df7
Start refactoring of `-o` and `-v` (#7449)

This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.
25 files changed:
src/api/cpp/cvc5.cpp
src/main/command_executor.cpp
src/options/mkoptions.py
src/options/options_handler.cpp
src/smt/check_models.cpp
src/smt/env.cpp
src/smt/env.h
src/smt/env_obj.cpp
src/smt/env_obj.h
src/smt/quant_elim_solver.cpp
src/smt/solver_engine.cpp
src/smt/sygus_solver.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus_sampler.cpp
src/theory/theory_engine.cpp
src/theory/uf/cardinality_extension.cpp
test/regress/regress0/options/set-and-get-options.smt2
test/regress/regress0/sygus/issue5512-vvv.sy
test/unit/api/java/SolverTest.java
test/unit/api/solver_black.cpp