prodigy.analysis.solver.smtz3_solver

class SMTZ3Solver(dist_factory)

Bases: Solver

Parameters:

dist_factory (CommonDistributionsFactory)

logger = <Logger Z3Solver (DEBUG)>

solve(f, g)

WARNING: This method currently just tries to find models which are positive FPS by design. We hence do not have completeness of the algorithm for a given template.

Parameters:

• f (Distribution)

• g (Distribution)

Return type:

Tuple[bool | None, List[Dict[Expr, Expr]]]