class TypeBase(object):
class AutoType(TypeBase):
class BoolType(TypeBase):
class IntType(TypeBase):
class FloatingPointType(TypeBase):
class FloatType(FloatingPointType):
class DoubleType(FloatingPointType):
class FunctionType(TypeBase):
class ArrayType(TypeBase):
class IntegerArrayType(ArrayType):
class FloatArrayType(ArrayType):
    def __repr__(self):
    def __eq__(self, other):
    def __hash__(self):
    def __str__(self):
    def __str__(self):
    def __str__(self):
    def __str__(self):
    def __str__(self):
    def __str__(self):
    def __str__(self):
    def __init__(self, shape):
    def __str__(self):
    def __eq__(self, other):
    def __hash__(self):
def type_of(value):
def type_cast(dtype, value=None, top=False, bottom=False): ADD_OP = '+'
SUBTRACT_OP = '-'
UNARY_SUBTRACT_OP = '_'
MULTIPLY_OP = '*'
DIVIDE_OP = '/'
EXPONENTIATE_OP = 'exp'
EQUAL_OP = '=='
NOT_EQUAL_OP = '!='
GREATER_OP = '>'
GREATER_EQUAL_OP = '>='
LESS_OP = '<'
LESS_EQUAL_OP = '<='
UNARY_NEGATION_OP = '!'
AND_OP = '&&'
OR_OP = '||'
VARIABLE_OP = 'v'
EXTERNAL_OP = 'extern'
TERNARY_SELECT_OP = '?'
FIXPOINT_OP = 'fix'
FOR_OP = 'for'
STATE_GETTER_OP = '()'
BARRIER_OP = ','
INDEX_ACCESS_OP = 'access'
INDEX_UPDATE_OP = 'update'
SUBSCRIPT_OP = 'subscript'
ARITHMETIC_OPERATORS = [
    ADD_OP, SUBTRACT_OP, UNARY_SUBTRACT_OP, MULTIPLY_OP, DIVIDE_OP,
    EXPONENTIATE_OP, TERNARY_SELECT_OP, FIXPOINT_OP, FOR_OP, BARRIER_OP,
]
COMPARISON_OPERATORS = [
    EQUAL_OP, NOT_EQUAL_OP, GREATER_OP, LESS_OP, GREATER_EQUAL_OP,
    LESS_EQUAL_OP,
]
BOOLEAN_OPERATORS = COMPARISON_OPERATORS + [
    UNARY_NEGATION_OP, AND_OP, OR_OP
]
TRADITIONAL_OPERATORS = [
    ADD_OP, SUBTRACT_OP, UNARY_SUBTRACT_OP, MULTIPLY_OP, DIVIDE_OP,
    EQUAL_OP, NOT_EQUAL_OP, GREATER_OP, LESS_OP, GREATER_EQUAL_OP,
    LESS_EQUAL_OP, UNARY_NEGATION_OP, AND_OP, OR_OP
]
SPECIAL_OPERATORS = [
    TERNARY_SELECT_OP, FIXPOINT_OP
]
OPERATORS = BOOLEAN_OPERATORS + ARITHMETIC_OPERATORS + SPECIAL_OPERATORS
UNARY_OPERATORS = [UNARY_SUBTRACT_OP, UNARY_NEGATION_OP]
BINARY_OPERATORS = list(set(OPERATORS) - set(UNARY_OPERATORS))
ASSOCIATIVITY_OPERATORS = [ADD_OP, MULTIPLY_OP, EQUAL_OP, AND_OP, OR_OP]
COMMUTATIVITY_OPERATORS = ASSOCIATIVITY_OPERATORS
COMMUTATIVE_DISTRIBUTIVITY_OPERATOR_PAIRS = [(MULTIPLY_OP, ADD_OP)]
LEFT_DISTRIBUTIVITY_OPERATOR_PAIRS = \
    COMMUTATIVE_DISTRIBUTIVITY_OPERATOR_PAIRS
RIGHT_DISTRIBUTIVITY_OPERATOR_PAIRS = \
    COMMUTATIVE_DISTRIBUTIVITY_OPERATOR_PAIRS
