Skip to content

SmtContracts

Specializes IO contract into contracts with SMT assumptions and guarantees.

SmtIoContract

Bases: IoContract

IO Contracts with assumptions and guarantees expressed as SMT constraints.

Source code in pacti\src\pacti\contracts\smt_iocontract.py 
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
class SmtIoContract(IoContract):
    """IO Contracts with assumptions and guarantees expressed as SMT constraints."""

    def rename_variables(self, variable_mappings: List[Tuple[str, str]]) -> SmtIoContract:
        """
        Rename variables in a contract.

        Args:
            variable_mappings: Variables to be replaced.

        Returns:
            A contract with `source_var` replaced by `target_var`.
        """
        new_contract = self.copy()
        for mapping in variable_mappings:
            new_contract = new_contract.rename_variable(Var(mapping[0]), Var(mapping[1]))
        return new_contract

    def to_machine_dict(self) -> ser_contract:
        """
        Map contract into a machine-optimized dictionary.

        Returns:
            A dictionary containing the contract's information.
        """
        return self.to_dict()

    def to_dict(self) -> ser_contract:
        """
        Map contract into a user-readable dictionary.

        Returns:
            A dictionary containing the contract's information.
        """
        c_temp: ser_contract = {
            "input_vars": [str(x) for x in self.inputvars],
            "output_vars": [str(x) for x in self.outputvars],
            "assumptions": self.a.to_str_list(),
            "guarantees": self.g.to_str_list(),
        }
        return c_temp  # noqa: WPS331 c_temp only used for `return`

    @staticmethod
    def from_z3_terms(
        assumptions: List[z3.BoolRef],
        guarantees: List[z3.BoolRef],
        input_vars: List[str],
        output_vars: List[str],
        simplify: bool = True,
    ) -> SmtIoContract:
        """
        Create contract from several lists of z3 terms.

        Args:
            assumptions: contract's assumptions.
            guarantees: contract's guarantees.
            input_vars: input variables of contract.
            output_vars: output variables of contract.
            simplify: whether to simplify the guarantees with respect to the assumptions.

        Returns:
            An SMT contract built from the arguments provided.
        """
        a: List[SmtTerm] = []
        if assumptions:
            a = [SmtTerm(x) for x in assumptions]

        g: List[SmtTerm] = []
        if guarantees:
            g = [SmtTerm(x) for x in guarantees]

        return SmtIoContract(
            input_vars=[Var(x) for x in input_vars],
            output_vars=[Var(x) for x in output_vars],
            assumptions=SmtTermList(a),
            guarantees=SmtTermList(g),
            simplify=simplify,
        )

    def compose(
        self,
        other: SmtIoContract,
        vars_to_keep: Optional[List[str]] = None,
        simplify: bool = True,
    ) -> SmtIoContract:
        """Compose SMT contracts.

        Compute the composition of the two given contracts and abstract the
        result in such a way that the result is a well-defined IO contract,
        i.e., that assumptions refer only to inputs, and guarantees to both
        inputs and outputs.

        Args:
            other:
                The second contract being composed.
            vars_to_keep:
                A list of variables that should be kept as top-level outputs.
            simplify:
                Whether to simplify the result of variable elimination by refining or relaxing.

        Returns:
            The abstracted composition of the two contracts.
        """
        if vars_to_keep is None:
            vars_to_keep = []
        return super().compose(other, [Var(x) for x in vars_to_keep], simplify)

    def compose_tactics(
        self,
        other: SmtIoContract,
        vars_to_keep: Optional[List[str]] = None,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtIoContract, List[TacticStatistics]]:
        """Compose SMT contracts.

        Compute the composition of the two given contracts and abstract the
        result in such a way that the result is a well-defined IO contract,
        i.e., that assumptions refer only to inputs, and guarantees to both
        inputs and outputs.

        Args:
            other:
                The second contract being composed.
            vars_to_keep:
                A list of variables that should be kept as top-level outputs.
            simplify:
                Whether to simplify the result of variable elimination by refining or relaxing.
            tactics_order:
                The order of tactics to try for variable term elimination.

        Returns:
            The tuple of the abstracted composition of the two contracts and of the list of tactics used.
        """
        if tactics_order is None:
            tactics_order = TACTICS_ORDER

        if vars_to_keep is None:
            vars_to_keep = []
        return super().compose_tactics(other, [Var(x) for x in vars_to_keep], simplify, tactics_order)

    def quotient(  # noqa: WPS612
        self: SmtIoContract,
        other: SmtIoContract,
        additional_inputs: Optional[List[Var]] = None,
        simplify: bool = True,
    ) -> SmtIoContract:
        """Quotient SMT contracts.

        Compute the quotient of the two given contracts and abstract the
        result in such a way that the result is a well-defined IO contract,
        i.e., that assumptions refer only to inputs, and guarantees to both
        inputs and outputs.

        Args:
            other:
                The contract by which we take the quotient.
            additional_inputs:
                Additional variables that the quotient is allowed to consider as
                inputs. These variables can be either top level-inputs or
                outputs of the other argument.
            simplify:
                Whether to simplify the result of variable elimination by refining or relaxing.

        Returns:
            The abstracted quotient of the two contracts.
        """
        return super().quotient(other, additional_inputs, simplify)

    def quotient_tactics(
        self: SmtIoContract,
        other: SmtIoContract,
        additional_inputs: Optional[List[Var]] = None,
        simplify: bool = True,
        tactics_order: Optional[List[int]] = None,
    ) -> Tuple[SmtIoContract, List[TacticStatistics]]:
        """Quotient SMT contracts with support for specifying the order of tactics and measuring their use.

        Compute the quotient of the two given contracts and abstract the
        result in such a way that the result is a well-defined IO contract,
        i.e., that assumptions refer only to inputs, and guarantees to both
        inputs and outputs.

        Args:
            other:
                The contract by which we take the quotient.
            additional_inputs:
                Additional variables that the quotient is allowed to consider as
                inputs. These variables can be either top level-inputs or
                outputs of the other argument.
            simplify:
                Whether to simplify the result of variable elimination by refining or relaxing.
            tactics_order:
                The order of tactics to try for variable term elimination.

        Returns:
            The tuple of the abstracted quotient of the two contracts and of the list of tactics used.
        """
        if tactics_order is None:
            tactics_order = TACTICS_ORDER

        return super().quotient_tactics(other, additional_inputs, simplify, tactics_order)

