Skip to content

Commit

Permalink
Logic: Make API for getting array sort more robust
Browse files Browse the repository at this point in the history
Creating array sorts should be allowed only for logics that support
arrays.
  • Loading branch information
blishko committed Nov 10, 2023
1 parent f30e983 commit 7f50216
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/logics/Logic.cc
Original file line number Diff line number Diff line change
Expand Up @@ -1543,6 +1543,7 @@ bool Logic::isArrayStore(SymRef sr) const { return stores.has(sr); }
bool Logic::isArrayStore(PTRef tr) const { return isArrayStore(getPterm(tr).symb()); }

SRef Logic::getArraySort(SRef domain, SRef codomain) {
if (not hasArrays()) { throw OsmtApiException("Selected logic does not support arrays"); }
return getSort(sym_ArraySort, {domain, codomain});
}

Expand Down

0 comments on commit 7f50216

Please sign in to comment.