package smtml

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

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 ts adds the terms ts 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.

add_simplifier solver adds a simplifier to the solver solver.

interrupt () interrupts the current solver operation.

get_statistics solver retrieves statistics from the solver solver.

pp_statistics fmt solver pretty-prints the statistics of the solver solver using the formatter fmt.