diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-11-05 17:13:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-05 17:13:44 -0600 |
commit | ac8b2593bed81125cb1a494e4b8311e517d0e3d9 (patch) | |
tree | eadc038a8e3700fdf96f52f41ac6a99f3090bf9b /src/theory/quantifiers/sygus/cegis.cpp | |
parent | d301b5175e39f82df9c179be1da7eaea892f7795 (diff) |
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
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
0 files changed, 0 insertions, 0 deletions