unicode_fol_kit.is_valid_arith

unicode_fol_kit.is_valid_arith(formula, sort='real', timeout=10000)

Return True iff formula is valid under interpreted arithmetic.

A formula is valid exactly when its negation is unsatisfiable, so this asks Z3 to refute ¬formula. A Z3 unknown result (e.g. hitting timeout milliseconds) is treated as not-known-valid and returns False.

Parameters:

• formula (Node) – the formula to check.

• sort (str) – 'real' (default) or 'int' numeric sort.

• timeout (int) – solver timeout in milliseconds.

Return type:

bool