projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1a2d93) | patch
Add InferenceId to buffered inference manager (#5911)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 17 Feb 2021 13:42:50 +0000 (14:42 +0100)
committerGitHub <noreply@github.com>
Wed, 17 Feb 2021 13:42:50 +0000 (07:42 -0600)
commit2d6de44a51fed47a625ae73181efbcc3dac0c751
tree50ebd370468514d15b71a1d5f7d8993c24116fc0tree
parenta1a2d9389730ed46ab246865e320108db07c30ffcommit | diff
Add InferenceId to buffered inference manager (#5911)

This PR collects the InferenceId in the InferenceManagerBuffered class.
17 files changed:
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/inference_manager_buffered.cpp diff | blob | history
src/theory/inference_manager_buffered.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history
src/theory/quantifiers/sygus_inst.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sets/inference_manager.cpp diff | blob | history