projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ef7cc3) | patch
Add a random Sygus enumerator. (#7782)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 14 Dec 2021 22:03:36 +0000 (16:03 -0600)
committerGitHub <noreply@github.com>
Tue, 14 Dec 2021 22:03:36 +0000 (22:03 +0000)
commitbbbe2f3ebbd7175930054cca12c3e5e32cd0cbd9
tree318e6335515d6ec911e764b60103b3dcfcb5f972tree
parent9ef7cc3520344901a704bda018cd1783ebc18d06commit | diff
Add a random Sygus enumerator. (#7782)

This PR adds a Sygus enumerator that generates random terms from a grammar. The size of the terms generated by the enumerator approximates a geometric distribution and can be configured with an option.
src/CMakeLists.txt diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/sygus/enum_value_manager.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_random_enumerator.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/sygus_random_enumerator.h [new file with mode: 0644] blob
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/rand_const.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/rand_p_0.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/rand_p_1.sy [new file with mode: 0644] blob