diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-04 15:10:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-04 15:10:24 -0500 |
commit | 13cf41801f8f2bac538cb45d53ae7427916041a7 (patch) | |
tree | 78e82b56e92004991890943ba5da863e6af3538f /src/api/cvc4cpp.cpp | |
parent | d662d3321a46aac61973f7a90341ea870c0b1171 (diff) |
Remove subtyping for sets theory (#5179)
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 6ed8855e4..179eb672e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3701,6 +3701,23 @@ Term Solver::mkEmptySet(Sort s) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkSingleton(Sort s, Term t) const +{ + NodeManagerScope scope(getNodeManager()); + + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_EXPECTED(!t.isNull(), t) << "non-null term"; + CVC4_API_SOLVER_CHECK_TERM(t); + checkMkTerm(SINGLETON, 1); + + TypeNode typeNode = TypeNode::fromType(*s.d_type); + Node res = getNodeManager()->mkSingleton(typeNode, *t.d_node); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::mkEmptyBag(Sort s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; |