kdrag.solvers

Facilities for pretty printing and calling external solvers

Functions

binpath(cmd)
collect_decls(exprs)
collect_sorts(exprs)
expr_to_smtlib(expr)
expr_to_tptp(expr[, env, format, theories])	Pretty print expr as TPTP
funcdecl_smtlib(decl)
install_solvers()
mangle_decl(d[, env])	Mangle a declaration to a tptp name.
mangle_decl_smtlib(d)	Mangle a declaration to remove overloading
run(cmd, args, **kwargs)
smtlib_datatypes(dts)
sort_to_tptp(sort)	Pretty print sort as tptp

Classes

BaseSolver()
EProverTHFSolver()
LeoIIISolver()
MultiSolver([solvers, strict])
NanoCopISolver()
SATSolver()
TweeSolver()
VampireSolver()
VampireTHFSolver()
ZipperpositionSolver()

class kdrag.solvers.BaseSolver

Bases: object

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.EProverTHFSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.LeoIIISolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.MultiSolver(solvers=None, strict=False)

Bases: BaseSolver

a = a

add(thm)

assert_and_track(thm, name)

b = b

c = c

check(strict=False)

with concurrent.futures.ThreadPoolExecutor(

max_workers=len(self.solvers)

) as executor:

results = list(executor.map(lambda s: s.check(), self.solvers))

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

solver_classes = [<class 'kdrag.solvers.VampireTHFSolver'>, <class 'kdrag.solvers.EProverTHFSolver'>, <class 'kdrag.solvers.LeoIIISolver'>]

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.NanoCopISolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.SATSolver

Bases: object

add(clause)

check(debug=False)

class kdrag.solvers.TweeSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.VampireSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

query(q)

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.VampireTHFSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.ZipperpositionSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

assert_and_track(thm: BoolRef, name: str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

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

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

proof()

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

kdrag.solvers.binpath(cmd)

kdrag.solvers.collect_decls(exprs)

kdrag.solvers.collect_sorts(exprs)

kdrag.solvers.expr_to_smtlib(expr: ExprRef)

kdrag.solvers.expr_to_tptp(expr: ExprRef, env=None, format='thf', theories=True)

Pretty print expr as TPTP

kdrag.solvers.funcdecl_smtlib(decl: FuncDeclRef)

kdrag.solvers.install_solvers()

kdrag.solvers.mangle_decl(d: FuncDeclRef, env=[])

Mangle a declaration to a tptp name. SMTLib supports type based overloading, TPTP does not.

kdrag.solvers.mangle_decl_smtlib(d: FuncDeclRef)

Mangle a declaration to remove overloading

kdrag.solvers.run(cmd, args, **kwargs)

kdrag.solvers.smtlib_datatypes(dts: list[DatatypeSortRef]) → str

kdrag.solvers.sort_to_tptp(sort: SortRef)

Pretty print sort as tptp

Modules

aprove
egglog
gappa