from abc import abstractmethod, ABC
from typing import Any, Union, Iterable
from smt_encoding.constraints.function import Function
from smt_encoding.constraints.assertions import AssertHard, AssertSoft
from enum import Enum, unique

@unique
class OptimizeOutcome(Enum):
    no_model = 0
    non_optimal = 1
    optimal = 2
    unsat = 3
    error = 4

class Solver(ABC):
    """
    Interface that encapsulates the necessary functions a solver must perform
    """

    @abstractmethod
    def set_logic(self, logic: str) -> None:
        pass

    @abstractmethod
    def set_option(self, option: str, value: str) -> None:
        pass

    @abstractmethod
    def set_timeout(self, timeout: int) -> None:
        """
        Set the timeout for the overall execution of the SMT solver

        :param timeout: timeout in seconds!
        :return: None
        """
        pass

    @abstractmethod
    def declare_sort(self, sort_name: str) -> None:
        pass

    @abstractmethod
    def declare_function(self, *func: Function):
        pass

    @abstractmethod
    def assert_hard(self, hard_constraints: Iterable):
        pass

    @abstractmethod
    def assert_soft(self, soft_constraint: Iterable):
        pass

    @abstractmethod
    def check_sat(self) -> OptimizeOutcome:
        """
        Execute the SMT solver

        :param kwargs: arguments needed for the execution
        :return: the outcome after performing the optimization process
        """
        pass

    @abstractmethod
    def time_statistics(self) -> float:
        pass

    @abstractmethod
    def to_smt2(self) -> str:
        """
        Returns the current SMT problem . Note that smt2 has no standard for soft constraints, and thus, each solver
        may use their own representation

        :return: a string with the representation of the current problem
        """
        pass

    @abstractmethod
    def get_objectives(self):
        pass

    @abstractmethod
    def get_model(self):
        pass

    @abstractmethod
    def get_value(self, variable: Union[Function, str]) -> Any:
        """
        Returns the model generated by the SMT solver. Note that it is assumed that method execute was called
        beforehand. If not an empty model must be returned

        :return: the stored model by the smt solver
        """
        pass
