kdrag.Guard

kdrag.Guard(cond: BoolRef, body: ExprRef) → ExprRef

Make a guard over an expression. If the condition is true, this is just the expression. If the condition is false, this is an unconstrained value of the same sort as the expression.

>>> x = smt.Real("x")
>>> Guard(x >= 0, smt.Sqrt(x))
Real.guard(x >= 0, x**(1/2))

Parameters:

• cond (BoolRef)

• body (ExprRef)

Return type:

ExprRef