projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f99850) | patch
Remove usage of static options in arithmetic theory (#7221)
authorGereon Kremer <nafur42@gmail.com>
Thu, 30 Sep 2021 13:59:52 +0000 (06:59 -0700)
committerGitHub <noreply@github.com>
Thu, 30 Sep 2021 13:59:52 +0000 (13:59 +0000)
commit0a15133a7de2289fdfb10ccf65e9b753f5064ba7
tree59ce4531f7c71b9f53cb6936ea068e1e806a327ctree
parent5f998504d88e507bae22cdd7cc0dfd20f786ed99commit | diff
Remove usage of static options in arithmetic theory (#7221)

This PR removes the usage of static accesses to options from the arithmetic theory, mostly by making more classes inherit from EnvObj.
25 files changed:
src/preprocessing/passes/ite_simp.cpp diff | blob | history
src/theory/arith/arith_ite_utils.cpp diff | blob | history
src/theory/arith/arith_ite_utils.h diff | blob | history
src/theory/arith/attempt_solution_simplex.cpp diff | blob | history
src/theory/arith/attempt_solution_simplex.h diff | blob | history
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/dio_solver.cpp diff | blob | history
src/theory/arith/dio_solver.h diff | blob | history
src/theory/arith/dual_simplex.cpp diff | blob | history
src/theory/arith/dual_simplex.h diff | blob | history
src/theory/arith/fc_simplex.cpp diff | blob | history
src/theory/arith/fc_simplex.h diff | blob | history
src/theory/arith/linear_equality.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.h diff | blob | history
src/theory/arith/operator_elim.cpp diff | blob | history
src/theory/arith/operator_elim.h diff | blob | history
src/theory/arith/pp_rewrite_eq.cpp diff | blob | history
src/theory/arith/pp_rewrite_eq.h diff | blob | history
src/theory/arith/simplex.cpp diff | blob | history
src/theory/arith/simplex.h diff | blob | history
src/theory/arith/soi_simplex.cpp diff | blob | history
src/theory/arith/soi_simplex.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history