unicode_fol_kit.get_model

unicode_fol_kit.get_model(formula, timeout=10000)

Return a satisfying assignment as a dict, or None if unsat/unknown.

The dict maps each Z3 declaration name (constants, uninterpreted functions/predicates) to the string form of its interpretation. For an invalid equivalence or entailment, get_model(Not(...)) yields the concrete counterexample. Returns None when the formula is unsatisfiable or Z3 cannot decide it within the timeout.

Parameters:

• formula (Node)

• timeout (int)