"""This module contains the SMT abstraction for a basic symbol expression."""
from typing import Optional, Set, Any, TypeVar, Generic, cast
import z3
Annotations = Set[Any]
T = TypeVar("T", bound=z3.ExprRef)
[docs]class Expression(Generic[T]):
"""This is the base symbol class and maintains functionality for
simplification and annotations."""
def __init__(self, raw: T, annotations: Optional[Annotations] = None):
"""
:param raw:
:param annotations:
"""
self.raw = raw
if annotations:
assert isinstance(annotations, set)
self._annotations = annotations or set()
@property
def annotations(self) -> Annotations:
"""Gets the annotations for this expression.
:return:
"""
return self._annotations
[docs] def annotate(self, annotation: Any) -> None:
"""Annotates this expression with the given annotation.
:param annotation:
"""
self._annotations.add(annotation)
[docs] def simplify(self) -> None:
"""Simplify this expression."""
self.raw = cast(T, z3.simplify(self.raw))
def __repr__(self) -> str:
return repr(self.raw)
[docs] def size(self):
return self.raw.size()
def __hash__(self) -> int:
return self.raw.__hash__()
[docs] def get_annotations(self, annotation: Any):
return list(filter(lambda x: isinstance(x, annotation), self.annotations))
G = TypeVar("G", bound=Expression)
[docs]def simplify(expression: G) -> G:
"""Simplify the expression .
:param expression:
:return:
"""
expression.simplify()
return expression