projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec36a86) | patch
Add cardinality constraint utilities (#7286)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Oct 2021 08:20:19 +0000 (03:20 -0500)
committerGitHub <noreply@github.com>
Mon, 11 Oct 2021 08:20:19 +0000 (08:20 +0000)
commitb509f2700e31b4189ac76e4d0eabdde050535c0a
tree11c8d38df8c367c789f91f84e8eed3106595db74tree
parentec36a86e7250707a1c848779e856078fb3af0b04commit | diff
Add cardinality constraint utilities (#7286)

This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.

This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.
src/expr/CMakeLists.txt diff | blob | history
src/expr/cardinality_constraint.cpp [new file with mode: 0644] blob
src/expr/cardinality_constraint.h [new file with mode: 0644] blob