# Path: typpete/src/constants.py
# ALIASES = {
#     'Dict': 'dict',
#     'Set': 'set',
#     'List': 'list',
#     'str': 'str'
# }
# 
# Path: typpete/src/z3_types.py
# class Dummy():
# class DummyOptimize:
# class TypesSolver(Solver):
# class Z3Types:
#     def add_soft(self, *args, **kwargs):
#     def add(self, *args, **kwargs):
#     def __init__(self, tree, solver=None, ctx=None, base_folder='',
#                  type_params:dict=None, class_type_params: dict=None):
#     def add(self, *args, fail_message):
#     def init_axioms(self):
#     def infer_stubs(self, context, infer_func):
#     def new_element_id(self):
#     def new_z3_const(self, name, sort=None):
#     def resolve_annotation(self, annotation, module):
#     def __init__(self, config, solver):
#     def subtype(self, t0, t1):
#     def create_class_tree(all_classes, type_sort):
#     def create_subst_axioms(self, tree):
#     def create_subtype_axioms(self, tree):
# def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type_vars):
# def create_classes_attributes(type_sort, classes_to_attrs, attributes_map):


from typpete.src.constants import ALIASES
from typpete.src.z3_types import And, Or, Implies, Not


def unary_invert(unary, types):
    """Constraints for the invert unary operation
    
    Only subtypes for int are eligible for this operation (No floats)
    
    Ex:
    - ~231
    """
    return [
        types.subtype(unary, types.int),
        unary != types.none
    ]


def unary_other(unary, result, types):
    """Constraints for any unary operation except (~) and (not)
    
    Cases:
        - (op) Number --> Stronger(Int, Number)
        
    Ex:
        - -True
        - +2.0
    """
    return [
        unary != types.none,
        types.subtype(unary, types.complex),
        Implies(unary == types.bool, result == types.int),

# Path: typpete/src/constants.py
# ALIASES = {
#     'Dict': 'dict',
#     'Set': 'set',
#     'List': 'list',
#     'str': 'str'
# }
# 
# Path: typpete/src/z3_types.py
# class Dummy():
# class DummyOptimize:
# class TypesSolver(Solver):
# class Z3Types:
#     def add_soft(self, *args, **kwargs):
#     def add(self, *args, **kwargs):
#     def __init__(self, tree, solver=None, ctx=None, base_folder='',
#                  type_params:dict=None, class_type_params: dict=None):
#     def add(self, *args, fail_message):
#     def init_axioms(self):
#     def infer_stubs(self, context, infer_func):
#     def new_element_id(self):
#     def new_z3_const(self, name, sort=None):
#     def resolve_annotation(self, annotation, module):
#     def __init__(self, config, solver):
#     def subtype(self, t0, t1):
#     def create_class_tree(all_classes, type_sort):
#     def create_subst_axioms(self, tree):
#     def create_subtype_axioms(self, tree):
# def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type_vars):
# def create_classes_attributes(type_sort, classes_to_attrs, attributes_map):


# Path: typpete/src/z3_axioms.py
from typpete.src.constants import ALIASES
from typpete.src.z3_types import And, Or, Implies, Not



def unary_invert(unary, types):
    """Constraints for the invert unary operation
    
    Only subtypes for int are eligible for this operation (No floats)
    
    Ex:
    - ~231
    """
    return [
        types.subtype(unary, types.int),
        unary != types.none
    ]


def unary_other(unary, result, types):
    """Constraints for any unary operation except (~) and (not)
    
    Cases:
        - (op) Number --> Stronger(Int, Number)
        
    Ex:
        - -True
        - +2.0
    """
    return [
        unary != types.none,
        types.subtype(unary, types.complex),
        Implies(unary == types.bool, result == types.int),

        Implies(unary != types.bool, result == unary)