types

Type Members

1. class IntToTermTranslator extends CollectingVisitor[Unit, IExpression]

   

   Class to systematically replace integer literals in an expression with equivalent symbolic terms.

2. class MonoSortedIFunction extends SortedIFunction

   

   Class for monomorphically sorted functions.

3. class MonoSortedPredicate extends SortedPredicate

   

   Class for monomorphically sorted predicates

4. class ProxySort extends Sort

   

   Class to define proxy sorts, which inherit most properties from some underlying sort, but may override some of the features.

5. trait Sort extends AnyRef

   

   Trait representing sorts of individuals in the logic.

6. class SortedConstantTerm extends ConstantTerm

   

   Sorted version of constants.

7. abstract class SortedIFunction extends IFunction

   

   General class representing sorted functions; sub-classes can model both monomorphic and polymorphic functions.

8. abstract class SortedPredicate extends Predicate

   

   General class representing sorted predicates; sub-classes can model both monomorphic and polymorphic predicates.

9. class UninterpretedSortTheory extends Theory

   

   Theory to handle an uninterpreted sort.

   Theory to handle an uninterpreted sort. To ensure correct semantics, (non-empty, but cardinality might be finite or infinite), each uninterpreted sort is associated to a domain predicate, and an axiom specifying inhabitation is added.