Initialize theory rewriters in theories (#4197)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 2 Apr 2020 02:35:25 +0000 (19:35 -0700)
committerGitHub <noreply@github.com>
Thu, 2 Apr 2020 02:35:25 +0000 (19:35 -0700)
commit3915eb7b497bd185385048f8c7f2b4c8f2bf7c03
tree8686d5ceea120ebda1ea65c0a8696ab1bdf78543
parent936e9c442443799c866a65c6ca3fbdcd3ac9aab8
Initialize theory rewriters in theories (#4197)

Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
45 files changed:
src/preprocessing/passes/bv_gauss.cpp
src/preprocessing/passes/bv_gauss.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/booleans/theory_bool.cpp
src/theory/booleans/theory_bool.h
src/theory/builtin/theory_builtin.cpp
src/theory/builtin/theory_builtin.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/mkrewriter
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/rewriter.cpp
src/theory/rewriter.h
src/theory/rewriter_tables_template.h
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/unit/preprocessing/pass_bv_gauss_white.h
test/unit/theory/evaluator_white.h
test/unit/theory/regexp_operation_black.h
test/unit/theory/sequences_rewriter_white.h
test/unit/theory/theory_black.h
test/unit/theory/theory_bv_rewriter_white.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_quantifiers_bv_instantiator_white.h
test/unit/theory/theory_sets_type_enumerator_white.h
test/unit/theory/theory_strings_skolem_cache_black.h
test/unit/theory/theory_white.h
test/unit/theory/type_enumerator_white.h