kdrag.solvers

Facilities for pretty printing and calling external solvers

To install extra solvers, run either: ` python3 -m kdrag.solvers install # install extra solvers `

or from project root run

` ./install.sh # install extra solvers `

Functions

binpath(cmd)
collect_decls(exprs)
collect_sorts(exprs)
download(url, filename, checksum)
install_solvers()
install_solvers2()
run(cmd, args, **kwargs)
smt2tptp(smt_filename, outfile[, format])
tptp2smt(tptp_filename)

Classes

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

class kdrag.solvers.BaseSolver

Bases: object

a = a

add(thm: BoolRef)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• 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() → object

Return type:

object

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.EProverSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.EProverTHFSolver

Bases: EProverSolver

a = a

add(thm: BoolRef)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

set(option, value)

unsat_core()

write_smt(fp)

write_tptp(filename, format='thf')

x = x

y = y

z = z

class kdrag.solvers.LeanSolver

Bases: BaseSolver

a = a

add(thm: BoolRef)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof()

query(q)

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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)

Parameters:

thm (BoolRef)

assert_and_track(thm: BoolRef, name: str)

Parameters:

• thm (BoolRef)

• name (str)

b = b

c = c

check()

check_tptp_status(res)

k = k

m = m

n = n

options: dict

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

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

proof() → object

Return type:

object

res: CompletedProcess | None

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) → set[FuncDeclRef]

Return type:

set[FuncDeclRef]

kdrag.solvers.collect_sorts(exprs) → set[SortRef]

Return type:

set[SortRef]

kdrag.solvers.download(url, filename, checksum) → bool

Return type:

bool

kdrag.solvers.install_solvers()

kdrag.solvers.install_solvers2()

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

kdrag.solvers.smt2tptp(smt_filename, outfile, format='tff')

kdrag.solvers.tptp2smt(tptp_filename)

Modules

aprove
datalog
egraph
gappa
kb	Knuth Bendix completion.
ljt	Dyckhoff Intuitionistic Propositional Prover
prolog
sat
sympy