Class to systematically replace integer literals in an expression with equivalent symbolic terms.
Class for monomorphically sorted functions.
Class for monomorphically sorted predicates
Class to define proxy sorts, which inherit most properties from some underlying sort, but may override some of the features.
Trait representing sorts of individuals in the logic.
Sorted version of constants.
General class representing sorted functions; sub-classes can model both monomorphic and polymorphic functions.
General class representing sorted predicates; sub-classes can model both monomorphic and polymorphic predicates.
Theory to handle an uninterpreted sort.