kdrag.printers.prolog

Functions

to_clause(e)
to_prolog(vs, expr)

kdrag.printers.prolog.to_clause(e: BoolRef) → str

>>> x,y = smt.Ints("x y")
>>> to_clause(smt.ForAll([x, y], smt.Or(x == y, x + 1 <= y)))
 '((X = Y) ; ((X + 1) #=< Y)).'

Parameters:

e (BoolRef)

Return type:

str

kdrag.printers.prolog.to_prolog(vs: list[ExprRef], expr: ExprRef) → str

>>> x,y = smt.Ints("x y")
>>> to_prolog([x,y], smt.Or(x == 0, x == y))
'((X = 0) ; (X = Y))'

Parameters:

• vs (list[ExprRef])

• expr (ExprRef)

Return type:

str