txgraffiti.processing

txgraffiti.processing.postprocessors

Post‐processing functions for TxGraffiti conjecture pipelines.

Each function is registered under a short name via the @register_post decorator and can be applied in a ConjecturePlayground’s post_processors step.

txgraffiti.processing.postprocessors.extract_equalities(conjs, df)

Given conjectures whose conclusions are Inequalities, check each one:

– if on all rows where the hypothesis holds the slack == 0,

convert it to an equality Conjecture (lhs == rhs);

– otherwise keep the original inequality Conjecture.

Return type:

(equalities, inequalities)

txgraffiti.processing.postprocessors.remove_duplicates(conjs, df)

Remove duplicate conjectures based on hypothesis and conclusion names.

This post‐processor walks through the list of conjectures in order and only keeps the first occurrence of each unique (hypothesis.name, conclusion.name) pair.

Parameters:

• conjs (List[Conjecture]) – The list of conjectures to filter.

• df (pandas.DataFrame) – The DataFrame on which these conjectures were evaluated (not used in this function).

Returns:

A new list containing only the first instance of each unique hypothesis/conclusion combination.

Return type:

List[Conjecture]

txgraffiti.processing.postprocessors.sort_by_accuracy(conjs, df)

Sort conjectures by descending accuracy on the DataFrame.

Parameters:

• conjs (List[Conjecture]) – The list of conjectures to sort.

• df (pandas.DataFrame) – The DataFrame on which to compute each conjecture’s accuracy.

Returns:

A new list of conjectures sorted so that the highest‐accuracy conjecture comes first.

Return type:

List[Conjecture]

txgraffiti.processing.postprocessors.sort_by_touch_count(conjs, df)

Sort conjectures by descending touch count (slack‐zero instances).

The touch count of an inequality is the number of rows where its conclusion holds with equality (zero slack). This post‐processor brings conjectures with more tight instances to front.

Parameters:

• conjs (List[Conjecture]) – The list of conjectures to sort.

• df (pandas.DataFrame) – The DataFrame on which to compute each conjecture’s touch count.

Returns:

A new list of conjectures sorted so that those with the highest touch counts appear first.

Return type:

List[Conjecture]