mod package:what4

mod x1 x2 returns x1 - x2 * (x1 div [x2])@. The terms are expected to have type Int.

A line in the model response

Necessary monadic operations

Mode flag for how floating-point values should be interpreted.

Reduce a weighted sum of integers modulo a concrete integer. This reduces each of the coefficients modulo the given integer, removing any that are congruent to 0; the offset value is also reduced.

Desired instances for the IsInterpretedFloatExprBuilder class are selected via the different mode values from this module.

Rounding modes for IEEE-754 floating point operations.

intMod x y computes the integer modulus of x by y. See intDiv for more details. The value of intMod x y is undefined when y = 0. Integer modulus requires nonlinear support whenever the divisor is not a constant.

natMod sym x y returns x mod y. See natDiv for a description of the properties the return value is expected to satisfy.

realMod x y returns the value of x - y * floor(x / y) when y is not zero and x when y is zero.

Send a check command to the solver and get the model in the case of a SAT result.

Check if the formula is satisifiable in the current solver state. This is done in a fresh frame, which is exited after the continuation complets. The evaluation function can be used to query the model. The model is valid only in the given continuation.

Following a successful check-sat command, build a ground evaluation function that will evaluate terms in the context of the current model.

Set the produce models option (We typically want this)

The parsed declarations and definitions returned by "(get-model)"