kdrag.solvers.gappa

Functions

`gappa_of_bool`(e)
`gappa_of_real`(e)

Classes

GappaSolver()

class kdrag.solvers.gappa.GappaSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

Parameters:: thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

thm (BoolRef)
name (str)

b = b

bound(e: ExprRef)

Parameters:: e (ExprRef)

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

predefined = [And, Or, Not, Implies, -, +, *, ==, <=]

predefined_sorts = ['Int', 'Real', 'Bool']

proof() → object

Return type:: object

res: subprocess.CompletedProcess | None

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

kdrag.solvers.gappa.gappa_of_bool(e: BoolRef)

Parameters:: e (BoolRef)

kdrag.solvers.gappa.gappa_of_real(e: ArithRef)

Parameters:: e (ArithRef)