Towards standard usage of ExtendedRewriter (#7145)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 8 Sep 2021 17:30:31 +0000 (12:30 -0500)
committerGitHub <noreply@github.com>
Wed, 8 Sep 2021 17:30:31 +0000 (17:30 +0000)
commitd6b3329e3f2b6e29e5f4af6cf09fd32e26c47e15
tree4452ff0d7aaf72d726ab86625713aa508885afea
parentddce3af579b12b3eb8f69baec3806bc33f4ac23c
Towards standard usage of ExtendedRewriter (#7145)

This PR:

Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.
48 files changed:
src/preprocessing/passes/extended_rewriter_pass.cpp
src/smt/env_obj.cpp
src/smt/env_obj.h
src/smt/preprocess_proof_generator.cpp
src/smt/quant_elim_solver.cpp
src/smt/quant_elim_solver.h
src/theory/arith/nl/cad/cdcac.cpp
src/theory/arith/nl/cad/cdcac.h
src/theory/builtin/proof_checker.h
src/theory/datatypes/sygus_extension.cpp
src/theory/datatypes/sygus_extension.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/candidate_rewrite_database.cpp
src/theory/quantifiers/candidate_rewrite_database.h
src/theory/quantifiers/expr_miner_manager.cpp
src/theory/quantifiers/expr_miner_manager.h
src/theory/quantifiers/extended_rewrite.cpp
src/theory/quantifiers/extended_rewrite.h
src/theory/quantifiers/quantifiers_modules.cpp
src/theory/quantifiers/quantifiers_modules.h
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
src/theory/quantifiers/sygus/cegis.cpp
src/theory/quantifiers/sygus/enum_stream_substitution.cpp
src/theory/quantifiers/sygus/enum_value_manager.cpp
src/theory/quantifiers/sygus/enum_value_manager.h
src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
src/theory/quantifiers/sygus/sygus_enumerator_callback.h
src/theory/quantifiers/sygus/sygus_grammar_red.cpp
src/theory/quantifiers/sygus/sygus_invariance.cpp
src/theory/quantifiers/sygus/sygus_pbe.cpp
src/theory/quantifiers/sygus/sygus_unif_io.cpp
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_conjecture.h
src/theory/quantifiers/sygus/synth_engine.cpp
src/theory/quantifiers/sygus/synth_engine.h
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h
src/theory/quantifiers/term_registry.cpp
src/theory/quantifiers/term_registry.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/rewriter.cpp
src/theory/rewriter.h
test/unit/theory/sequences_rewriter_white.cpp
test/unit/theory/theory_arith_cad_white.cpp