projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7ea2ea8) | patch
Improve syntax for fmf cardinality constraints (#7556)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 2 Nov 2021 19:58:13 +0000 (14:58 -0500)
committerGitHub <noreply@github.com>
Tue, 2 Nov 2021 19:58:13 +0000 (14:58 -0500)
commit9c767739c7ca2159de8800fff05dce3b7037cfc6
tree99db33c75820422b01cdfa293b93523b3badd67ftree
parent7ea2ea8f708fc7b5e8ea370898fbcb8cbf487aeccommit | diff
Improve syntax for fmf cardinality constraints (#7556)

This is an experimental extension of smt2.
12 files changed:
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 diff | blob | history
test/regress/regress0/fmf/fc-simple.smt2 diff | blob | history
test/regress/regress0/fmf/fc-unsat-pent.smt2 diff | blob | history
test/regress/regress0/fmf/fc-unsat-tot-2.smt2 diff | blob | history
test/regress/regress0/fmf/issue4850-force-card.smt2 diff | blob | history
test/regress/regress0/fmf/issue4872-qf_ufc.smt2 diff | blob | history
test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 diff | blob | history
test/regress/regress0/issue5550-num-children.smt2 diff | blob | history
test/regress/regress1/fmf/fc-pigeonhole19.smt2 diff | blob | history