projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c35a4f) | patch
Refactor enumerator management in synth conjecture (#6942)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 24 Aug 2021 17:26:35 +0000 (12:26 -0500)
committerGitHub <noreply@github.com>
Tue, 24 Aug 2021 17:26:35 +0000 (14:26 -0300)
commitba34ba8fc1edc62702f6b6ffcd247d13ba7f8271
tree89250a8d7b045393b8aa21d41a1ea95767353679tree
parent2c35a4fd262a7aa1cc3b953265d327de4eae9f8ecommit | diff
Refactor enumerator management in synth conjecture (#6942)

This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.

It also integrates the sygus enumerator callback into the fast enumerator.
13 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/sygus/enum_value_manager.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/enum_value_manager.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/example_eval_cache.cpp diff | blob | history
src/theory/quantifiers/sygus/example_eval_cache.h diff | blob | history
src/theory/quantifiers/sygus/rcons_type_info.h diff | blob | history
src/theory/quantifiers/sygus/sygus_enumerator.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_enumerator.h diff | blob | history
src/theory/quantifiers/sygus/sygus_enumerator_callback.h diff | blob | history
src/theory/quantifiers/sygus/sygus_reconstruct.h diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.h diff | blob | history
src/theory/quantifiers/sygus_sampler.cpp diff | blob | history