Eliminate Output macro in favor of simple Env functions (#7223)
authorGereon Kremer <nafur42@gmail.com>
Thu, 23 Sep 2021 23:14:08 +0000 (16:14 -0700)
committerGitHub <noreply@github.com>
Thu, 23 Sep 2021 23:14:08 +0000 (23:14 +0000)
commit07a47262c405fb37248572d3029883d078273cd7
treefb868ba98c8e3148db5a7397cd482c509514baaf
parent6b56848d3b09894aa4d987ca2e91a87ff1d022ab
Eliminate Output macro in favor of simple Env functions (#7223)

This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
21 files changed:
src/CMakeLists.txt
src/api/cpp/cvc5.cpp
src/options/outputc.cpp [deleted file]
src/options/outputc.h [deleted file]
src/smt/env.cpp
src/smt/env.h
src/theory/quantifiers/ematching/ho_trigger.cpp
src/theory/quantifiers/ematching/ho_trigger.h
src/theory/quantifiers/ematching/inst_strategy.cpp
src/theory/quantifiers/ematching/inst_strategy.h
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching.h
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
src/theory/quantifiers/ematching/instantiation_engine.cpp
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/ematching/trigger.h
src/theory/quantifiers/ematching/trigger_database.cpp
src/theory/quantifiers/ematching/trigger_database.h
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/sygus/synth_conjecture.cpp