txgraffiti.playground

txgraffiti.playground.conjecture

class txgraffiti.playground.conjecture.ConjecturePlayground(df, object_symbol='G', base=None)

Bases: object

append_row(row)

Append a new row (dict of col:value) to self.df, then clear any cached conjectures.

convert_columns(convert_dict)

discover(*args, **kwargs)

Run generate(…) with the given parameters, cache, and return the list.

Return type:

list[Conjecture]

discover_equalities(*, generators=None, min_fraction=0.15)

Find all single‐feature inequalities of the form L≤R or L≥R (with hypothesis TRUE) that are tight (slack==0) on at least min_fraction of the rows. For each, register & return a Predicate L_eq_R.

Return type:

list[Predicate]

exists(pred)

Return type:

bool

export_conjectures(path, format='json')

Write self.conjectures to disk in JSON or CSV form.

export_to_lean(path, name_prefix='conjecture', object_symbol=None)

Write all cached conjectures to path in Lean theorem‐stub format. Each theorem will be named {name_prefix}_{i}.

forall(pred)

Return type:

bool

generate(*, methods=None, features=None, target=None, hypothesis=None, heuristics=None, post_processors=None, **kwargs)

Return type:

Iterator[Conjecture]

prop(name)

Return type:

Property

reset(new_df=None)

If new_df is given, replace self.df; otherwise rebind the same DataFrame (e.g. after in-place edits). In either case, clear cached conjectures.

class txgraffiti.playground.conjecture.Exists(pred, df, object_symbol='G')

Bases: object

is_true()

Return type:

bool

witness()

Return type:

DataFrame

class txgraffiti.playground.conjecture.ForAll(conj, df, object_symbol='G')

Bases: object

counterexamples()

Return type:

DataFrame

is_true()

Return type:

bool

txgraffiti.playground.registry

txgraffiti.playground.registry.list_playgrounds()

Return all registered generator functions.

Return type:

list[Callable[..., Iterator[Conjecture]]]

txgraffiti.playground.registry.register_playground(fn)

Use as a plain decorator: :rtype: Callable[..., Iterator[Conjecture]]

@register_gen def convex_hull(…): …