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.