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 /examples | |
| 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 'examples')
| -rw-r--r-- | examples/api/python/sets.py | 6 | ||||
| -rw-r--r-- | examples/api/sets.cpp | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 77de3e5b3..e4350ea1b 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -66,9 +66,9 @@ if __name__ == "__main__": two = slv.mkInteger(2) three = slv.mkInteger(3) - singleton_one = slv.mkSingleton(integer, one) - singleton_two = slv.mkSingleton(integer, two) - singleton_three = slv.mkSingleton(integer, three) + singleton_one = slv.mkTerm(kinds.Singleton, one) + singleton_two = slv.mkTerm(kinds.Singleton, two) + singleton_three = slv.mkTerm(kinds.Singleton, three) one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two) two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three) intersection = slv.mkTerm(kinds.Intersection, one_two, two_three) diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 549b68e0d..f8053a756 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -73,9 +73,9 @@ int main() Term two = slv.mkInteger(2); Term three = slv.mkInteger(3); - Term singleton_one = slv.mkSingleton(integer, one); - Term singleton_two = slv.mkSingleton(integer, two); - Term singleton_three = slv.mkSingleton(integer, three); + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); |