LEFT_DISTRIBUTIVITY_OPERATORS, LEFT_DISTRIBUTION_OVER_OPERATORS = \
    list(zip(*LEFT_DISTRIBUTIVITY_OPERATOR_PAIRS))
RIGHT_DISTRIBUTIVITY_OPERATORS, RIGHT_DISTRIBUTION_OVER_OPERATORS = \
    list(zip(*RIGHT_DISTRIBUTIVITY_OPERATOR_PAIRS))
COMPARISON_NEGATE_DICT = {
    LESS_OP: GREATER_EQUAL_OP,
    LESS_EQUAL_OP: GREATER_OP,
    GREATER_OP: LESS_EQUAL_OP,
    GREATER_EQUAL_OP: LESS_OP,
    EQUAL_OP: NOT_EQUAL_OP,
    NOT_EQUAL_OP: EQUAL_OP,
}
COMPARISON_MIRROR_DICT = {
    LESS_OP: GREATER_OP,
    LESS_EQUAL_OP: GREATER_EQUAL_OP,
    GREATER_OP: LESS_OP,
    GREATER_EQUAL_OP: LESS_EQUAL_OP,
    EQUAL_OP: EQUAL_OP,
    NOT_EQUAL_OP: NOT_EQUAL_OP,
} class Variable(ArithmeticMixin, BooleanMixin, BinaryExpression):
    """The variable class."""
    __slots__ = ()
    _str_brackets = False

    def __init__(self, name, dtype=auto_type):
        super().__init__(VARIABLE_OP, name, dtype)

    @property
    def name(self):
        return self.args[0]

    @property
    def dtype(self):
        return self.args[1]

    def format(self):
        return '{}'.format(self.name)

    def __repr__(self):
        return '{cls}({name!r}, {dtype!r})'.format(
            cls=self.__class__.__name__, name=self.name, dtype=self.dtype) class UnaryArithExpr(UnaryExpression, ArithExpr):
    """Unary arithmetic expressions."""

    __slots__ = ()
    _str_brackets = False

    def format(self):
        arg, = self._args_to_str()
        if self.op == UNARY_SUBTRACT_OP:
            return '-{}'.format(arg)
        return super().format() class BinaryArithExpr(BinaryExpression, ArithExpr):
    """Binary arithmetic expressions."""

    __slots__ = ()

    def _attr(self):
        if self.op in COMMUTATIVITY_OPERATORS:
            args = frozenset(self.args)
        else:
            args = tuple(self.args)
        return (self.op, args) class SelectExpr(TernaryArithExpr):
    """Ternary expression with TERNARY_SELECT_OP operator."""

    __slots__ = ()

    def __init__(self, a1, a2, a3):
        super().__init__(TERNARY_SELECT_OP, a1, a2, a3)

    @property
    def bool_expr(self):
        return self.a1

    @property
    def true_expr(self):
        return self.a2

    @property
    def false_expr(self):
        return self.a3

    def format(self):
        return '{} ? {} : {}'.format(*self._args_to_str()) class BinaryBoolExpr(BinaryExpression, BoolExpr):
    """Binary boolean expressions."""

    __slots__ = () class FixExpr(QuaternaryArithExpr):
    """Fixpoint expression."""

    def __init__(self, a1, a2, a3, a4):
        super().__init__(FIXPOINT_OP, a1, a2, a3, a4)

    @property
    def bool_expr(self):
        return self.a1

    @property
    def loop_state(self):
        return self.a2

    @property
    def loop_var(self):
        return self.a3

    @property
    def init_state(self):
        return self.a4

    def format(self):
        fixpoint_var = underline('e')
        s = ('{op}(λ{fvar}.({bool_expr} ? {fvar} % {loop_state} : {var}))'
             ' % {init_state}')
        return s.format(
            fvar=fixpoint_var, op=self.op, bool_expr=self.bool_expr,
            loop_state=self.loop_state.format(), var=self.loop_var,
            init_state=self.init_state.format()) class AccessExpr(
        ArithmeticMixin, BooleanMixin, BinaryExpression, _TrueVarMixin):
    __slots__ = ()
    _str_brackets = False

    def __init__(self, var, subscript):
        from soap.semantics.label import Label
        if not isinstance(subscript, Label):
            subscript = Subscript(*subscript)
        super().__init__(INDEX_ACCESS_OP, var, subscript)

    @property
    def var(self):
        return self.a1

    @property
    def subscript(self):
        return self.a2

    def format(self):
        var, subscript = self._args_to_str()
        return '{}{}'.format(var, subscript)

    def __repr__(self):
        return '{cls}({var!r}, {subscript!r})'.format(
            cls=self.__class__.__name__, var=self.var,
            subscript=self.subscript) class UpdateExpr(
        ArithmeticMixin, BooleanMixin, TernaryExpression, _TrueVarMixin):
    __slots__ = ()
    _str_brackets = False

    def __init__(self, var, subscript, expr):
        from soap.semantics.label import Label
        if not isinstance(subscript, Label):
            subscript = Subscript(*subscript)
        super().__init__(INDEX_UPDATE_OP, var, subscript, expr)

    @property
    def var(self):
        return self.a1

    @property
    def subscript(self):
        return self.a2

    @property
    def expr(self):
        return self.a3

    def format(self):
        var, subscript, expr = (a.format() for a in self.args)
        args = '{}, \n{}, \n{}'.format(var, subscript, expr)
        return 'update(\n{})'.format(indent(args))

    def __repr__(self):
        return '{cls}({var!r}, {subscript!r}, {expr!r})'.format(
            cls=self.__class__.__name__, var=self.var,
            subscript=self.subscript, expr=self.expr) class IntegerInterval(Interval):
    """The interval containing integer values."""
    def __init__(self, v=None, top=False, bottom=False):
        super().__init__(v, top=top, bottom=bottom)
        try:
            if self.min not in (-inf, inf):
                self.min = mpz(self.min)
            if self.max not in (-inf, inf):
                self.max = mpz(self.max)
        except AttributeError:
            'The interval is a top or bottom.'

    def __truediv__(self, other):
        return FloatInterval(self) / other class ErrorSemantics(Lattice):
    """The error semantics."""
    def __init__(self, v=None, e=None, top=False, bottom=False):
        super().__init__(top=top, bottom=bottom)
        if top or bottom:
            self.v = self.e = FloatInterval(top=top, bottom=bottom)
            return

        def error(v, e):
            if isinstance(e, FloatInterval):
                return e
            if e is not None:
                return overapproximate_error(e)
            if isinstance(v, Lattice):
                if v.is_top():
                    return FloatInterval(top=True)
                if v.is_bottom():
                    return FloatInterval(bottom=True)
            v_min, v_max = _unpack(v)
            if _are_instance(v, (int, mpz_type)):
                abs_val = max(abs(v_min), abs(v_max))
                if mpfr(abs_val) == abs_val:
                    # some integers cannot be expressed exactly in fp values
                    return FloatInterval(0)
            if v_min == v_max:
                return round_off_error_from_exact(v_min)
            return round_off_error(FloatInterval(v))

        if isinstance(v, ErrorSemantics):
            self.v, self.e = v
        else:
            self.v, self.e = FloatInterval(v), error(v, e)

    def is_top(self):
        return self.v.is_top()

    def is_bottom(self):
        return self.v.is_bottom()

    @_decorate_coerce
    def join(self, other, cls):
        if cls is not None:
            return cls(self) | cls(other)
        return self.__class__(self.v | other.v, self.e | other.e)

    @_decorate_coerce
    def meet(self, other, cls):
        if cls is not None:
            return cls(self) & cls(other)
        return self.__class__(self.v & other.v, self.e & other.e)

    @_decorate_coerce
    def le(self, other, cls):
        if cls is not None:
            return cls(self).le(cls(other))
        return self.v.le(other.v) and self.e.le(other.e)

    def __iter__(self):
        return iter((self.v, self.e))

    def __contains__(self, v):
        return self.v.min <= v <= self.v.max

    @_decorate_operator
    def __add__(self, other, cls):
        if cls is not None:
            return cls(self) + cls(other)
        self_v_min, self_v_max = self.v
        other_v_min, other_v_max = other.v
        if _propagate_constant and \
           self_v_min == self_v_max and other_v_min == other_v_max:
            v = mpq(self_v_min) + mpq(other_v_min)
            e = round_off_error_from_exact(v)
        else:
            v = self.v + other.v
            e = round_off_error(v)
        e += self.e + other.e
        return self.__class__(v, e)
    __radd__ = __add__

    @_decorate_operator
    def __sub__(self, other, cls):
        if cls is not None:
            return cls(self) - cls(other)
        self_v_min, self_v_max = self.v
        other_v_min, other_v_max = other.v
        if _propagate_constant and \
           self_v_min == self_v_max and other_v_min == other_v_max:
            v = mpq(self_v_min) - mpq(other_v_min)
            e = round_off_error_from_exact(v)
        else:
            v = self.v - other.v
            e = round_off_error(v)
        e += self.e - other.e
        return self.__class__(v, e)

    @_decorate_operator
    def __rsub__(self, other, cls):
        if cls is not None:
            return cls(other) - cls(self)
        return other - self

    @_decorate_operator
    def __mul__(self, other, cls):
        if cls is not None:
            return cls(self) * cls(other)
        e = self.e * other.e
        self_v_min, self_v_max = self.v
        other_v_min, other_v_max = other.v
        if _propagate_constant and \
           self_v_min == self_v_max and other_v_min == other_v_max:
            v = mpq(self_v_min) * mpq(other_v_min)
            e += round_off_error_from_exact(v)
        else:
            v = self.v * other.v
            e += round_off_error(v)
        e += self.v * other.e + other.v * self.e
        return self.__class__(v, e)
    __rmul__ = __mul__

    @_decorate_operator
    def __truediv__(self, other, cls):
        if cls is not None:
            return cls(self) / cls(other)
        self_v_min, self_v_max = self.v
        other_v_min, other_v_max = other.v
        if _propagate_constant and \
           self_v_min == self_v_max and other_v_min == other_v_max:
            v = mpq(self_v_min) / mpq(other_v_min)
            er = round_off_error_from_exact(v)
            v = mpfr(v)
        else:
            v = self.v / other.v
            er = round_off_error(v)
        e = self.e - v * other.e
        e /= other.v + other.e
        e += er
        return self.__class__(v, e)

    @_decorate_operator
    def __rtruediv__(self, other, cls):
        if cls is not None:
            return cls(other) / cls(self)
        return other / self

    def __neg__(self):
        if self.is_top() or self.is_bottom():
            return self
        return self.__class__(-self.v, -self.e)

    def exp(self):
        if self.is_top() or self.is_bottom():
            return self
        v_min, v_max = self.v
        if _propagate_constant and v_min == v_max:
            v = gmpy2.exp(mpq(v_min))
        else:
            v = self.v.exp()
        # exponentiation generally computes irrational numbers
        e = round_off_error(v)
        e += (self.e.exp() - 1) * v
        return self.__class__(v, e)

    @_decorate_operator
    def widen(self, other, cls):
        if cls is not None:
            return cls(self).widen(cls(other))
        return self.__class__(self.v.widen(other.v), self.e | other.e)

    def __abs__(self):
        return self.v + self.e

    def __getitem__(self, key):
        try:
            k_min, k_max = key
        except (TypeError, ValueError):
            raise KeyError(
                'Do not know how to produce the error interval from {}'
                .format(key))
        return ErrorSemantics(self.v, [k_min, k_max])

    def __str__(self):
        v = str(self.v)
        e = '' if self.e.min == self.e.max == 0 else str(self.e)
        if not e:
            return v
        if self.v.min == self.v.max:
            v = '[{}]'.format(v)
        if self.e.min == self.e.max:
            e = '[{}]'.format(e)
        return v + e

    def __repr__(self):
        return '{cls}({value!r}, {error!r})'.format(
            cls=self.__class__.__name__, value=self.v, error=self.e)

    def __hash__(self):
        self._hash = hash_val = hash((self.v, self.e))
        return hash_val class ArithmeticEvaluator(base_dispatcher()):
    def generic_execute(self, expr, state):
    def execute_numeral(self, expr, state):
    def execute_PartitionLabel(self, expr, state):
    def _execute_args(self, expr, state):
    def execute_Variable(self, expr, state):
    def execute_UnaryArithExpr(self, expr, state):
    def execute_BinaryArithExpr(self, expr, state):
    def execute_Subscript(self, expr, state):
    def execute_AccessExpr(self, expr, state):
    def execute_UpdateExpr(self, expr, state):
    def execute_SelectExpr(self, expr, state):
    def execute_FixExpr(self, expr, state):
    def execute_PreUnrollExpr(self, expr, state):
    def execute_MetaState(self, meta_state, state):
    def __call__(self, expr, state):
    def __eq__(self, other):
    def __hash__(self):
