Remove mkSingleton from the API (#5366)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 5 Nov 2020 23:13:44 +0000 (17:13 -0600)
committerGitHub <noreply@github.com>
Thu, 5 Nov 2020 23:13:44 +0000 (17:13 -0600)
commitac8b2593bed81125cb1a494e4b8311e517d0e3d9
treeeadc038a8e3700fdf96f52f41ac6a99f3090bf9b
parentd301b5175e39f82df9c179be1da7eaea892f7795
Remove mkSingleton from the API (#5366)

This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:

Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API
examples/api/python/sets.py
examples/api/sets.cpp
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/python/cvc4.pxd
src/api/python/cvc4.pxi
src/parser/cvc/Cvc.g
src/parser/smt2/smt2.cpp
src/theory/arith/nl/nonlinear_extension.cpp
test/unit/theory/theory_sets_type_rules_white.h