### Install TxGraffiti from source Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/getting_started/installation.rst.txt Clones the repository and installs TxGraffiti in editable mode. ```bash git clone https://github.com/RandyRDavila/TxGraffiti2.git cd txgraffiti pip install -e . ``` -------------------------------- ### Install TxGraffiti with all extras Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/getting_started/installation.rst.txt Installs TxGraffiti with all optional dependencies, including pulp, scipy, networkx, and lean4-export. ```bash pip install "txgraffiti[all]" ``` -------------------------------- ### Verify TxGraffiti installation Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/getting_started/installation.rst.txt Runs a Python script to print the installed TxGraffiti version, confirming the installation. ```bash python - <= ((-3 * D) + 9))> = 3)> ``` -------------------------------- ### Sophie heuristic complete example with txgraffiti Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/history_with_txgraffiti/graffiti_pc/index.rst.txt Complete example of the Sophie heuristic on a small pandas DataFrame. It builds three conjectures from TxGraffiti Property and Predicate objects, then uses sophie_accept to accept c1 and c2 (each adds a new row) and reject c3 (adds no new row beyond the union). Requires txgraffiti.logic and txgraffiti.heuristics. ```python import pandas as pd from txgraffiti.logic import Property, Predicate from txgraffiti.heuristics import sophie_accept # 1) Sample data df = pd.DataFrame({ 'alpha': [1, 2, 3, 4], 'p': [True, True, False, False], 'q': [False, True, True, False], }) # 2) Lift into TxGraffiti objects A = Property('alpha', lambda df: df['alpha']) P = Predicate('p', lambda df: df['p']) Q = Predicate('q', lambda df: df['q']) # 3) Build three conjectures # c1 covers rows 0 and 1 c1 = P >> (A <= 10) # c2 covers rows 1 and 2 c2 = Q >> (A <= 10) # c3 covers rows 0,1,2 but adds no new row beyond c1,c2 P_or_Q = P | Q c3 = P_or_Q >> (A <= 10) # 4) Apply Sophie accepted = [] # c1 is first → covers new rows ⇒ accept assert sophie_accept(c1, accepted, df) is True accepted.append(c1) # c2 adds row 2 beyond c1’s cover ⇒ accept assert sophie_accept(c2, accepted, df) is True accepted.append(c2) # c3 adds no new rows beyond {0,1,2} ⇒ reject assert sophie_accept(c3, accepted, df) is False ``` -------------------------------- ### Load CSV datasets and example graphs with importlib.resources Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/example_data.html Loads CSV datasets and example graphs from package resources using importlib.resources for zip/wheel-safe access. The CSV loader drops an 'Unnamed: 0' column from several datasets, and load_example_graphs reads .txt edge lists from the 'graph-edgelists' folder, returning graphcalc.SimpleGraph objects named by filename. ```python import pandas as pd import importlib.resources as pkg_resources def _load_csv(name: str) -> pd.DataFrame: # Zip/wheel safe: open text resource from this package with pkg_resources.open_text(__name__, name) as fp: return pd.read_csv(fp) # Expose CSVs at import time graph_data = _load_csv("graph_data.csv") integer_data = _load_csv("integer_data.csv") integer_data.drop(columns=['Unnamed: 0'], inplace=True) nba_game_data = _load_csv("nba_game_data.csv") calabi_yau_data = _load_csv("calabi_yau_data.csv") polytope_data = _load_csv("polytope_data.csv") polytope_data.drop(columns=['Unnamed: 0'], inplace=True) qubits_data = _load_csv("Nqubits_data.csv") qubits_data.drop(columns=['Unnamed: 0'], inplace=True) # ---- Example graphs loader (zip-safe) ---- import networkx as nx from importlib.resources import files import graphcalc as gc # if this creates a circular import, see note below [docs] def load_example_graphs() -> dict: """ Load all example graphs from the ``graph-edgelists`` resource folder. Each ``.txt`` file is a plain-text edge list (one edge per line). Graphs are returned as :class:`graphcalc.SimpleGraph` with names taken from the filename (without extension). Returns ------- dict Mapping from graph name (str) to :class:`graphcalc.SimpleGraph`. """ graphs = [] # Use importlib.resources for zip/wheel-safe resource access base_dir = files(__package__).joinpath("graph-edgelists") for file in base_dir.iterdir(): if file.suffix != ".txt": continue # NetworkX can read from a path-like object G_nx = nx.read_edgelist(file, nodetype=int) # Wrap into your SimpleGraph and preserve the filename as the name graphs.append(gc.SimpleGraph(G_nx.edges, name=file.stem)) return graphs ``` -------------------------------- ### Sophie heuristic acceptance example Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/heuristics/sophie.html Demonstrates using sophie_accept to decide whether to accept a new conjecture based on its cover set. The example creates a DataFrame and two conjectures, then shows that a conjecture covering the same rows as an accepted one is rejected, while a conjecture covering an additional row is accepted. ```python >>> import pandas as pd >>> from txgraffiti.logic import Property, Predicate, Conjecture >>> from txgraffiti.heuristics.delavina import sophie_accept >>> df = pd.DataFrame({ ... 'alpha': [1, 2, 3, 4], ... 'connected': [True, False, True, False], ... }) >>> A = Property('alpha', lambda df: df['alpha']) >>> P = Predicate('connected', lambda df: df['connected']) >>> # conj1 covers rows 0 and 2 >>> conj1 = P >> (A <= 10) >>> # conj2 covers the same rows → no new coverage >>> conj2 = P >> (A >= 0) >>> sophie_accept(conj2, [conj1], df) False >>> # conj3 covers row 0,2, plus row 1 (connected=False so hypothesis False) >>> # so still no new coverage >>> sophie_accept(conj3:= (P | ~P) >> (A >= 0), [conj1], df) True ``` -------------------------------- ### Quantify a Predicate with forall and exists Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/predicates.rst.txt Wrap a Predicate in universal (∀) or existential (∃) quantifiers using a ConjecturePlayground instance. The example shows the printed symbolic forms for the 'tree' predicate. ```python from txgraffiti.playground import ConjecturePlayground pg = ConjecturePlayground(df, object_symbol='G') print(pg.forall(tree)) # prints "∀ G: tree" print(pg.exists(tree)) # prints "∃ G: tree" ``` -------------------------------- ### Create an Inequality from Property comparisons Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/predicates.rst.txt Create Property objects and combine them with arithmetic and comparison to form an Inequality (a subclass of Predicate). The example shows the symbolic name of the inequality and how to combine it with a Boolean predicate using AND. ```python from txgraffiti.logic.conjecture_logic import Property A = Property('alpha', lambda df: df['alpha']) C = Property('cost', lambda df: df['beta'] * 2) test = (A + 1 >= C) print(test.name) # → "(alpha + 1) ≥ (beta * 2)" # Combine numeric tests with Boolean predicates: conj = tree & test print(conj.name) # → "(tree) ∧ (alpha + 1 ≥ beta * 2)" ``` -------------------------------- ### Generate linear programming bounds with txgraffiti Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/generators/linear_programming.rst.txt Minimal example on a toy DataFrame that generates linear bounds on 'alpha' in terms of 'beta' under the hypothesis 'connected'. Requires an LP solver (CBC or GLPK) on PATH and the pulp, numpy, and pandas packages. The printed output shows the two conjectures emitted by the generator. ```python import pandas as pd from txgraffiti.logic import Property, Predicate from txgraffiti.generators.optimization import linear_programming # Sample data df = pd.DataFrame({ 'alpha': [1, 2, 3, 4], 'beta': [3, 1, 1, 2], 'connected': [True, True, True, True], }) # Lift into TxGraffiti objects A = Property('alpha', lambda df: df['alpha']) B = Property('beta', lambda df: df['beta']) H = Predicate('connected', lambda df: df['connected']) # Generate linear bounds on alpha in terms of beta under H for conj in linear_programming( df, features=[B], target=A, hypothesis=H ): print(conj) ``` ```text (connected) → (alpha >= ((-1/2 * beta) + 5/2)) (connected) → (alpha <= ((-1 * beta) + 4)) ``` -------------------------------- ### Using morgan_accept with pandas DataFrame Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/heuristics/davila.html Shows how to use `morgan_accept` with a pandas DataFrame and `Predicate`/`Property` objects. The example creates two conjectures, `c1` (tree) and `c2` (connected), and verifies that the more general hypothesis `c2` is accepted while the less general `c1` is rejected. ```python >>> import pandas as pd >>> from txgraffiti.logic import Predicate, Property, Conjecture, Inequality >>> from txgraffiti.heuristics.davila import morgan_accept >>> df = pd.DataFrame({ ... 'alpha': [1, 2, 3], ... 'beta': [3, 2, 1], ... 'connected': [True, True, True], ... 'tree': [False, True, False], ... }) >>> P_gen = Predicate('connected', lambda df: df['connected']) >>> P_sub = Predicate('tree', lambda df: df['tree']) >>> A = Property('alpha', lambda df: df['alpha']) >>> B = Property('beta', lambda df: df['beta']) >>> # less general hypothesis on tree >>> c1 = P_sub >> (A <= B) >>> # more general hypothesis on connected >>> c2 = P_gen >> (A <= B) >>> # c2 covers strictly more rows → accept c2 but not c1 if c2 exists >>> morgan_accept(c1, [c2], df) False >>> morgan_accept(c2, [c1], df) True ``` -------------------------------- ### Test dalmatian_accept with pandas DataFrame and Conjecture objects Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/heuristics/fajtlowicz.html Use this example to see how the Dalmatian heuristic accepts or rejects conjectures. It builds a small DataFrame and three conjectures (weak, strong, best) with the same hypothesis and left-hand side, then shows that no existing bounds cause acceptance, a weaker bound is rejected, and a strictly tighter bound is accepted. ```python >>> import pandas as pd >>> from txgraffiti.logic import Property, Predicate, Conjecture, Inequality >>> from txgraffiti.heuristics.fajtlowicz import dalmatian_accept >>> df = pd.DataFrame({ ... 'alpha': [1, 1, 1], ... 'beta': [1, 1, 1], ... 'connected': [True, True, True], ... }) >>> P = Predicate('connected', lambda df: df['connected']) >>> A = Property('alpha', lambda df: df['alpha']) >>> B = Property('beta', lambda df: df['beta']) >>> weak = P >> (A <= B + 2) >>> strong = P >> (A <= B + 1) >>> best = P >> (A <= B) >>> # No existing bounds ⇒ accept >>> dalmatian_accept(best, [], df) True >>> # Reject the weaker conjecture >>> dalmatian_accept(weak, [strong], df) False >>> # Accept the strictly tighter one >>> dalmatian_accept(best, [strong], df) True ``` -------------------------------- ### Expected Output from convex_hull generator Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/generators/convex_hull.html The expected output when running the usage example. It shows two conjectures with rational coefficients, one for alpha >= and one for alpha <=. ```text (connected) → (alpha >= ((-1/2 * beta) + 5/2)) (connected) → (alpha <= ((-1 * beta) + 4)) ``` -------------------------------- ### Create Conjecture with three methods Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/conjectures.rst.txt Builds a Conjecture using the direct constructor, .implies(..., as_conjecture=True), and the >> operator. Requires a DataFrame with columns 'alpha', 'beta', 'connected', 'tree'. The example prints the conjecture, the boolean mask from calling it, and the result of is_true(df). ```python import pandas as pd from txgraffiti.logic.conjecture_logic import ( Property, Predicate, Conjecture, TRUE ) # Sample DataFrame df = pd.DataFrame({ 'alpha': [1, 2, 3], 'beta': [3, 1, 1], 'connected':[True, True, True], 'tree': [False, False, True], }) # Lift numeric columns to Property alpha = Property('alpha', lambda df: df['alpha']) beta = Property('beta', lambda df: df['beta']) # Hypothesis and conclusion hypothesis = Predicate('connected', lambda df: df['connected']) conclusion = alpha <= (2 * beta + 3) # 1) Direct constructor conj1 = Conjecture(hypothesis, conclusion) print(f"conj1 = {conj1}") print(conj1(df)) print(f"conj1.is_true(df) = {conj1.is_true(df)}\n") # 2) Using .implies(..., as_conjecture=True) conj2 = hypothesis.implies(conclusion, as_conjecture=True) print(f"conj2 = {conj2}") print(conj2(df)) print(f"conj2.is_true(df) = {conj2.is_true(df)}\n") # 3) Using >> operator conj3 = hypothesis >> conclusion print(f"conj3 = {conj3}") print(conj3(df)) print(f"conj3.is_true(df) = {conj3.is_true(df)}\n") ``` ```text conj1 = 0 True 1 True 2 True dtype: bool conj1.is_true(df) = True conj2 = 0 True 1 True 2 True dtype: bool conj2.is_true(df) = True conj3 = 0 True 1 True 2 True dtype: bool conj3.is_true(df) = True ``` -------------------------------- ### Python example: Generate convex hull conjectures with TxGraffiti Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/history_with_txgraffiti/graphedron/index.rst.txt Builds a dataframe of graph invariants (diameter D, size m) for several connected graphs, defines Property and Predicate objects, and calls convex_hull to print conjectures. Requires networkx, pandas, txgraffiti, and graphcalc (or custom invariant functions). ```python import networkx as nx import pandas as pd from txgraffiti.logic import Property, TRUE from txgraffiti.generators import convex_hull from itertools import combinations from graphcalc import diameter, size # replace with your actual graph invariant functions # Generate all connected 4-vertex graphs paw = nx.Graph() paw.add_edges_from([(0, 1), (1, 2), (1, 3), (3, 0), (0, 4)]) graphs = [ nx.star_graph(3), # (2, 3) nx.path_graph(4), # (3, 3) paw, # (2, 3) + isolated node nx.cycle_graph(4), # (2, 4) nx.Graph([(0,1), (1,2), (2,3), (0,2), (1,3)]), # (2, 5) nx.complete_graph(4) # (1, 6) ] # Build dataframe of invariants df = pd.DataFrame({ "name": [f"G{i}" for i in range(len(graphs))], "D": [diameter(G) for G in graphs], "m": [size(G) for G in graphs], 'connected_graph': [True for G in graphs], }) D = Property("D", lambda df: df["D"]) m = Property("m", lambda df: df["m"]) connected = Predicate("connected graph", lambda df: df["connected_graph"]) for conj in convex_hull(df, features=[D], target=m, hypothesis=connected): print(conj) ``` -------------------------------- ### Create and use a Property Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/logic/properties.html Demonstrates how to initialize a Property from a DataFrame column and perform arithmetic operations on it. ```python from txgraffiti.logic import Property >>> deg = Property("deg", lambda df: df["degree"]) >>> 2 * deg + 3 ``` -------------------------------- ### Load graph data with txgraffiti.example_data Source: https://txgraffiti2.readthedocs.io/en/latest/getting_started/quickstart.html Loads the built-in graph dataset as a pandas DataFrame. Use this as the first step before creating a ConjecturePlayground session. ```python from txgraffiti.example_data import graph_data df = graph_data # structured invariants for connected graphs ``` -------------------------------- ### ForAll.counterexamples() Source: https://txgraffiti2.readthedocs.io/en/latest/api/txgraffiti.playground.html Returns a DataFrame containing counterexamples to the universal predicate. ```APIDOC ## ForAll.counterexamples() ### Description Returns a DataFrame containing counterexamples to the universal predicate. ### Method counterexamples ### Returns - **DataFrame** - The counterexample rows. ``` -------------------------------- ### Using quantifiers in ConjecturePlayground Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/logic/predicates.html Demonstrates wrapping predicates with forall and exists quantifiers inside a ConjecturePlayground instance, printing the symbolic forms. ```python from txgraffiti.playground import ConjecturePlayground pg = ConjecturePlayground(df, object_symbol='G') print(pg.forall(tree)) # prints "∀ G: tree" print(pg.exists(tree)) # prints "∃ G: tree" ``` -------------------------------- ### Create and Combine Constants Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/properties.rst.txt Demonstrates creating Constant objects and performing arithmetic operations on them. ```python from txgraffiti import Constant c2 = Constant(2) c3 = Constant(3) print(c2) # print(c2(df)) # Series: [2, 2, 2] print(c2 + c3) # print((c2 + c3)(df)) # [5, 5, 5] expr = 2*c2 - c3 print(expr) # print(expr(df)) # [1, 1, 1] ``` -------------------------------- ### Combine Predicates with AND operator Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/predicates.rst.txt Create two Predicates from lambda expressions and combine them with the AND operator (&). The example shows the symbolic name of the combined predicate and its evaluation on the DataFrame, producing a boolean mask. ```python # Build two simple Predicates from columns: is_high_alpha = Predicate('high_alpha', lambda df: df['alpha'] >= 3) is_low_beta = Predicate('low_beta', lambda df: df['beta'] <= 1) # Combine them: combo = is_high_alpha & is_low_beta print(combo.name) # → "(high_alpha) ∧ (low_beta)" # Evaluate: print(combo(df)) # 0 False # 1 False # 2 True # dtype: bool ``` -------------------------------- ### Create and manipulate symbolic expressions with KnowledgeTable Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/logic/tables.html Shows how to instantiate a KnowledgeTable from a dictionary, access columns as Property objects, perform arithmetic (alpha + beta), and use Predicate logic (kt.tree & (alpha == 3)). The printed outputs are [4, 3, 4] and [False, False, True]. ```python from txgraffiti.logic.tables import KnowledgeTable kt = KnowledgeTable({ 'alpha': [1, 2, 3], 'beta': [3, 1, 1], 'tree': [False, False, True], }) alpha = kt.alpha # ← Property('alpha') beta = kt.beta # ← Property('beta') # Properties support arithmetic expr1 = alpha + beta print(expr1(kt)) # [4, 3, 4] # Logical operations using Predicates pred = kt.tree & (alpha == 3) print(pred(kt)) # [False, False, True] ``` -------------------------------- ### Integration with ConjecturePlayground Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/generators/convex_hull.html Shows how to use convex_hull inside ConjecturePlayground with the discover method, passing methods, features, target, and hypothesis as arguments. ```python from txgraffiti.playground import ConjecturePlayground pg = ConjecturePlayground(df, object_symbol='G') pg.discover( methods = [convex_hull], features = ['beta', 'gamma'], target = 'alpha', hypothesis= 'connected', ) ``` -------------------------------- ### Evaluate a Predicate to get a boolean mask Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/predicates.rst.txt Apply a Predicate to a DataFrame to obtain a pandas.Series[bool] mask. The output shows the boolean mask for the 'tree' column, with True only for the row where tree is True. ```python mask = tree(df) print(mask) # Output: # 0 False # 1 False # 2 True # Name: tree, dtype: bool ``` -------------------------------- ### Initialize KnowledgeTable and access numeric Property Source: https://txgraffiti2.readthedocs.io/en/latest/api/txgraffiti.logic.html Demonstrates creating a KnowledgeTable from a pandas DataFrame and accessing a numeric column as a Property. ```python >>> import pandas as pd >>> from txgraffiti.logic.tables import KnowledgeTable >>> df = pd.DataFrame({ ... 'alpha': [1, 2, 3], ... 'connected': [True, False, True], ... }) >>> kt = KnowledgeTable(df) >>> # Numeric column lifts to Property: >>> prop = kt.alpha >>> print(prop(df)) 0 1 1 2 2 3 Name: alpha, dtype: int64 ``` -------------------------------- ### Lift DataFrame Columns into Properties Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/properties.rst.txt Shows how to lift DataFrame columns into Property objects and build symbolic expressions. ```python from txgraffiti import Property alpha = Property('alpha', lambda df: df['alpha']) beta = Property('beta', lambda df: df['beta']) print(alpha) # print(alpha(df)) # [1, 2, 3] expr1 = 2 * alpha print(expr1) # print(expr1(df)) # [2, 4, 6] combo = alpha*alpha + 5 print(combo) # print(combo(df)) # [6, 9, 14] ``` -------------------------------- ### Lift a Boolean column into a Predicate Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/predicates.rst.txt Lift an existing Boolean column into a Predicate using the Predicate constructor with a lambda that returns the column. The example also shows how to inspect the symbolic name with print(tree), which outputs . ```python import pandas as pd from txgraffiti.logic.conjecture_logic import Predicate df = pd.DataFrame({ 'alpha': [1, 2, 3], 'beta': [3, 1, 1], 'connected':[True, True, True], 'tree': [False, False, True], }) # 1) Lift an existing Boolean column: tree = Predicate('tree', lambda df: df['tree']) # 2) Inspect its symbolic form: print(tree) # → ``` -------------------------------- ### Define and Combine Properties Source: https://txgraffiti2.readthedocs.io/en/latest/api/txgraffiti.logic.html Shows how to define a custom Property using a lambda function and combine it with arithmetic operators. ```python from txgraffiti.logic import Property >>> deg = Property(“deg”, lambda df: df[“degree”]) >>> 2 * deg + 3 ``` -------------------------------- ### Run full conjecture discovery and export to Lean4 with ConjecturePlayground Source: https://txgraffiti2.readthedocs.io/en/latest/key_features/playground/index.html Use this snippet to run a full conjecture discovery workflow with ConjecturePlayground: load a DataFrame, mine equality hypotheses, run discovery with generators, heuristics, and post-processors, export to Lean4, and print the top three conjectures. Requires a CSV file named graph_data.csv and the txgraffiti package. The export call uses keyword arguments with type annotations (object_symbol: str = "G", object_decl: str = "SimpleGraph V") as shown in the source. ```python import pandas as pd from txgraffiti.playground import ConjecturePlayground from txgraffiti.generators import convex_hull, ratios, lp_model from txgraffiti.heuristics import morgan, dalmatian from txgraffiti.postprocessing import remove_duplicates, sort_by_touch_count # 1) Load your DataFrame df = pd.read_csv("graph_data.csv") # 2) Create a playground with base hypothesis “connected” pg = ConjecturePlayground(df, object_symbol="G", base="connected") # 3) Auto-mine any equality hypotheses holding ≥20% of rows new_hyps = pg.discover_equalities(min_fraction=0.2) # 4) Run full discovery over two hypotheses: conjs = pg.discover( methods = [convex_hull, ratios, lp_model], features = ['order','matching_number','min_degree'], target = 'independence_number', hypothesis = new_hyps, # includes base ∧ each discovered heuristics = [morgan, dalmatian], post_processors = [remove_duplicates, sort_by_touch_count], round_decimals = 2, drop_coeff_below= 0.05, ) # 5) Export to Lean pg.conjecture_to_lean4( "graph_conjectures.lean", name="graph_conj", object_symbol: str = "G", object_decl: str = "SimpleGraph V", ) # 6) Wrap and print top 3 for i, conj in enumerate(pg.conjectures[:3], start=1): print(f"Conjecture {i}.", pg.forall(conj)) ``` -------------------------------- ### Discover inequalities with ConjecturePlayground and print conjectures Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/inequalities.rst.txt Runs inequality discovery on the built-in graph_data dataset using three methods (ratios, convex_hull, linear_programming) with a custom cubic predicate, then prints the first three conjectures. The output shows the generated inequalities in universal form. ```python from txgraffiti.playground import ConjecturePlayground from txgraffiti.generators import convex_hull, linear_programming, ratios from txgraffiti.heuristics import dalmatian_accept, morgan_accept from txgraffiti.processing import remove_duplicates, sort_by_touch_count from txgraffiti.example_data import graph_data from txgraffiti import Predicate ai = ConjecturePlayground( graph_data, object_symbol='G', base='connected', ) # Define custom predicate: G is cubic regular = Predicate('regular', lambda df: df['min_degree'] == df['max_degree']) cubic = regular & (ai.max_degree == 3) # Run discovery using three methods ai.discover( methods = [ratios, convex_hull, linear_programming], features = [ai.independence_number], target = ai.zero_forcing_number, heuristics = [dalmatian_accept, morgan_accept], hypothesis = [cubic], post_processors = [remove_duplicates, sort_by_touch_count], ) # Print resulting inequalities for idx, conj in enumerate(ai.conjectures[:3], start=1): print(f"Conjecture {idx}: {ai.forall(conj)}") ``` ```text Conjecture 1: ∀ G: ((connected) ∧ (regular) ∧ (max_degree == 3)) → (zero_forcing_number >= 3) Conjecture 2: ∀ G: ((connected) ∧ (regular) ∧ (max_degree == 3)) → (zero_forcing_number >= (-2 + independence_number)) Conjecture 3: ∀ G: ((connected) ∧ (regular) ∧ (max_degree == 3)) → (zero_forcing_number >= ((2 * independence_number) + -8)) ``` -------------------------------- ### KnowledgeTable class with auto_wrap, __getattr__, and to_session Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/logic/tables.html Defines the KnowledgeTable class, a pandas DataFrame subclass that lifts columns into TxGraffiti Property or Predicate objects. Includes the auto_wrap helper function, the _constructor property, __getattr__ for column access, and the to_session method. The docstring contains doctest examples showing numeric and boolean column lifting and session creation. ```python import pandas as pd from pandas.api.types import is_bool_dtype, is_numeric_dtype from txgraffiti.logic.properties import Property from txgraffiti.logic.predicates import Predicate, TRUE __all__ = [ 'KnowledgeTable', ] def auto_wrap(df: pd.DataFrame): numeric_props = [] bool_preds = [] for col in df.columns: if col in ["name", 'Unnamed: 0']: continue series = df[col] if is_bool_dtype(series): bool_preds.append(Predicate(col, lambda df, c=col: df[c])) elif is_numeric_dtype(series): numeric_props.append(Property(col, lambda df, c=col: df[c])) return numeric_props, bool_preds [docs] class KnowledgeTable(pd.DataFrame): """ A pandas DataFrame subclass that “lifts” its columns into TxGraffiti Properties and Predicates, preserving the subclass through most DataFrame operations. Parameters ---------- *args, **kwargs Passed through to `pandas.DataFrame`. See `pandas.DataFrame` for supported parameters. Attributes ---------- : Property or Predicate If a column is boolean, `kt.` returns a `txgraffiti.logic.predicates.Predicate` that masks the DataFrame on that column. Otherwise it returns a `txgraffiti.logic.properties.Property` on that column. Methods ------- to_session(object_symbol="G", base=TRUE) Create a `ConjecturePlayground` for this table. Notes ----- - We implement the pandas `_constructor` hook so that methods like `df.loc[...]`, `.assign()`, etc., return a `KnowledgeTable` again. - Only existing column names are intercepted in `__getattr__`; all other attributes fall back to the normal DataFrame API. Examples -------- >>> import pandas as pd >>> from txgraffiti.logic.tables import KnowledgeTable >>> df = pd.DataFrame({ ... 'alpha': [1, 2, 3], ... 'connected': [True, False, True], ... }) >>> kt = KnowledgeTable(df) >>> # Numeric column lifts to Property: >>> prop = kt.alpha >>> print(prop(df)) 0 1 1 2 2 3 Name: alpha, dtype: int64 >>> # Boolean column lifts to Predicate: >>> pred = kt.connected >>> print(pred(df)) 0 True 1 False 2 True Name: connected, dtype: bool >>> # Start a conjecturing session: >>> session = kt.to_session(object_symbol="G", base=kt.connected) >>> session # doctest: +ELLIPSIS """ # Tell pandas to preserve our subclass in most operations _metadata = [] @property def _constructor(self): return KnowledgeTable def __getattr__(self, name): """ Lift a column into a Property or Predicate on attribute access. Parameters ---------- name : str The attribute name being accessed. Returns ------- Predicate or Property - If ``name`` matches a boolean column, returns ``Predicate(name, lambda df: df[name])``. - If ``name`` matches a non-boolean column, returns ``Property(name, lambda df: df[name])``. """ if name in self.columns: series = self[name] if pd.api.types.is_bool_dtype(series): return Predicate(name, lambda df, c=name: df[c]) return Property(name, lambda df, c=name: df[c]) return super().__getattr__(name) [docs] def to_session(self, object_symbol="G", base: Predicate = TRUE): """ Create a ConjecturePlayground session from this table. Parameters ---------- object_symbol : str, optional The symbol to use for the “object” in generated conjectures (default is ``"G"``). base : Predicate, optional A base hypothesis to conjoin with any user‐provided hypothesis (default is ``TRUE``, i.e. no restriction). Returns ------- ConjecturePlayground An instance of :class:`txgraffiti.playground.conjecture.ConjecturePlayground` initialized with this table. """ from txgraffiti.playground.conjecture import ConjecturePlayground return ConjecturePlayground(self, object_symbol=object_symbol, base=base) [docs] def auto_wrap(self): self.numeric_properties = [] self.bool_predicates = [] ``` -------------------------------- ### Define and combine Predicates Source: https://txgraffiti2.readthedocs.io/en/latest/api/txgraffiti.logic.html Demonstrates creating symbolic predicates using lambda functions and combining them with logical operators like AND (&). ```python from txgraffiti.logic import Predicate >>> even = Predicate(“even”, lambda df: df[“n”] % 2 == 0) >>> gt_5 = Predicate(“>5”, lambda df: df[“n”] > 5) >>> even & gt_5 5)> ``` -------------------------------- ### sophie_accept heuristic for conjecture acceptance Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/heuristics/delavina.html Defines the sophie_accept heuristic, which accepts a new conjecture only if its cover set includes at least one row not already covered by the union of accepted conjectures' cover sets. The function returns True if new coverage exists, False otherwise. The docstring includes doctest examples demonstrating the behavior with a small DataFrame. ```python import pandas as pd from typing import List, Union from txgraffiti.logic import Conjecture, KnowledgeTable __all__ = [ 'sophie_accept', ] [docs] def sophie_accept( new_conj: Conjecture, accepted: List[Conjecture], df: Union[pd.DataFrame, KnowledgeTable], ) -> bool: """ Decide whether to accept a new conjecture based on its cover set. A conjecture’s *cover set* is the set of rows where its hypothesis holds. Under the Sophie heuristic, we accept `new_conj` only if its cover set includes at least one row *not* already covered by the union of cover sets of all `accepted` conjectures. Parameters ---------- new_conj : Conjecture The candidate conjecture whose hypothesis cover set is tested. accepted : list of Conjecture Previously accepted conjectures. Their hypothesis masks are unioned to form the existing coverage. df : pandas.DataFrame or KnowledgeTable The data on which hypotheses are evaluated. Returns ------- bool True if `new_conj` covers at least one additional row beyond the union of all `accepted` cover sets, False otherwise. Examples -------- >>> import pandas as pd >>> from txgraffiti.logic import Property, Predicate, Conjecture >>> from txgraffiti.heuristics.delavina import sophie_accept >>> df = pd.DataFrame({ ... 'alpha': [1, 2, 3, 4], ... 'connected': [True, False, True, False], ... }) >>> A = Property('alpha', lambda df: df['alpha']) >>> P = Predicate('connected', lambda df: df['connected']) >>> # conj1 covers rows 0 and 2 >>> conj1 = P >> (A <= 10) >>> # conj2 covers the same rows → no new coverage >>> conj2 = P >> (A >= 0) >>> sophie_accept(conj2, [conj1], df) False >>> # conj3 covers row 0,2, plus row 1 (connected=False so hypothesis False) >>> # so still no new coverage >>> sophie_accept(conj3:= (P | ~P) >> (A >= 0), [conj1], df) True """ # cover set of the new conjecture new_cover = new_conj.hypothesis(df) # union of old covers if accepted: old_union = pd.concat( [c.hypothesis(df) for c in accepted], axis=1 ).any(axis=1) else: old_union = pd.Series(False, index=df.index) # must add at least one row not already covered delta = new_cover & ~old_union return bool(delta.any()) ``` -------------------------------- ### Combine Constants and Properties Source: https://txgraffiti2.readthedocs.io/en/latest/_sources/key_features/logic/properties.rst.txt Demonstrates mixing constants and column-based properties in symbolic expressions. ```python # c2 and c3 from above, alpha from above bound = c2 * alpha + c3 print(bound) # print(bound(df)) # [5, 7, 9] # Using multiple properties and constants: expr2 = (alpha + beta) * c3 - c2 print(expr2) # print(expr2(df)) # [10, 4, 4] ``` -------------------------------- ### Create a constant-valued Property Source: https://txgraffiti2.readthedocs.io/en/latest/_modules/txgraffiti/logic/properties.html Demonstrates how to initialize a Constant property with a value and apply it to a pandas DataFrame to produce a series of that constant. ```python >>> import pandas as pd >>> from txgraffiti.logic import Constant >>> df = pd.DataFrame({"x": [1, 2, 3]}) >>> p = Constant(7) >>> p(df).tolist() [7, 7, 7] ``` -------------------------------- ### ConjecturePlayground.discover() Source: https://txgraffiti2.readthedocs.io/en/latest/api/txgraffiti.playground.html Runs generate() with the given parameters, caches the results, and returns the list of conjectures. ```APIDOC ## ConjecturePlayground.discover() ### Description Run generate(…) with the given parameters, cache, and return the list. ### Method discover ### Parameters - **args** - Optional - Positional arguments passed to generate(). - **kwargs** - Optional - Keyword arguments passed to generate(). ### Returns - **list[Conjecture]** - The list of discovered conjectures. ```