def _to_norm(value):
def error_eval(expr, state, to_norm=True): class IntegerIntervalArray(MultiDimensionalArray):
    value_class = IntegerInterval class BoxState(BaseState, MapLattice):
    __slots__ = ()

    def _init_key_value(self, key, value):
        value = self._cast_value(key, value)
        if isinstance(key, str):
            key = Variable(key, type_of(value))
        elif isinstance(key, Variable):
            dtype = key.dtype
            if dtype is not auto_type and dtype != type_of(value):
                value = type_cast(dtype, value=value)
        return key, value

    def _cast_key(self, key, value=None):
        if isinstance(key, (Variable, Label)):
            return key
        if isinstance(key, str):
            var_list = [var for var in self.keys() if var.name == key]
            if not var_list:
                raise KeyErrorFromString(key)
            if len(var_list) > 1:
                raise KeyErrorFromString(
                    'Multiple variables with the same name.')
            var = var_list.pop()
            return var
        raise TypeError(
            'Do not know how to convert {!r} into a variable'.format(key))

    def _cast_value(self, key=None, value=None, top=False, bottom=False):
        if top or bottom:
            return type_cast(key.dtype, value=value, top=top, bottom=bottom)
        if isinstance(value, MultiDimensionalArray):
            return value
        return cast(value)

    def is_fixpoint(self, other):
        """Checks if `self` is equal to `other` in the value ranges.

        For potential non-terminating loops, states are not the bottom element
        in the evaluation of loop statements even if a fixpoint is reached.
        This computation would result in a fixpoint of value ranges but
        the resulting error terms are strictly greater. Consequently for
        non-terminating loops the fixpoint for the error terms are always
        [-inf, inf] = ⊤. To gain any useful information about the program we
        wish to disregard the error terms and warn about non-termination.
        """
        if self.is_top() and other.is_top():
            return True
        if self.is_bottom() and other.is_bottom():
            return True
        non_bottom_keys = lambda d: set(
            [k for k, v in d.items() if not v.is_bottom()])
        if non_bottom_keys(self) != non_bottom_keys(other):
            return False
        for k, v in self.items():
            u = other[k]
            if type(v) is not type(u):
                return False
            if isinstance(v, ErrorSemantics):
                if not v.is_top() and not u.is_top():
                    u, v = u.v, v.v
            if u != v:
                return False
        return True

    def widen(self, other):
        """Simple widening operator, jumps to infinity if interval widens.

        self.widen(other) => self ∇ other
        """
        if self.is_top() or other.is_bottom():
            return self
        if self.is_bottom() or other.is_top():
            return other
        mapping = dict(self)
        for k, v in other.items():
            if k not in mapping:
                mapping[k] = v
            else:
                mapping[k] = mapping[k].widen(v)
        return self.__class__(mapping) class MetaState(BaseState, dict):
    __slots__ = ('_hash')

    def __init__(self, dictionary=None, **kwargs):
        dictionary = dict(dictionary or {}, **kwargs)
        mapping = {
            self._cast_key(key): self._cast_value(key, value)
            for key, value in dictionary.items()
        }
        super().__init__(mapping)
        self._hash = None

    def _cast_key(self, key):
        if isinstance(key, (Variable, Label, OutputVariableTuple)):
            return key
        if isinstance(key, str):
            var_list = [var for var in self.keys() if var.name == key]
            if not var_list:
                raise KeyError(key)
            if len(var_list) > 1:
                raise KeyError('Multiple variables with the same name.')
            var = var_list.pop()
            return var
        raise TypeError(
            'Do not know how to convert {!r} into a variable'.format(key))

    def _cast_value(self, key, value):
        if isinstance(value, (Label, Expression)):
            return value
        if isinstance(value, str):
            from soap.parser import parse
            return parse(value)
        if isinstance(value, (int, float)) or is_numeral(value):
            return cast(value)
        if isinstance(value, dict):
            return self.__class__(value)
        raise TypeError(
            'Do not know how to convert {!r} into an expression'.format(value))

    def __getitem__(self, key):
        try:
            return super().__getitem__(key)
        except KeyError:
            logger.warning('Variable {} does not exist.'.format(key))
            return Variable('__unreachable', key.dtype)

    def is_fixpoint(self, other):
        raise RuntimeError('Should not be called.')

    def widen(self, other):
        raise RuntimeError('Should not be called.')

    def visit_SkipFlow(self, flow):
        return self

    def visit_AssignFlow(self, flow):
        var, expr = flow.var, flow.expr
        if isinstance(var, AccessExpr):
            var, subscript = var.var, var.subscript
            expr = UpdateExpr(var, subscript, expr)
        return self.immu_update(var, expand_expr(expr, self))

    def visit_IfFlow(self, flow):
        def get(state, var):
            expr = state[var]
            return expr
        bool_expr = expand_expr(flow.conditional_expr, self)
        true_state = self.transition(flow.true_flow)
        false_state = self.transition(flow.false_flow)
        var_list = set(self.keys())
        var_list |= set(true_state.keys()) | set(false_state.keys())
        mapping = dict(self)
        for var in var_list:
            true_expr = get(true_state, var)
            false_expr = get(false_state, var)
            if true_expr == false_expr:
                value = true_expr
            else:
                value = SelectExpr(bool_expr, true_expr, false_expr)
            mapping[var] = value
        return self.__class__(mapping)

    @staticmethod
    def _input_vars(meta_state, var):
        in_vars = {var}
        next_vars = {var}
        while next_vars:
            var = next_vars.pop()
            expr = meta_state.get(var)
            if expr is None or is_numeral(expr):
                continue
            expr_vars = expr.vars()
            next_vars |= expr_vars - in_vars
            in_vars |= expr_vars
        return in_vars

    def _visit_loop(self, init_state, bool_expr, loop_flow):
        """
        Finds necessary loop variables and loop states for each variable.
        """
        bool_expr_vars = bool_expr.vars()
        input_vars = loop_flow.vars(output=False) | bool_expr_vars
        loop_vars = loop_flow.vars(input=False)
        id_state = self.__class__({k: k for k in input_vars | loop_vars})
        loop_state = id_state.transition(loop_flow)

        loop_map = {}
        init_map = {}

        for var in loop_vars:
            # local loop/init variables
            local_loop_vars = self._input_vars(loop_state, var)
            local_loop_vars |= bool_expr_vars
            # local loop/init states
            loop_map[var] = self.__class__(
                {k: v for k, v in loop_state.items() if k in local_loop_vars})
            init_map[var] = self.__class__(
                {k: v for k, v in init_state.items() if k in local_loop_vars})

        mapping = dict(init_state)
        for var in loop_map:
            # fixpoint expression
            mapping[var] = FixExpr(
                bool_expr, loop_map[var], var, init_map[var])
        return self.__class__(mapping)

    def visit_WhileFlow(self, flow):
        return self._visit_loop(self, flow.conditional_expr, flow.loop_flow)

    def visit_ForFlow(self, flow):
        init_state = self(flow.init_flow)
        return self._visit_loop(
            init_state, flow.conditional_expr, flow.loop_flow + flow.incr_flow)

    def format(self):
        items = []
        for k, v in sorted(self.items(), key=str):
            if isinstance(v, (Expression, MetaState)):
                v = v.format()
            items.append('{}: {}'.format(k, v))
        items = ', \n'.join(items)
        return '{{\n{}}}'.format(indent(items))

    def __str__(self):
        return self.format().replace('    ', '').replace('\n', '').strip()

    def __hash__(self):
        if self._hash is None:
            self._hash = hash(tuple(sorted(self.items(), key=hash)))
        return self._hash
