projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ce6e00) | patch
Remove uf-ss-totality option (#5251)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 12 Oct 2020 22:56:32 +0000 (17:56 -0500)
committerGitHub <noreply@github.com>
Mon, 12 Oct 2020 22:56:32 +0000 (17:56 -0500)
commitb22b24ed70962fb9a5ce50d4cd202d70d7380bee
tree46f03874565e350a15a2ede32eee7cff8279dc41tree
parent3ce6e00068c02286704143d82d5f044fdb356516commit | diff
Remove uf-ss-totality option (#5251)

This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.

This does some additional cleaning of the uf cardinality extension, some methods changed indentation.

Fixes #5239, fixes #4872, fixes #4865.
src/options/uf_options.toml diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history
src/theory/uf/cardinality_extension.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fmf/issue4872-qf_ufc.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 [new file with mode: 0644] blob
test/regress/regress1/fmf/issue4068-si-qf.smt2 diff | blob | history