projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 43170db) | patch
Refactor and fixes related to getSpecializedConstructorTerm (#7774)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 10 Dec 2021 21:47:18 +0000 (15:47 -0600)
committerGitHub <noreply@github.com>
Fri, 10 Dec 2021 21:47:18 +0000 (21:47 +0000)
commitbcd447593e30dd08c6dfc2e162505b9e815fd29b
tree2dfd99b5c66a14bd6940b2a05d434a975c275cdatree
parent43170db86742dd5fbe33b4bdc9a938f6c1ceae5dcommit | diff
Refactor and fixes related to getSpecializedConstructorTerm (#7774)

Fixes cvc5/cvc5-projects#381.
13 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/expr/dtype_cons.cpp diff | blob | history
src/expr/dtype_cons.h diff | blob | history
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.cpp diff | blob | history
src/theory/datatypes/type_enumerator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/skolemize.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history