Make theory rewriters non-static (#3547)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 9 Dec 2019 19:19:10 +0000 (11:19 -0800)
committerGitHub <noreply@github.com>
Mon, 9 Dec 2019 19:19:10 +0000 (11:19 -0800)
commitb6ce0f23ce0aaa0552767e8067fe58dbceee11cb
tree0783321580ed511c7ecfa3f59363dadcee15acde
parentd06b46efade674023236da228601806daf06f1af
Make theory rewriters non-static (#3547)

This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
  singletons in general. Note that the `Rewriter` class is still a
  singleton, which will be changed in a future commit.
22 files changed:
src/CMakeLists.txt
src/theory/arith/arith_rewriter.h
src/theory/arrays/theory_arrays_rewriter.h
src/theory/booleans/theory_bool_rewriter.h
src/theory/builtin/theory_builtin_rewriter.cpp
src/theory/builtin/theory_builtin_rewriter.h
src/theory/bv/theory_bv_rewriter.cpp
src/theory/bv/theory_bv_rewriter.h
src/theory/datatypes/datatypes_rewriter.h
src/theory/fp/theory_fp_rewriter.cpp
src/theory/fp/theory_fp_rewriter.h
src/theory/mkrewriter
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/rewriter.cpp
src/theory/rewriter.h
src/theory/rewriter_tables_template.h
src/theory/sep/theory_sep_rewriter.h
src/theory/sets/theory_sets_rewriter.h
src/theory/strings/regexp_elim.cpp
src/theory/strings/theory_strings_rewriter.h
src/theory/theory_rewriter.h [new file with mode: 0644]
src/theory/uf/theory_uf_rewriter.h