compose(other, vars_to_keep=None, simplify=True)

Compose SMT contracts.

Compute the composition of the two given contracts and abstract the result in such a way that the result is a well-defined IO contract, i.e., that assumptions refer only to inputs, and guarantees to both inputs and outputs.

Parameters:

Name Type Description Default
other SmtIoContract

The second contract being composed.

 required
vars_to_keep Optional[List[str]]

A list of variables that should be kept as top-level outputs.

 None
simplify bool

Whether to simplify the result of variable elimination by refining or relaxing.

 True

Returns:

Type Description
SmtIoContract

The abstracted composition of the two contracts.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
def compose(
    self,
    other: SmtIoContract,
    vars_to_keep: Optional[List[str]] = None,
    simplify: bool = True,
) -> SmtIoContract:
    """Compose SMT contracts.

    Compute the composition of the two given contracts and abstract the
    result in such a way that the result is a well-defined IO contract,
    i.e., that assumptions refer only to inputs, and guarantees to both
    inputs and outputs.

    Args:
        other:
            The second contract being composed.
        vars_to_keep:
            A list of variables that should be kept as top-level outputs.
        simplify:
            Whether to simplify the result of variable elimination by refining or relaxing.

    Returns:
        The abstracted composition of the two contracts.
    """
    if vars_to_keep is None:
        vars_to_keep = []
    return super().compose(other, [Var(x) for x in vars_to_keep], simplify)

compose_tactics(other, vars_to_keep=None, simplify=True, tactics_order=None)

Compose SMT contracts.

Compute the composition of the two given contracts and abstract the result in such a way that the result is a well-defined IO contract, i.e., that assumptions refer only to inputs, and guarantees to both inputs and outputs.

Parameters:

Name Type Description Default
other SmtIoContract

The second contract being composed.

 required
vars_to_keep Optional[List[str]]

A list of variables that should be kept as top-level outputs.

 None
simplify bool

Whether to simplify the result of variable elimination by refining or relaxing.

 True
tactics_order Optional[List[int]]

The order of tactics to try for variable term elimination.

 None

