projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3c53479) | patch
Do not export dt.size (#8483)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2022 18:28:16 +0000 (13:28 -0500)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 18:28:16 +0000 (18:28 +0000)
commitfa0068aa7b53e4cd87b274dbbeed27ebc403e949
treeabc3b04e75910e9797c8023e3f37c9b63727507btree
parent3c53479aab2d7bb086a9d25acd0417c60b98affccommit | diff
Do not export dt.size (#8483)

This kind is hardcoded only to work for sygus. I am not sure we want to support general constraints over it, or even if the token dt.size is the appropriate one.

Also adds a missing experimental warning that I had missed.

Fixes cvc5/cvc5-projects#504.
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/datatypes/kinds diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history