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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
2 files changed, 9 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 5f959c660..6eb0924ac 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2158,9 +2158,9 @@ simpleTerm[CVC4::api::Term& f] /* finite set literal */ | LBRACE formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RBRACE - { f = MK_TERM(api::SINGLETON, args[0]); + { f = SOLVER->mkSingleton(args[0].getSort(), args[0]); for(size_t i = 1; i < args.size(); ++i) { - f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i])); + f = MK_TERM(api::UNION, f, SOLVER->mkSingleton(args[i].getSort(), args[i])); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e7bb8795c..c154db399 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1216,6 +1216,13 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError( "eqrange predicate requires option --arrays-exp to be enabled."); } + if (kind == api::SINGLETON && args.size() == 1) + { + api::Sort sort = args[0].getSort(); + api::Term ret = d_solver->mkSingleton(sort, args[0]); + Debug("parser") << "applyParseOp: return singleton " << ret << std::endl; + return ret; + } api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; |