21566889325

Committed 01 Feb 2026 05:11PM UTC coverage: 27.419% (-66.8%) from 94.188%

Build # 21566889325

Build Type

Pull #1290

github

Committed by

web-flow

Commit Message

Merge 0deb64788 into c539ba7b6

Pull Request Pull Request #1290: Create python-ta-z3 package

Coverage Stats

21 of 73 new or added lines in 3 files covered. (28.77%)

68 of 248 relevant lines covered (27.42%)

5.48 hits per line

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

31.58

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

from __future__ import annotations

import astroid
from astroid import AstroidError, nodes
from astroid.transforms import TransformVisitor
from astroid.util import safe_infer
from z3 import And, simplify
from z3.z3types import Z3Exception

from .utils import parse_assertions
from .z3_parser import Z3ParseException, Z3Parser


class Z3Visitor:
    """
    The class responsible for visiting astroid nodes (currently only FunctionDef nodes),
    parsing preconditions, and converting them to z3 expressions to be appended in the
    z3_constraints attribute of the node.
    """

    def __init__(self):
        """Return a TransformVisitor that sets an environment for every node."""
        visitor = TransformVisitor()
        # Register transforms
        visitor.register_transform(nodes.FunctionDef, self.set_function_def_z3_constraints)
        self.visitor = visitor

    def set_function_def_z3_constraints(self, node: nodes.FunctionDef):
        # Parse types
        types = {}
        annotations = node.args.annotations
        arguments = node.args.args
        for ann, arg in zip(annotations, arguments):
            if ann is None:
                continue
            # TODO: what to do about subscripts ex. set[int], list[set[int]], ...
            inferred = safe_infer(ann)
            if isinstance(inferred, nodes.ClassDef):
                types[arg.name] = inferred.name
        # Parse preconditions
        preconditions = parse_assertions(node, parse_token="Precondition")
        # Get z3 constraints
        z3_constraints = []
        for pre in preconditions:
            pre = astroid.parse(pre).body[0]
            parser = Z3Parser(types)
            try:
                transformed = parser.parse(pre)
            except (AstroidError, Z3Exception, Z3ParseException):
                transformed = None
            if transformed is not None:
                z3_constraints.append(transformed)
        # Set z3 constraints
        if z3_constraints:
            node.z3_constraints = [simplify(expr) for expr in z3_constraints]
        else:
            node.z3_constraints = []

1	from __future__ import annotations	20✔
2
3	import astroid	20✔
4	from astroid import AstroidError, nodes	20✔
5	from astroid.transforms import TransformVisitor	20✔
6	from astroid.util import safe_infer	20✔
7	from z3 import And, simplify	20✔
8	from z3.z3types import Z3Exception	20✔
9
10	from .utils import parse_assertions	20✔
11	from .z3_parser import Z3ParseException, Z3Parser	20✔
12
13
14	class Z3Visitor:	20✔
15	"""
16	The class responsible for visiting astroid nodes (currently only FunctionDef nodes),
17	parsing preconditions, and converting them to z3 expressions to be appended in the
18	z3_constraints attribute of the node.
19	"""
20
21	def __init__(self):	20✔
22	"""Return a TransformVisitor that sets an environment for every node."""
NEW 23	visitor = TransformVisitor()	×
24	# Register transforms
NEW 25	visitor.register_transform(nodes.FunctionDef, self.set_function_def_z3_constraints)	×
NEW 26	self.visitor = visitor	×
27
28	def set_function_def_z3_constraints(self, node: nodes.FunctionDef):	20✔
29	# Parse types
NEW 30	types = {}	×
NEW 31	annotations = node.args.annotations	×
NEW 32	arguments = node.args.args	×
NEW 33	for ann, arg in zip(annotations, arguments):	×
NEW 34	if ann is None:	×
NEW 35	continue	×
36	# TODO: what to do about subscripts ex. set[int], list[set[int]], ...
NEW 37	inferred = safe_infer(ann)	×
NEW 38	if isinstance(inferred, nodes.ClassDef):	×
NEW 39	types[arg.name] = inferred.name	×
40	# Parse preconditions
NEW 41	preconditions = parse_assertions(node, parse_token="Precondition")	×
42	# Get z3 constraints
NEW 43	z3_constraints = []	×
NEW 44	for pre in preconditions:	×
NEW 45	pre = astroid.parse(pre).body[0]	×
NEW 46	parser = Z3Parser(types)	×
NEW 47	try:	×
NEW 48	transformed = parser.parse(pre)	×
NEW 49	except (AstroidError, Z3Exception, Z3ParseException):	×
NEW 50	transformed = None	×
NEW 51	if transformed is not None:	×
NEW 52	z3_constraints.append(transformed)	×
53	# Set z3 constraints
NEW 54	if z3_constraints:	×
NEW 55	node.z3_constraints = [simplify(expr) for expr in z3_constraints]	×
56	else:
NEW 57	node.z3_constraints = []	×

pyta-uoft / pyta / 21566889325

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