Module Z3_mappings.SolverSource

make ?params ?logic () creates a new solver with optional parameters params and logic logic.

add_simplifier solver adds a simplifier to the solver solver.

clone solver creates a copy of the solver solver.

push solver pushes a new context level onto the solver solver.

pop solver n pops n context levels from the solver solver.

reset solver resets the solver solver to its initial state.

add solver exprs adds the expressions exprs to the solver solver.

check solver ~assumptions checks the satisfiability of the solver solver with the given assumptions. Returns `Sat, `Unsat, or `Unknown.

model solver retrieves the model from the solver solver, if one exists.

interrupt solver interrupts the current solver operation.

get_statistics solver retrieves statistics from the solver solver.