unicode_fol_kit.is_satisfiable_arith

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

Return True iff formula has a model under interpreted arithmetic.

Translates with to_z3_arith() and asks Z3 for a model. A Z3 unknown result (e.g. a hard quantified formula hitting timeout milliseconds) is treated as not-known-satisfiable 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