switching to high quality piper tts and added label translations

2026-01-29 23:48:19 +01:00
commit d80c619df9
3934 changed files with 1451600 additions and 0 deletions
@@ -0,0 +1,286 @@
+from sympy.assumptions.assume import global_assumptions
+from sympy.assumptions.cnf import CNF, EncodedCNF
+from sympy.assumptions.ask import Q
+from sympy.logic.inference import satisfiable
+from sympy.logic.algorithms.lra_theory import UnhandledInput, ALLOWED_PRED
+from sympy.matrices.kind import MatrixKind
+from sympy.core.kind import NumberKind
+from sympy.assumptions.assume import AppliedPredicate
+from sympy.core.mul import Mul
+from sympy.core.singleton import S
+
+
+def lra_satask(proposition, assumptions=True, context=global_assumptions):
+    """
+    Function to evaluate the proposition with assumptions using SAT algorithm
+    in conjunction with an Linear Real Arithmetic theory solver.
+
+    Used to handle inequalities. Should eventually be depreciated and combined
+    into satask, but infinity handling and other things need to be implemented
+    before that can happen.
+    """
+    props = CNF.from_prop(proposition)
+    _props = CNF.from_prop(~proposition)
+
+    cnf = CNF.from_prop(assumptions)
+    assumptions = EncodedCNF()
+    assumptions.from_cnf(cnf)
+
+    context_cnf = CNF()
+    if context:
+        context_cnf = context_cnf.extend(context)
+
+    assumptions.add_from_cnf(context_cnf)
+
+    return check_satisfiability(props, _props, assumptions)
+
+# Some predicates such as Q.prime can't be handled by lra_satask.
+# For example, (x > 0) & (x < 1) & Q.prime(x) is unsat but lra_satask would think it was sat.
+# WHITE_LIST is a list of predicates that can always be handled.
+WHITE_LIST = ALLOWED_PRED | {Q.positive, Q.negative, Q.zero, Q.nonzero, Q.nonpositive, Q.nonnegative,
+                                            Q.extended_positive, Q.extended_negative, Q.extended_nonpositive,
+                                            Q.extended_negative, Q.extended_nonzero, Q.negative_infinite,
+                                            Q.positive_infinite}
+
+
+def check_satisfiability(prop, _prop, factbase):
+    sat_true = factbase.copy()
+    sat_false = factbase.copy()
+    sat_true.add_from_cnf(prop)
+    sat_false.add_from_cnf(_prop)
+
+    all_pred, all_exprs = get_all_pred_and_expr_from_enc_cnf(sat_true)
+
+    for pred in all_pred:
+        if pred.function not in WHITE_LIST and pred.function != Q.ne:
+            raise UnhandledInput(f"LRASolver: {pred} is an unhandled predicate")
+    for expr in all_exprs:
+        if expr.kind == MatrixKind(NumberKind):
+            raise UnhandledInput(f"LRASolver: {expr} is of MatrixKind")
+        if expr == S.NaN:
+            raise UnhandledInput("LRASolver: nan")
+
+    # convert old assumptions into predicates and add them to sat_true and sat_false
+    # also check for unhandled predicates
+    for assm in extract_pred_from_old_assum(all_exprs):
+        n = len(sat_true.encoding)
+        if assm not in sat_true.encoding:
+            sat_true.encoding[assm] = n+1
+        sat_true.data.append([sat_true.encoding[assm]])
+
+        n = len(sat_false.encoding)
+        if assm not in sat_false.encoding:
+            sat_false.encoding[assm] = n+1
+        sat_false.data.append([sat_false.encoding[assm]])
+
+
+    sat_true = _preprocess(sat_true)
+    sat_false = _preprocess(sat_false)
+
+    can_be_true = satisfiable(sat_true, use_lra_theory=True) is not False
+    can_be_false = satisfiable(sat_false, use_lra_theory=True) is not False
+
+    if can_be_true and can_be_false:
+        return None
+
+    if can_be_true and not can_be_false:
+        return True
+
+    if not can_be_true and can_be_false:
+        return False
+
+    if not can_be_true and not can_be_false:
+        raise ValueError("Inconsistent assumptions")
+
+
+def _preprocess(enc_cnf):
+    """
+    Returns an encoded cnf with only Q.eq, Q.gt, Q.lt,
+    Q.ge, and Q.le predicate.
+
+    Converts every unequality into a disjunction of strict
+    inequalities. For example, x != 3 would become
+    x < 3 OR x > 3.
+
+    Also converts all negated Q.ne predicates into
+    equalities.
+    """
+
+    # loops through each literal in each clause
+    # to construct a new, preprocessed encodedCNF
+
+    enc_cnf = enc_cnf.copy()
+    cur_enc = 1
+    rev_encoding = {value: key for key, value in enc_cnf.encoding.items()}
+
+    new_encoding = {}
+    new_data = []
+    for clause in enc_cnf.data:
+        new_clause = []
+        for lit in clause:
+            if lit == 0:
+                new_clause.append(lit)
+                new_encoding[lit] = False
+                continue
+            prop = rev_encoding[abs(lit)]
+            negated = lit < 0
+            sign = (lit > 0) - (lit < 0)
+
+            prop = _pred_to_binrel(prop)
+
+            if not isinstance(prop, AppliedPredicate):
+                if prop not in new_encoding:
+                    new_encoding[prop] = cur_enc
+                    cur_enc += 1
+                lit = new_encoding[prop]
+                new_clause.append(sign*lit)
+                continue
+
+
+            if negated and prop.function == Q.eq:
+                negated = False
+                prop = Q.ne(*prop.arguments)
+
+            if prop.function == Q.ne:
+                arg1, arg2 = prop.arguments
+                if negated:
+                    new_prop = Q.eq(arg1, arg2)
+                    if new_prop not in new_encoding:
+                        new_encoding[new_prop] = cur_enc
+                        cur_enc += 1
+
+                    new_enc = new_encoding[new_prop]
+                    new_clause.append(new_enc)
+                    continue
+                else:
+                    new_props = (Q.gt(arg1, arg2), Q.lt(arg1, arg2))
+                    for new_prop in new_props:
+                        if new_prop not in new_encoding:
+                            new_encoding[new_prop] = cur_enc
+                            cur_enc += 1
+
+                        new_enc = new_encoding[new_prop]
+                        new_clause.append(new_enc)
+                    continue
+
+            if prop.function == Q.eq and negated:
+                assert False
+
+            if prop not in new_encoding:
+                new_encoding[prop] = cur_enc
+                cur_enc += 1
+            new_clause.append(new_encoding[prop]*sign)
+        new_data.append(new_clause)
+
+    assert len(new_encoding) >= cur_enc - 1
+
+    enc_cnf = EncodedCNF(new_data, new_encoding)
+    return enc_cnf
+
+
+def _pred_to_binrel(pred):
+    if not isinstance(pred, AppliedPredicate):
+        return pred
+
+    if pred.function in pred_to_pos_neg_zero:
+        f = pred_to_pos_neg_zero[pred.function]
+        if f is False:
+            return False
+        pred = f(pred.arguments[0])
+
+    if pred.function == Q.positive:
+        pred = Q.gt(pred.arguments[0], 0)
+    elif pred.function == Q.negative:
+        pred = Q.lt(pred.arguments[0], 0)
+    elif pred.function == Q.zero:
+        pred = Q.eq(pred.arguments[0], 0)
+    elif pred.function == Q.nonpositive:
+        pred = Q.le(pred.arguments[0], 0)
+    elif pred.function == Q.nonnegative:
+        pred = Q.ge(pred.arguments[0], 0)
+    elif pred.function == Q.nonzero:
+        pred = Q.ne(pred.arguments[0], 0)
+
+    return pred
+
+pred_to_pos_neg_zero = {
+    Q.extended_positive: Q.positive,
+    Q.extended_negative: Q.negative,
+    Q.extended_nonpositive: Q.nonpositive,
+    Q.extended_negative: Q.negative,
+    Q.extended_nonzero: Q.nonzero,
+    Q.negative_infinite: False,
+    Q.positive_infinite: False
+}
+
+def get_all_pred_and_expr_from_enc_cnf(enc_cnf):
+    all_exprs = set()
+    all_pred = set()
+    for pred in enc_cnf.encoding.keys():
+        if isinstance(pred, AppliedPredicate):
+            all_pred.add(pred)
+            all_exprs.update(pred.arguments)
+
+    return all_pred, all_exprs
+
+def extract_pred_from_old_assum(all_exprs):
+    """
+    Returns a list of relevant new assumption predicate
+    based on any old assumptions.
+
+    Raises an UnhandledInput exception if any of the assumptions are
+    unhandled.
+
+    Ignored predicate:
+    - commutative
+    - complex
+    - algebraic
+    - transcendental
+    - extended_real
+    - real
+    - all matrix predicate
+    - rational
+    - irrational
+
+    Example
+    =======
+    >>> from sympy.assumptions.lra_satask import extract_pred_from_old_assum
+    >>> from sympy import symbols
+    >>> x, y = symbols("x y", positive=True)
+    >>> extract_pred_from_old_assum([x, y, 2])
+    [Q.positive(x), Q.positive(y)]
+    """
+    ret = []
+    for expr in all_exprs:
+        if not hasattr(expr, "free_symbols"):
+            continue
+        if len(expr.free_symbols) == 0:
+            continue
+
+        if expr.is_real is not True:
+            raise UnhandledInput(f"LRASolver: {expr} must be real")
+        # test for I times imaginary variable; such expressions are considered real
+        if isinstance(expr, Mul) and any(arg.is_real is not True for arg in expr.args):
+            raise UnhandledInput(f"LRASolver: {expr} must be real")
+
+        if expr.is_integer == True and expr.is_zero != True:
+            raise UnhandledInput(f"LRASolver: {expr} is an integer")
+        if expr.is_integer == False:
+            raise UnhandledInput(f"LRASolver: {expr} can't be an integer")
+        if expr.is_rational == False:
+            raise UnhandledInput(f"LRASolver: {expr} is irational")
+
+        if expr.is_zero:
+            ret.append(Q.zero(expr))
+        elif expr.is_positive:
+            ret.append(Q.positive(expr))
+        elif expr.is_negative:
+            ret.append(Q.negative(expr))
+        elif expr.is_nonzero:
+            ret.append(Q.nonzero(expr))
+        elif expr.is_nonpositive:
+            ret.append(Q.nonpositive(expr))
+        elif expr.is_nonnegative:
+            ret.append(Q.nonnegative(expr))
+
+    return ret