projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7ca17de) | patch
Eliminate non-static members in term util (#5919)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 18 Feb 2021 03:15:39 +0000 (21:15 -0600)
committerGitHub <noreply@github.com>
Thu, 18 Feb 2021 03:15:39 +0000 (21:15 -0600)
commit0bd5ef36d2b773912c3049f8f3fed62eaf0fa68b
tree10885ad08d1a3b7d311b21a8223183e8cfe611d1tree
parent7ca17deba3b0f0308bda304ac739caf43e9536c0commit | diff
Eliminate non-static members in term util (#5919)

This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.

This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
20 files changed:
src/theory/datatypes/sygus_simple_sym.cpp diff | blob | history
src/theory/datatypes/sygus_simple_sym.h diff | blob | history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/quant_module.cpp diff | blob | history
src/theory/quantifiers/quant_module.h diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.h diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_norm.h diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_red.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_red.h diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history