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/cvc/Cvc.g | |
| 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/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
1 files changed, 2 insertions, 2 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])); } } |