projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7ace6d4) | patch
Make all dependencies in the fast enumerator optional (#6918)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 27 Jul 2021 13:50:38 +0000 (08:50 -0500)
committerGitHub <noreply@github.com>
Tue, 27 Jul 2021 13:50:38 +0000 (13:50 +0000)
commit9d3eec992f14a8fa83a4b34de5eebe98604bdee6
treeb5f7f3ff7ca5420dd1cfea6e4490c90d10582b55tree
parent7ace6d43eeabb9ff2575f385ced5e2ed3c31ea2dcommit | diff
Make all dependencies in the fast enumerator optional (#6918)

This allows one to use a fast enumerator without having access to sygus term database, statistics, etc.
16 files changed:
src/theory/datatypes/sygus_datatype_utils.cpp diff | blob | history
src/theory/datatypes/sygus_datatype_utils.h diff | blob | history
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.h diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_unif.cpp diff | blob | history
src/theory/quantifiers/sygus/rcons_type_info.cpp 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_explain.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_unif.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_unif_io.cpp 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/sygus/term_database_sygus.h diff | blob | history