kdrag.parsers.tptp

TPTP is a format for automated theorem provers. Read more about it at https://www.tptp.org/

Functions

test()

to_z3(tree[, sort])

Transform a TPTP parse tree into Z3 expressions.

Classes

FormulaRole(*values)

TPTPFormulaEntry(name, role, formula)

TPTPTransformer([sort, thf_mode])

class kdrag.parsers.tptp.FormulaRole(*values)

Bases: Enum

AXIOM = 'axiom'
CONJECTURE = 'conjecture'
classmethod __contains__(value)

Return True if value is in cls.

value is in cls if: 1) value is a member of cls, or 2) value is the value of one of the cls’s members. 3) value is a pseudo-member (flags)

classmethod __getitem__(name)

Return the member matching name.

classmethod __iter__()

Return members in definition order.

classmethod __len__()

Return the number of members (no aliases)

class kdrag.parsers.tptp.TPTPFormulaEntry(name: 'str', role: 'FormulaRole', formula: 'smt.BoolRef')

Bases: object

Parameters:
formula: BoolRef
name: str
role: FormulaRole
class kdrag.parsers.tptp.TPTPTransformer(sort: SortRef | None = None, thf_mode: bool = False)

Bases: Transformer

Parameters:

  • sort (smt.SortRef | None)

  • thf_mode (bool)

__default__(data, children, meta)

Default function that is called if there is no attribute matching data

Can be overridden. Defaults to creating a new copy of the tree node (i.e. return Tree(data, children, meta))

__default_token__(token)

Default function that is called if there is no attribute matching token.type

Can be overridden. Defaults to returning the token as-is.

__mul__(other: Transformer | TransformerChain[_Leaf_U, _Return_V]) → TransformerChain[_Leaf_T, _Return_V]

Chain two transformers together, returning a new transformer.

Parameters:

  • self (Transformer)

  • other (Transformer | TransformerChain[_Leaf_U, _Return_V])

Return type:

TransformerChain[_Leaf_T, _Return_V]

arguments(items)
atomic_formula(items)
cnf(items)
cnf_formula(items)
const(items)
const_sorts: dict[str, SortRef]
consts: dict[str, ExprRef]
diseq(items)
disjunction(items)
eq(items)
exists(items)
fof(items)
fof_and_formula(items)
fof_or_formula(items)
fof_variable_list(items)
forall(items)
fun_app(items)
func_sigs: dict[str, tuple[list[SortRef], SortRef | None]]
funcs: dict[tuple[str, int], FuncDeclRef]
iff(items)
implies(items)
neglit(items)
not_formula(items)
poslit(items)
predicate(items)
preds: dict[tuple[str, int], FuncDeclRef | BoolRef]
reverse_implies(items)
sorts: dict[str, SortRef]
start(items)
tff(items)
tff_type(items)
tff_type_atom(items)
tff_type_formula(items)
tff_type_product(items)
tff_typed_variable(items)
thf(items)
thf_and_formula(items)
thf_app(items)
thf_lambda(items)
thf_or_formula(items)
transform(tree: Tree[_Leaf_T]) → _Return_T

Transform the given tree, and return the final result

Parameters:

tree (Tree[_Leaf_T])

Return type:

_Return_T

var(items)
vars: dict[str, ExprRef]
kdrag.parsers.tptp.test()
>>> term_parser.parse("f(Xy1,g(y23))")
Tree('fun_app', [Token('NAME', 'f'), Tree(Token('RULE', 'arguments'), [Tree('var', [Token('UPPER_WORD', 'Xy1')]), Tree('fun_app', [Token('NAME', 'g'), Tree(Token('RULE', 'arguments'), [Tree('const', [Token('NAME', 'y23')])])])])])
kdrag.parsers.tptp.to_z3(tree: Tree, sort: SortRef | None = None) → list[TPTPFormulaEntry]

Transform a TPTP parse tree into Z3 expressions.

>>> import kdrag.parsers.tptp as tptp
>>> tree = tptp.fof_parser.parse("fof(a,axiom, p(a) ).")
>>> entries = tptp.to_z3(tree)
>>> entries[0].name
'a'
>>> entries[0].role
<FormulaRole.AXIOM: 'axiom'>
>>> entries[0].formula
p(a)
Parameters:

  • tree (Tree)

  • sort (SortRef | None)

Return type:

list[TPTPFormulaEntry]