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 /test | |
| 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 'test')
| -rw-r--r-- | test/unit/theory/theory_sets_type_rules_white.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index f06c1f77d..66c8dc123 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -56,9 +56,10 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite Sort realSort = d_slv->getRealSort(); Sort intSort = d_slv->getIntegerSort(); Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort)); - Term one = d_slv->mkInteger(1); - Term singletonInt = d_slv->mkSingleton(intSort, one); - Term singletonReal = d_slv->mkSingleton(realSort, one); + Term integerOne = d_slv->mkInteger(1); + Term realOne = d_slv->mkReal(1); + Term singletonInt = d_slv->mkTerm(api::SINGLETON, integerOne); + Term singletonReal = d_slv->mkTerm(api::SINGLETON, realOne); // (union // (singleton (singleton_op Int) 1) // (as emptyset (Set Real))) |