projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fa18d91) | patch
Eliminate more hard coded uses of user context (#7309)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Oct 2021 15:12:17 +0000 (10:12 -0500)
committerGitHub <noreply@github.com>
Wed, 6 Oct 2021 15:12:17 +0000 (15:12 +0000)
commit9b9fef64a317128b94dbf266ee50a30f6f3a64ac
tree710209a2645ec9513b96ea90a6e1d6caddae702btree
parentfa18d91091ef640fd38b29ed87f69260d8f80208commit | diff
Eliminate more hard coded uses of user context (#7309)

This is in preparation to make the "lemma context" configurable.
18 files changed:
src/theory/arith/congruence_manager.cpp diff | blob | history
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/ext_theory.cpp diff | blob | history
src/theory/ext_theory.h diff | blob | history
src/theory/quantifiers/candidate_rewrite_filter.cpp diff | blob | history
src/theory/quantifiers/candidate_rewrite_filter.h diff | blob | history
src/theory/quantifiers/dynamic_rewrite.cpp diff | blob | history
src/theory/quantifiers/dynamic_rewrite.h diff | blob | history
src/theory/relevance_manager.cpp diff | blob | history
src/theory/relevance_manager.h diff | blob | history
src/theory/shared_terms_database.cpp diff | blob | history
src/theory/shared_terms_database.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory_engine_proof_generator.cpp diff | blob | history
src/theory/theory_engine_proof_generator.h diff | blob | history
src/theory/uf/proof_equality_engine.cpp diff | blob | history
src/theory/uf/proof_equality_engine.h diff | blob | history