Further simplifications in preparation for removing Expr layer (#5756)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Jan 2021 15:46:28 +0000 (09:46 -0600)
committerGitHub <noreply@github.com>
Mon, 11 Jan 2021 15:46:28 +0000 (09:46 -0600)
commitb8841e768a37131c492508cd0e12b9acd8bf4c2b
treea4de18a51ac37abcf874265bea431154f18cc2ac
parentae82eb306143ade54a6f99b2aae0b62b8c77cd35
Further simplifications in preparation for removing Expr layer (#5756)

This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.

These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.

This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
23 files changed:
src/api/cvc4cpp.cpp
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/expr_template.cpp
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/node_manager_attributes.h
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/miplib_trick.h
src/preprocessing/passes/synth_rew_rules.cpp
src/printer/ast/ast_printer.cpp
src/smt/dump_manager.cpp
src/smt/dump_manager.h
src/smt/listeners.cpp
src/smt/listeners.h
src/smt/smt_engine.cpp
src/theory/builtin/theory_builtin_type_rules.h
src/theory/datatypes/sygus_datatype_utils.cpp
src/theory/quantifiers/sygus/cegis_unif.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
test/unit/expr/type_cardinality_public.h
test/unit/util/datatype_black.h