projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b38ffa2) | patch
Universe set cardinality for finite types with finite cardinality (#3392)
authormudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu>
Wed, 8 Jan 2020 00:13:07 +0000 (18:13 -0600)
committerGitHub <noreply@github.com>
Wed, 8 Jan 2020 00:13:07 +0000 (18:13 -0600)
commit7ce64c96d655d675778bc70d424fd72f82db589f
treead43650d7c2cc82d8c96098530fb04485e63defctree
parentb38ffa21717d220e98581854e2af1ee9d13ce5b7commit | diff
Universe set cardinality for finite types with finite cardinality (#3392)

* rewrote set cardinality for finite-types

* small changes and format
23 files changed:
src/theory/sets/cardinality_extension.cpp diff | blob | history
src/theory/sets/cardinality_extension.h diff | blob | history
src/theory/sets/solver_state.cpp diff | blob | history
src/theory/sets/solver_state.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-color.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 [new file with mode: 0644] blob
test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 [new file with mode: 0644] blob