projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 469de05) | patch
[API] Remove redundant version of `mkFunctionSort` (#8503)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 1 Apr 2022 04:50:25 +0000 (21:50 -0700)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 04:50:25 +0000 (04:50 +0000)
commit01061af730c2805c8c1d4a7cc2a03dee6ffc0017
tree0bc45fd5c8b4dcddebddcb50385279a801c04c83tree
parent469de059de55ad61b4f8601d4da6020ed42e368dcommit | diff
[API] Remove redundant version of `mkFunctionSort` (#8503)

mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.
14 files changed:
examples/api/cpp/combination.cpp diff | blob | history
examples/simple_vc_quant_cxx.cpp diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/java/io/github/cvc5/Solver.java diff | blob | history
src/api/java/jni/solver.cpp diff | blob | history
src/api/python/cvc5.pxd diff | blob | history
src/api/python/cvc5.pxi diff | blob | history
src/parser/tptp/tptp.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history
test/unit/api/cpp/sort_black.cpp diff | blob | history
test/unit/api/cpp/term_black.cpp diff | blob | history
test/unit/api/cpp/term_white.cpp diff | blob | history
test/unit/parser/parser_black.cpp diff | blob | history