import unittest
from soap.datatype import int_type, float_type, IntegerArrayType
from soap.expression import (
    operators, UnaryArithExpr, BinaryArithExpr, SelectExpr, FixExpr,
    AccessExpr, UpdateExpr, BinaryBoolExpr, Variable
)
from soap.semantics.error import IntegerInterval, ErrorSemantics
from soap.semantics.functions.arithmetic import arith_eval
from soap.semantics.linalg import IntegerIntervalArray
from soap.semantics.state.box import BoxState
from soap.semantics.state.meta import MetaState



class TestArithmeticEvaluator(unittest.TestCase):
    def setUp(self):
        self.a = Variable('a', IntegerArrayType([2, 2]))
        self.x = Variable('x', int_type)
        self.y = Variable('y', int_type)
        self.z = Variable('z', float_type)
        self.state = BoxState(x=[1, 2], y=3, z=[1.0, 2.0])
        self.array_state = BoxState(
            a=IntegerIntervalArray([[1, 2], [3, 4]]), x=[0, 1], y=0)

    def test_numeral(self):
        test_value = self.state['x']
        value = arith_eval(test_value, self.state)
        self.assertEqual(test_value, value)

    def test_Variable(self):
        test_expr = self.x
        test_value = self.state[test_expr]
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

    def test_UnaryArithExpr(self):
        test_expr = UnaryArithExpr(operators.UNARY_SUBTRACT_OP, self.x)
        test_value = -self.state['x']
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

    def test_BinaryArithExpr(self):
        test_expr = BinaryArithExpr(operators.ADD_OP, self.x, self.y)
        test_value = self.state['x'] + self.state['y']
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

    def test_AccessExpr(self):
        test_expr = AccessExpr(self.a, (self.x, self.y))
        test_value = IntegerInterval([1, 3])
        value = arith_eval(test_expr, self.array_state)
        self.assertEqual(test_value, value)

    def test_UpdateExpr(self):
        test_expr = UpdateExpr(self.a, (self.x, self.y), IntegerInterval(2))
        test_value = IntegerIntervalArray(
            [[IntegerInterval([1, 2]), 2], [IntegerInterval([2, 3]), 4]])
        value = arith_eval(test_expr, self.array_state)
        self.assertEqual(test_value, value)

    def test_SelectExpr(self):
        test_expr = SelectExpr(
            BinaryBoolExpr(operators.LESS_OP, self.x, ErrorSemantics(1.5)),
            IntegerInterval(0), self.y)
        test_value = IntegerInterval(0)
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

        test_expr = SelectExpr(
            BinaryBoolExpr(operators.LESS_OP, self.z, ErrorSemantics(1.5)),
            IntegerInterval(0), self.y)
        test_value = IntegerInterval([0, 3])
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

    def test_FixExpr(self):
        bool_expr = BinaryBoolExpr(operators.LESS_OP, self.x, self.y)
        loop_state = MetaState({
            self.x: BinaryArithExpr(
                operators.ADD_OP, self.x, IntegerInterval(1)),
            self.y: self.y,
        })
        init_state = MetaState({
            self.x: self.x, self.y: self.y,
        })
        test_expr = FixExpr(bool_expr, loop_state, self.x, init_state)
        test_value = IntegerInterval(3)
        value = arith_eval(test_expr, self.state)
        self.assertEqual(test_value, value)

    def test_MetaState(self):

        meta_state = MetaState({