# Path: tt/errors/arguments.py
# class InvalidArgumentTypeError(ArgumentError):
#     """An exception type for invalid argument types.
# 
#     To illustrate this error type, let's try passing an invalid argument when
#     creating a :class:`TruthTable <tt.tables.truth_table.TruthTable>`::
# 
#         >>> from tt import TruthTable
#         >>> t = TruthTable(7)
#         Traceback (most recent call last):
#             ...
#         tt.errors.arguments.InvalidArgumentTypeError: Arg `expr` must be of \
# type `str` or `BooleanExpression`
# 
#     """
# 
# class InvalidArgumentValueError(ArgumentError):
#     """An exception type for invalid argument values.
# 
#     Here's an example where we pass a non-power of 2 number of values when
#     attempting to create a :class:`TruthTable \
#     <tt.tables.truth_table.TruthTable>`::
# 
#         >>> from tt import TruthTable
#         >>> t = TruthTable(from_values='01x')
#         Traceback (most recent call last):
#             ...
#         tt.errors.arguments.InvalidArgumentValueError: Must specify a number \
# of input values that is a power of 2
# 
#     """


import os
from tt.errors.arguments import (
    InvalidArgumentTypeError,
    InvalidArgumentValueError)
    from tt._clibs import picosat as _c_picosat
    :type assumptions: List[:class:`int <python:int>`]

    :returns: If solution is found, a list of ints representing the terms of
        the solution; otherwise, if no solution found, ``None``.
    :rtype: List[:class:`int <python:int>`] or ``None``

    :raises InvalidArgumentTypeError: If ``clauses`` is not a list of lists of
        ints or ``assumptions`` is not a list of ints.
    :raises InvalidArgumentValueError: If any literal ints are equal to zero.

    Let's look at a simple example with no satisfiable solution::

        >>> from tt import picosat
        >>> picosat.sat_one([[1], [-1]]) is None
        True

    Here's an example where a solution exists::

        >>> picosat.sat_one([[1, 2, 3], [-2, -3], [1, -2], [2, -3], [-2]])
        [1, -2, -3]

    Finally, here's an example using assumptions::

        >>> picosat.sat_one([[1, 2, 3], [2, 3]], assumptions=[-1, -3])
        [-1, 2, -3]

    """
    try:
        return _c_picosat.sat_one(clauses, assumptions=assumptions)
    except TypeError as e:

# Path: tt/errors/arguments.py
# class InvalidArgumentTypeError(ArgumentError):
#     """An exception type for invalid argument types.
# 
#     To illustrate this error type, let's try passing an invalid argument when
#     creating a :class:`TruthTable <tt.tables.truth_table.TruthTable>`::
# 
#         >>> from tt import TruthTable
#         >>> t = TruthTable(7)
#         Traceback (most recent call last):
#             ...
#         tt.errors.arguments.InvalidArgumentTypeError: Arg `expr` must be of \
# type `str` or `BooleanExpression`
# 
#     """
# 
# class InvalidArgumentValueError(ArgumentError):
#     """An exception type for invalid argument values.
# 
#     Here's an example where we pass a non-power of 2 number of values when
#     attempting to create a :class:`TruthTable \
#     <tt.tables.truth_table.TruthTable>`::
# 
#         >>> from tt import TruthTable
#         >>> t = TruthTable(from_values='01x')
#         Traceback (most recent call last):
#             ...
#         tt.errors.arguments.InvalidArgumentValueError: Must specify a number \
# of input values that is a power of 2
# 
#     """


# Path: tt/satisfiability/picosat.py
import os
from tt.errors.arguments import (
    InvalidArgumentTypeError,
    InvalidArgumentValueError)
    from tt._clibs import picosat as _c_picosat

    :type assumptions: List[:class:`int <python:int>`]

    :returns: If solution is found, a list of ints representing the terms of
        the solution; otherwise, if no solution found, ``None``.
    :rtype: List[:class:`int <python:int>`] or ``None``

    :raises InvalidArgumentTypeError: If ``clauses`` is not a list of lists of
        ints or ``assumptions`` is not a list of ints.
    :raises InvalidArgumentValueError: If any literal ints are equal to zero.

    Let's look at a simple example with no satisfiable solution::

        >>> from tt import picosat
        >>> picosat.sat_one([[1], [-1]]) is None
        True

    Here's an example where a solution exists::

        >>> picosat.sat_one([[1, 2, 3], [-2, -3], [1, -2], [2, -3], [-2]])
        [1, -2, -3]

    Finally, here's an example using assumptions::

        >>> picosat.sat_one([[1, 2, 3], [2, 3]], assumptions=[-1, -3])
        [-1, 2, -3]

    """
    try:
        return _c_picosat.sat_one(clauses, assumptions=assumptions)
    except TypeError as e:

        raise InvalidArgumentTypeError(str(e))