def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
    """

    :param constraints:
    :param minimize:
    :param maximize:
    :param enforce_execution_time: Bool variable which enforces --execution-timeout's time
    :return:
    """
    s = Optimize()
    timeout = 100000
    if enforce_execution_time:
        timeout = min(timeout, time_handler.time_remaining() - 500)
        if timeout <= 0:
            raise UnsatError
    s.set_timeout(timeout)
    for constraint in constraints:
        if type(constraint) == bool and not constraint:
            raise UnsatError

    constraints = [constraint for constraint in constraints if type(constraint) != bool]

    for constraint in constraints:
        s.add(constraint)
    for e in minimize:
        s.minimize(e)
    for e in maximize:
        s.maximize(e)

    result = s.check()
    if result == sat:
        return s.model()
    elif result == unknown:
        log.debug("Timeout encountered while solving expression using z3")
    raise UnsatError
def get_model ( constraints , minimize = ( ) , maximize = ( ) , enforce_execution_time = True ) : s = Optimize ( ) timeout = 100000 if enforce_execution_time : timeout = min ( timeout , time_handler . time_remaining ( ) - 500 ) if timeout <= 0 : raise UnsatError s . set_timeout ( timeout ) for constraint in constraints : if type ( constraint ) == bool and not constraint : raise UnsatError constraints = [ constraint for constraint in constraints if type ( constraint ) != bool ] for constraint in constraints : s . add ( constraint ) for e in minimize : s . minimize ( e ) for e in maximize : s . maximize ( e ) result = s . check ( ) if result == sat : return s . model ( ) elif result == unknown : log . debug ( "Timeout encountered while solving expression using z3" ) raise UnsatError
:param constraints:
    :param minimize:
    :param maximize:
    :param enforce_execution_time: Bool variable which enforces --execution-timeout's time
    :return: