| This class represents the translation rule for an Equality.
Three different types of an Equality are currently translated:
If the target Sort of an Equality is FORMULA, it is translated
into an SMT-LIB ConnectiveFormula as equivalence. The same happens for an Equality
having a boolean target Sort.
If the target Sort is an integer or object Sort, it is translated into a
PredicateFormula as equality
author: akuwertz version: 1.2, 03/27/2006 (Added support for obejct sort) |