Returns:

Type Description
Tuple[SmtIoContract, List[TacticStatistics]]

The tuple of the abstracted composition of the two contracts and of the list of tactics used.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
def compose_tactics(
    self,
    other: SmtIoContract,
    vars_to_keep: Optional[List[str]] = None,
    simplify: bool = True,
    tactics_order: Optional[List[int]] = None,
) -> Tuple[SmtIoContract, List[TacticStatistics]]:
    """Compose SMT contracts.

    Compute the composition of the two given contracts and abstract the
    result in such a way that the result is a well-defined IO contract,
    i.e., that assumptions refer only to inputs, and guarantees to both
    inputs and outputs.

    Args:
        other:
            The second contract being composed.
        vars_to_keep:
            A list of variables that should be kept as top-level outputs.
        simplify:
            Whether to simplify the result of variable elimination by refining or relaxing.
        tactics_order:
            The order of tactics to try for variable term elimination.

    Returns:
        The tuple of the abstracted composition of the two contracts and of the list of tactics used.
    """
    if tactics_order is None:
        tactics_order = TACTICS_ORDER

    if vars_to_keep is None:
        vars_to_keep = []
    return super().compose_tactics(other, [Var(x) for x in vars_to_keep], simplify, tactics_order)

from_z3_terms(assumptions, guarantees, input_vars, output_vars, simplify=True) staticmethod

Create contract from several lists of z3 terms.

Parameters:

Name Type Description Default
assumptions List[BoolRef]

contract's assumptions.

 required
guarantees List[BoolRef]

contract's guarantees.

 required
input_vars List[str]

input variables of contract.

 required
output_vars List[str]

output variables of contract.

 required
simplify bool

whether to simplify the guarantees with respect to the assumptions.

 True

Returns:

Type Description
SmtIoContract

An SMT contract built from the arguments provided.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
@staticmethod
def from_z3_terms(
    assumptions: List[z3.BoolRef],
    guarantees: List[z3.BoolRef],
    input_vars: List[str],
    output_vars: List[str],
    simplify: bool = True,
) -> SmtIoContract:
    """
    Create contract from several lists of z3 terms.

    Args:
        assumptions: contract's assumptions.
        guarantees: contract's guarantees.
        input_vars: input variables of contract.
        output_vars: output variables of contract.
        simplify: whether to simplify the guarantees with respect to the assumptions.

    Returns:
        An SMT contract built from the arguments provided.
    """
    a: List[SmtTerm] = []
    if assumptions:
        a = [SmtTerm(x) for x in assumptions]

    g: List[SmtTerm] = []
    if guarantees:
        g = [SmtTerm(x) for x in guarantees]

    return SmtIoContract(
        input_vars=[Var(x) for x in input_vars],
        output_vars=[Var(x) for x in output_vars],
        assumptions=SmtTermList(a),
        guarantees=SmtTermList(g),
        simplify=simplify,
    )

quotient(other, additional_inputs=None, simplify=True)

Quotient SMT contracts.

Compute the quotient of the two given contracts and abstract the result in such a way that the result is a well-defined IO contract, i.e., that assumptions refer only to inputs, and guarantees to both inputs and outputs.

Parameters:

Name Type Description Default
other SmtIoContract

The contract by which we take the quotient.

 required
additional_inputs Optional[List[Var]]

Additional variables that the quotient is allowed to consider as inputs. These variables can be either top level-inputs or outputs of the other argument.

 None
simplify bool

Whether to simplify the result of variable elimination by refining or relaxing.

 True

Returns:

Type Description
SmtIoContract

The abstracted quotient of the two contracts.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
def quotient(  # noqa: WPS612
    self: SmtIoContract,
    other: SmtIoContract,
    additional_inputs: Optional[List[Var]] = None,
    simplify: bool = True,
) -> SmtIoContract:
    """Quotient SMT contracts.

    Compute the quotient of the two given contracts and abstract the
    result in such a way that the result is a well-defined IO contract,
    i.e., that assumptions refer only to inputs, and guarantees to both
    inputs and outputs.

    Args:
        other:
            The contract by which we take the quotient.
        additional_inputs:
            Additional variables that the quotient is allowed to consider as
            inputs. These variables can be either top level-inputs or
            outputs of the other argument.
        simplify:
            Whether to simplify the result of variable elimination by refining or relaxing.

    Returns:
        The abstracted quotient of the two contracts.
    """
    return super().quotient(other, additional_inputs, simplify)

