21571587322

Committed 01 Feb 2026 10:39PM UTC coverage: 89.835% (-4.4%) from 94.188%

Build # 21571587322

Build Type

push

github

Committed by

web-flow

Commit Message

Created python-ta-z3 package (#1290)

Adds python-ta-z3 as a dependency of python-ta[z3]

Run Details

14 of 38 new or added lines in 6 files covered. (36.84%)

3429 of 3817 relevant lines covered (89.83%)

17.42 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

17.24

/packages/python-ta-z3/src/python_ta_z3/utils.py

"""Utility functions for Z3 integration."""

from __future__ import annotations

import logging
from typing import Any


# NOTE: _debug and parse_assertions are adapted from python_ta.contracts
def _debug(msg: str) -> None:
    """Display a debugging message."""
    logging.basicConfig(format="[%(levelname)s] %(message)s", level=logging.DEBUG)
    logging.debug(msg)


def parse_assertions(obj: Any, parse_token: str = "Precondition") -> list[str]:
    """Return a list of preconditions/postconditions/representation invariants parsed from the given entity's docstring.

    Uses parse_token to determine what to look for. parse_token defaults to Precondition.

    Currently only supports two forms:

    1. A single line of the form "<parse_token>: <cond>"
    2. A group of lines starting with "<parse_token>s:", where each subsequent
       line is of the form "- <cond>". Each line is considered a separate condition.
       The lines can be separated by blank lines, but no other text.
    """
    if hasattr(obj, "doc_node") and obj.doc_node is not None:
        # Check if obj is an astroid node
        docstring = obj.doc_node.value
    else:
        docstring = getattr(obj, "__doc__") or ""
    lines = [line.strip() for line in docstring.split("\n")]
    assertion_lines = [
        i for i, line in enumerate(lines) if line.lower().startswith(parse_token.lower())
    ]

    if assertion_lines == []:
        return []

    first = assertion_lines[0]

    if lines[first].startswith(parse_token + ":"):
        return [lines[first][len(parse_token + ":") :].strip()]
    elif lines[first].startswith(parse_token + "s:"):
        assertions = []
        for line in lines[first + 1 :]:
            if line.startswith("-"):
                assertion = line[1:].strip()
                if hasattr(obj, "__qualname__"):
                    _debug(f"Adding assertion to {obj.__qualname__}: {assertion}")
                assertions.append(assertion)
            elif line != "":
                break
        return assertions
    else:
        return []

1	"""Utility functions for Z3 integration."""
2
3	from __future__ import annotations	10✔
4
5	import logging	10✔
6	from typing import Any	10✔
7
8
9	# NOTE: _debug and parse_assertions are adapted from python_ta.contracts
10	def _debug(msg: str) -> None:	10✔
11	"""Display a debugging message."""
NEW 12	logging.basicConfig(format="[%(levelname)s] %(message)s", level=logging.DEBUG)	×
NEW 13	logging.debug(msg)	×
14
15
16	def parse_assertions(obj: Any, parse_token: str = "Precondition") -> list[str]:	10✔
17	"""Return a list of preconditions/postconditions/representation invariants parsed from the given entity's docstring.
18
19	Uses parse_token to determine what to look for. parse_token defaults to Precondition.
20
21	Currently only supports two forms:
22
23	1. A single line of the form "<parse_token>: <cond>"
24	2. A group of lines starting with "<parse_token>s:", where each subsequent
25	line is of the form "- <cond>". Each line is considered a separate condition.
26	The lines can be separated by blank lines, but no other text.
27	"""
NEW 28	if hasattr(obj, "doc_node") and obj.doc_node is not None:	×
29	# Check if obj is an astroid node
NEW 30	docstring = obj.doc_node.value	×
31	else:
NEW 32	docstring = getattr(obj, "__doc__") or ""	×
NEW 33	lines = [line.strip() for line in docstring.split("\n")]	×
NEW 34	assertion_lines = [	×
35	i for i, line in enumerate(lines) if line.lower().startswith(parse_token.lower())
36	]
37
NEW 38	if assertion_lines == []:	×
NEW 39	return []	×
40
NEW 41	first = assertion_lines[0]	×
42
NEW 43	if lines[first].startswith(parse_token + ":"):	×
NEW 44	return [lines[first][len(parse_token + ":") :].strip()]	×
NEW 45	elif lines[first].startswith(parse_token + "s:"):	×
NEW 46	assertions = []	×
NEW 47	for line in lines[first + 1 :]:	×
NEW 48	if line.startswith("-"):	×
NEW 49	assertion = line[1:].strip()	×
NEW 50	if hasattr(obj, "__qualname__"):	×
NEW 51	_debug(f"Adding assertion to {obj.__qualname__}: {assertion}")	×
NEW 52	assertions.append(assertion)	×
NEW 53	elif line != "":	×
NEW 54	break	×
NEW 55	return assertions	×
56	else:
NEW 57	return []	×

pyta-uoft / pyta / 21571587322

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous