Remove sygus print callback (#4727)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Jul 2020 19:12:18 +0000 (14:12 -0500)
committerGitHub <noreply@github.com>
Tue, 14 Jul 2020 19:12:18 +0000 (14:12 -0500)
commit14d32d598e9daa97cf1a29ff893caac2989baec4
treef37a48a15db69e6423a3149c1a2e91687b870542
parent455fed0b388ff9c534391eb88f8c2a336fa42f07
Remove sygus print callback (#4727)

This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.

This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.

This is required for further work towards eliminating the Expr layer.

FYI @4tXJ7f
34 files changed:
src/CMakeLists.txt
src/api/cvc4cpp.cpp
src/expr/datatype.cpp
src/expr/datatype.h
src/expr/sygus_datatype.cpp
src/expr/sygus_datatype.h
src/expr/type_node.cpp
src/expr/type_node.h
src/parser/smt2/smt2.cpp
src/preprocessing/passes/synth_rew_rules.cpp
src/printer/printer.cpp
src/printer/printer.h
src/printer/smt2/smt2_printer.cpp
src/printer/smt2/smt2_printer.h
src/printer/sygus_print_callback.cpp [deleted file]
src/printer/sygus_print_callback.h [deleted file]
src/theory/datatypes/sygus_datatype_utils.cpp
src/theory/datatypes/sygus_datatype_utils.h
src/theory/datatypes/sygus_extension.cpp
src/theory/quantifiers/candidate_rewrite_database.cpp
src/theory/quantifiers/candidate_rewrite_filter.cpp
src/theory/quantifiers/sygus/cegis_core_connective.cpp
src/theory/quantifiers/sygus/enum_stream_substitution.cpp
src/theory/quantifiers/sygus/sygus_abduct.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.h
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
src/theory/quantifiers/sygus/sygus_grammar_norm.h
src/theory/quantifiers/sygus/sygus_interpol.cpp
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/quantifiers/sygus/sygus_unif_rl.cpp
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h