projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0291f94) | patch
Make cardinality constraint a nullary operator (#7333)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 21 Oct 2021 14:11:57 +0000 (09:11 -0500)
committerGitHub <noreply@github.com>
Thu, 21 Oct 2021 14:11:57 +0000 (14:11 +0000)
commiteeb78c833af50c49fd581704b03fd3c500360c3d
tree4e546205fb5d7495fd45c6fa5e76adc279abaecdtree
parent0291f941d4a2bae49a80c3db4afe626b55636fdfcommit | diff
Make cardinality constraint a nullary operator (#7333)

This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously.

It also removes an unimplemented kind CARDINALITY_VALUE.

Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.
18 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/expr/cardinality_constraint.cpp diff | blob | history
src/expr/cardinality_constraint.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/term_registration_visitor.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history
src/theory/uf/cardinality_extension.h diff | blob | history
src/theory/uf/kinds diff | blob | history
src/theory/uf/symmetry_breaker.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf_type_rules.cpp diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history
test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 diff | blob | history
test/unit/api/solver_black.cpp diff | blob | history