unicode_fol_kit.is_valid¶ unicode_fol_kit.is_valid(formula, timeout=10000)[source]¶ Return True if the formula is valid, i.e. its negation is unsatisfiable. A Z3 unknown result (e.g. on hard quantified formulas hitting the timeout) is treated as not-known-valid and returns False. Parameters: formula (Node) timeout (int) Return type: bool