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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 3 |
2 files changed, 3 insertions, 4 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 81319e25a..b62fb0bbb 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 = SOLVER->mkSingleton(args[0].getSort(), args[0]); + { f = MK_TERM(api::SINGLETON, args[0]); for(size_t i = 1; i < args.size(); ++i) { - f = MK_TERM(api::UNION, f, SOLVER->mkSingleton(args[i].getSort(), args[i])); + f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i])); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index edeb47f06..a8a2eb27a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1163,8 +1163,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } if (kind == api::SINGLETON && args.size() == 1) { - api::Sort sort = args[0].getSort(); - api::Term ret = d_solver->mkSingleton(sort, args[0]); + api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]); Debug("parser") << "applyParseOp: return singleton " << ret << std::endl; return ret; } |