quotient_tactics(other, additional_inputs=None, simplify=True, tactics_order=None)

Quotient SMT contracts with support for specifying the order of tactics and measuring their use.

Compute the quotient of the two given contracts and abstract the result in such a way that the result is a well-defined IO contract, i.e., that assumptions refer only to inputs, and guarantees to both inputs and outputs.

Parameters:

Name Type Description Default
other SmtIoContract

The contract by which we take the quotient.

 required
additional_inputs Optional[List[Var]]

Additional variables that the quotient is allowed to consider as inputs. These variables can be either top level-inputs or outputs of the other argument.

 None
simplify bool

Whether to simplify the result of variable elimination by refining or relaxing.

 True
tactics_order Optional[List[int]]

The order of tactics to try for variable term elimination.

 None

Returns:

Type Description
Tuple[SmtIoContract, List[TacticStatistics]]

The tuple of the abstracted quotient of the two contracts and of the list of tactics used.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
def quotient_tactics(
    self: SmtIoContract,
    other: SmtIoContract,
    additional_inputs: Optional[List[Var]] = None,
    simplify: bool = True,
    tactics_order: Optional[List[int]] = None,
) -> Tuple[SmtIoContract, List[TacticStatistics]]:
    """Quotient SMT contracts with support for specifying the order of tactics and measuring their use.

    Compute the quotient of the two given contracts and abstract the
    result in such a way that the result is a well-defined IO contract,
    i.e., that assumptions refer only to inputs, and guarantees to both
    inputs and outputs.

    Args:
        other:
            The contract by which we take the quotient.
        additional_inputs:
            Additional variables that the quotient is allowed to consider as
            inputs. These variables can be either top level-inputs or
            outputs of the other argument.
        simplify:
            Whether to simplify the result of variable elimination by refining or relaxing.
        tactics_order:
            The order of tactics to try for variable term elimination.

    Returns:
        The tuple of the abstracted quotient of the two contracts and of the list of tactics used.
    """
    if tactics_order is None:
        tactics_order = TACTICS_ORDER

    return super().quotient_tactics(other, additional_inputs, simplify, tactics_order)

rename_variables(variable_mappings)

Rename variables in a contract.

Parameters:

Name Type Description Default
variable_mappings List[Tuple[str, str]]

Variables to be replaced.

 required

Returns:

Type Description
SmtIoContract

A contract with source_var replaced by target_var.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
23
24
25
26
27
28
29
30
31
32
33
34
35
36
def rename_variables(self, variable_mappings: List[Tuple[str, str]]) -> SmtIoContract:
    """
    Rename variables in a contract.

    Args:
        variable_mappings: Variables to be replaced.

    Returns:
        A contract with `source_var` replaced by `target_var`.
    """
    new_contract = self.copy()
    for mapping in variable_mappings:
        new_contract = new_contract.rename_variable(Var(mapping[0]), Var(mapping[1]))
    return new_contract

to_dict()

Map contract into a user-readable dictionary.

Returns:

Type Description
ser_contract

A dictionary containing the contract's information.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
47
48
49
50
51
52
53
54
55
56
57
58
59
60
def to_dict(self) -> ser_contract:
    """
    Map contract into a user-readable dictionary.

    Returns:
        A dictionary containing the contract's information.
    """
    c_temp: ser_contract = {
        "input_vars": [str(x) for x in self.inputvars],
        "output_vars": [str(x) for x in self.outputvars],
        "assumptions": self.a.to_str_list(),
        "guarantees": self.g.to_str_list(),
    }
    return c_temp  # noqa: WPS331 c_temp only used for `return`

to_machine_dict()

Map contract into a machine-optimized dictionary.

Returns:

Type Description
ser_contract

A dictionary containing the contract's information.
Source code in pacti\src\pacti\contracts\smt_iocontract.py 
38
39
40
41
42
43
44
45
def to_machine_dict(self) -> ser_contract:
    """
    Map contract into a machine-optimized dictionary.

    Returns:
        A dictionary containing the contract's information.
    """
    return self.to_dict()