Skip to content

QFLRA requirements

The backend for qflra requirements — quantifier-free linear real arithmetic (linear inequalities combined with boolean operators such as or and neg).

Shield Layer

shield_layer

The QFLRA Shield Layer, the main public entry point of this subpackage.

Defines :class:ShieldLayer, a differentiable PyTorch module that corrects neural network predictions so they satisfy a set of QFLRA requirements.

ShieldLayer 

ShieldLayer(num_variables: int, requirements_filepath: str, ordering_choice: str = 'given')

Bases: Module

Differentiable layer that corrects predictions so they satisfy a set of QFLRA requirements: quantifier-free linear real arithmetic, i.e. disjunctions ('or') and negations ('neg') of linear inequalities.

Like the linear ShieldLayer, the correction proceeds variable by variable following a fixed ordering, clipping each variable into the feasible region implied by its constraints given the already-corrected values of the preceding variables. The difference is that disjunctions make that feasible region a union of intervals rather than a single interval, so the per-variable correction (delegated to correct_preds) is more involved than in the purely conjunctive linear case.

Attributes:

Name Type Description
num_variables

The number of variables (prediction dimensions).
ordering

The ordering of variables used to drive the correction.
constraints

The parsed list of QFLRA :class:Constraint objects.
sets_of_constr

Mapping from each :class:Variable to its constraint set.
Example

layer = ShieldLayer(num_variables=2, requirements_filepath='constraints.txt') corrected = layer(preds) # preds is a (B, 2) tensor

Build the Shield Layer from a requirements file.

Parameters:

Name Type Description Default
num_variables int

The number of variables (prediction dimensions).

 required
requirements_filepath str

Path to the file holding the variable ordering and the QFLRA constraints.

 required
ordering_choice str

How to order variables for correction; 'given' keeps the file ordering, 'random' shuffles it.

 'given'
Source code in pishield/qflra_requirements/shield_layer.py 
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
def __init__(self, num_variables: int, requirements_filepath: str, ordering_choice: str = 'given'):
    """Build the Shield Layer from a requirements file.

    Args:
        num_variables: The number of variables (prediction dimensions).
        requirements_filepath: Path to the file holding the variable ordering and
            the QFLRA constraints.
        ordering_choice: How to order variables for correction; ``'given'`` keeps
            the file ordering, ``'random'`` shuffles it.
    """
    super().__init__()
    self.num_variables = num_variables
    # Read the variable ordering and the QFLRA constraints from the requirements file.
    ordering, constraints = parse_constraints_file(requirements_filepath)
    # Decide the order in which variables will be corrected ('given', 'random' or custom).
    self.ordering = set_ordering(ordering, ordering_choice)
    self.constraints = constraints
    # Group the constraints by the variable they bound (its "level" in the ordering).
    self.sets_of_constr = compute_sets_of_constraints(ordering, constraints, verbose=True)

Parser

parser

Parser for QFLRA requirements files.

Reads a requirements file declaring a variable ordering and a list of constraints (disjunctions and negations of linear inequalities) and builds the corresponding :class:Variable and :class:Constraint objects.

neg_postprocess_ineq 

neg_postprocess_ineq(ineq: Inequality) -> Inequality

Apply boolean negation to an inequality.

Negating a linear inequality is equivalent to negating both sides and flipping the inequality sign, e.g. neg (x1+x2-x3 >= c) becomes -x1-x2+x3 > -c.

Parameters:

Name Type Description Default
ineq Inequality

The :class:Inequality to negate.

 required

Returns:

Type Description
Inequality

A new negated :class:Inequality.
Source code in pishield/qflra_requirements/parser.py 
17
18
19
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
def neg_postprocess_ineq(ineq: Inequality) -> Inequality:
    """Apply boolean negation to an inequality.

    Negating a linear inequality is equivalent to negating both sides and flipping
    the inequality sign, e.g. ``neg (x1+x2-x3 >= c)`` becomes ``-x1-x2+x3 > -c``.

    Args:
        ineq: The :class:`Inequality` to negate.

    Returns:
        A new negated :class:`Inequality`.
    """
    # equivalent to negating the sign of the inequality and the multiplying by -1
    # e.g. neg x1+x2-x3 >=0 becomes -x1-x2+x3 > 0
    # e.g. neg x1+x2-x3 >= c becomes -x1-x2+x3 > -c
    atoms_list, ineq_sign, constant = ineq.get_ineq_attributes()

    # negate all atoms in the inequality
    neg_atoms_list = []
    for atom in atoms_list:
        variable, coefficient, positive_sign = atom.get_atom_attributes()
        neg_atom = Atom(variable, coefficient, not positive_sign)
        neg_atoms_list.append(neg_atom)

    # change the sign of the inequality
    neg_ineq_sign = '>' if ineq_sign == '>=' else '>='
    neg_ineq = Inequality(neg_atoms_list, neg_ineq_sign, -constant)
    return neg_ineq

parse_atom 

parse_atom(x)

Parse a single signed coefficient-variable term into an :class:Atom.

Parameters:

Name Type Description Default
x

The atom string, e.g. 'y1', '-2y2', '-y23' or '6y3'.

 required

Returns:

Type Description

The parsed :class:Atom, or None if the (stripped) string is empty.
Source code in pishield/qflra_requirements/parser.py 
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
def parse_atom(x):
    """Parse a single signed coefficient-variable term into an :class:`Atom`.

    Args:
        x: The atom string, e.g. ``'y1'``, ``'-2y2'``, ``'-y23'`` or ``'6y3'``.

    Returns:
        The parsed :class:`Atom`, or ``None`` if the (stripped) string is empty.
    """
    x = x.strip().replace(" ", "")
    if x == '':
        return None
    positive_sign = False if '-' in x else True

    if '-' in x or '+' in x:
        x = x[1:]

    coefficient, var_id = x.split('y')
    coefficient = float(coefficient) if coefficient != '' else 1
    var = Variable('y' + var_id)

    atom = Atom(var, coefficient, positive_sign)
    return atom

parse_inequality 

parse_inequality(inequality)

Parse a linear inequality string into an :class:Inequality.

Parameters:

Name Type Description Default
inequality

The inequality string, e.g. 'y1-2y2>0' or 'y1+y2>=0'.

 required

Returns:

Type Description

The parsed :class:Inequality.
Source code in pishield/qflra_requirements/parser.py 
 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
def parse_inequality(inequality):
    """Parse a linear inequality string into an :class:`Inequality`.

    Args:
        inequality: The inequality string, e.g. ``'y1-2y2>0'`` or ``'y1+y2>=0'``.

    Returns:
        The parsed :class:`Inequality`.
    """
    ineq_sign = None
    inequality = inequality.strip()
    for sign in ALLOWED_INEQ_SIGNS:
        if sign in inequality:
            ineq_sign = sign
            break
    body, constant = inequality.split(ineq_sign)
    constant = float(constant)

    atoms_list = []
    constructed_atom = ''
    for elem in body:
        if elem in ALLOWED_OPS:
            if constructed_atom == '':
                constructed_atom += elem
            else:
                atom = parse_atom(constructed_atom)
                if atom is not None:
                    atoms_list.append(atom)
                constructed_atom = elem
        else:
            constructed_atom += elem
    atom = parse_atom(constructed_atom)
    if atom is not None:
        atoms_list.append(atom)

    ineq = Inequality(atoms_list, ineq_sign, constant)
    return ineq

parse_constraint 

parse_constraint(constr) -> Constraint

Parse a constraint line into a :class:Constraint.

The line may contain several inequalities joined by 'or' (forming a disjunction); a clause prefixed with 'neg' is negated after parsing.

Parameters:

Name Type Description Default
constr

The constraint string, e.g. 'y1>0 or neg y2>=1'.

 required

Returns:

Type Description
Constraint

The parsed :class:Constraint.
Source code in pishield/qflra_requirements/parser.py 
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
def parse_constraint(constr) -> Constraint:
    """Parse a constraint line into a :class:`Constraint`.

    The line may contain several inequalities joined by ``'or'`` (forming a
    disjunction); a clause prefixed with ``'neg'`` is negated after parsing.

    Args:
        constr: The constraint string, e.g. ``'y1>0 or neg y2>=1'``.

    Returns:
        The parsed :class:`Constraint`.
    """
    ineqs = []
    neg_postprocess = False

    disjunct_inequalities = constr.split('or')
    for ineq in disjunct_inequalities:
        if 'neg' in ineq:
            ineq = ineq.split('neg')[-1]
            neg_postprocess = True
        ineq = parse_inequality(ineq)
        if neg_postprocess:
            ineq = neg_postprocess_ineq(ineq)
            neg_postprocess = False
        ineqs.append(ineq)

    constr = Constraint(ineqs)
    return constr

parse_constraints_file 

parse_constraints_file(file: str) -> (List[Variable], List[Constraint])

Parse a requirements file into a variable ordering and constraints.

The file must contain a line starting with 'ordering' listing the variables, plus one constraint per remaining line.

Parameters:

Name Type Description Default
file str

Path to the requirements file.

 required

Returns:

Type Description
(List[Variable], List[Constraint])

A tuple (ordering, constraints) of the list of :class:Variable objects
(List[Variable], List[Constraint])

and the list of parsed :class:Constraint objects.

Raises:

Type Description
Exception

If no ordering line is found in the file.
Source code in pishield/qflra_requirements/parser.py 
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
def parse_constraints_file(file: str) -> (List[Variable], List[Constraint]):
    """Parse a requirements file into a variable ordering and constraints.

    The file must contain a line starting with ``'ordering'`` listing the variables,
    plus one constraint per remaining line.

    Args:
        file: Path to the requirements file.

    Returns:
        A tuple ``(ordering, constraints)`` of the list of :class:`Variable` objects
        and the list of parsed :class:`Constraint` objects.

    Raises:
        Exception: If no ordering line is found in the file.
    """
    f = open(file, 'r')
    constraints = []
    ordering = []
    for line in f:
        line = line.strip()
        if 'ordering' in line:
            str_ordering = line.split('ordering ')[-1].split()
            for elem in str_ordering:
                ordering.append(Variable(elem.replace(" ", ""))) # remove all whitespace from variable string
            continue
        constraints.append(parse_constraint(line))
    if len(ordering) == 0:
        raise Exception('An ordering of the variables must be provided!')
    return ordering, constraints

main 

main()

Run a small demo: parse a constraints file and print the constraints.

Source code in pishield/qflra_requirements/parser.py 
173
174
175
176
177
178
179
180
181
182
183
184
def main():
    """Run a small demo: parse a constraints file and print the constraints."""
    ordering, constraints = parse_constraints_file('../data/constraints.txt')
    for constr in constraints:
        print(constr.readable())
        # for elem in constr.inequality_list[0].body:
        #     print('id', elem.get_variable_id())

    print('verbose constr')
    for constr in constraints:
        print(constr.verbose_readable())
    print('ordering', ordering)

Classes

classes

Core data structures for QFLRA requirements.

Defines variables, linear inequality atoms, inequalities, disjunctions of inequalities and constraints, together with methods to inspect, render and evaluate them on batched predictions.

Variable 

Variable(variable: str)

A variable (label or feature) identified by a string name.

Attributes:

Name Type Description
variable

The string name of the variable, e.g. 'y_3'.
id

The integer id parsed from the trailing part of the name.

Initialise the variable from its string name.

Parameters:

Name Type Description Default
variable str

The variable name, whose trailing integer (after the last '_') becomes its id.

 required
Source code in pishield/qflra_requirements/classes.py 
22
23
24
25
26
27
28
29
30
31
def __init__(self, variable: str):
    """Initialise the variable from its string name.

    Args:
        variable: The variable name, whose trailing integer (after the last
            ``'_'``) becomes its id.
    """
    super().__init__()
    self.variable = variable
    self.id = self.get_variable_id()

readable 

readable()

Return the human-readable name of the variable.

Returns:

Type Description

The variable's string name.
Source code in pishield/qflra_requirements/classes.py 
33
34
35
36
37
38
39
def readable(self):
    """Return the human-readable name of the variable.

    Returns:
        The variable's string name.
    """
    return self.variable

get_variable_id 

get_variable_id()

Parse the integer id from the variable name.

Returns:

Type Description

The integer following the last '_' in the variable name.
Source code in pishield/qflra_requirements/classes.py 
41
42
43
44
45
46
47
48
def get_variable_id(self):
    """Parse the integer id from the variable name.

    Returns:
        The integer following the last ``'_'`` in the variable name.
    """
    id = int(self.variable.split('_')[-1])
    return id

Atom 

Atom(variable: Variable, coefficient: float, positive_sign: bool)

A signed linear term (coefficient times a variable) in an inequality body.

Attributes:

Name Type Description
variable

The :class:Variable this atom refers to.
coefficient

The absolute value of the coefficient.
positive_sign

Whether the term is added (True) or subtracted (False).

Initialise the atom.

Parameters:

Name Type Description Default
variable Variable

The :class:Variable of this atom.

 required
coefficient float

The coefficient; its absolute value is stored.

 required
positive_sign bool

True if the term is positive, False if negative.

 required
Source code in pishield/qflra_requirements/classes.py 
60
61
62
63
64
65
66
67
68
69
70
71
def __init__(self, variable: Variable, coefficient: float, positive_sign: bool):
    """Initialise the atom.

    Args:
        variable: The :class:`Variable` of this atom.
        coefficient: The coefficient; its absolute value is stored.
        positive_sign: ``True`` if the term is positive, ``False`` if negative.
    """
    super().__init__()
    self.variable = variable
    self.coefficient = abs(coefficient)
    self.positive_sign = positive_sign

get_variable_id 

get_variable_id()

Return the id of this atom's variable.

Returns:

Type Description

The integer id of the underlying :class:Variable.
Source code in pishield/qflra_requirements/classes.py 
73
74
75
76
77
78
79
def get_variable_id(self):
    """Return the id of this atom's variable.

    Returns:
        The integer id of the underlying :class:`Variable`.
    """
    return self.variable.get_variable_id()

eval 

eval(x_value)

Evaluate the atom at a given variable value.

Parameters:

Name Type Description Default
x_value

The value (possibly batched tensor) of the variable.

 required

Returns:

Type Description

x_value multiplied by the signed coefficient.
Source code in pishield/qflra_requirements/classes.py 
81
82
83
84
85
86
87
88
89
90
def eval(self, x_value):
    """Evaluate the atom at a given variable value.

    Args:
        x_value: The value (possibly batched tensor) of the variable.

    Returns:
        ``x_value`` multiplied by the signed coefficient.
    """
    return x_value * self.get_signed_coefficient()

get_signed_coefficient 

get_signed_coefficient()

Return the coefficient with its sign applied.

Returns:

Type Description

+coefficient if the atom is positive, -coefficient otherwise.
Source code in pishield/qflra_requirements/classes.py 
92
93
94
95
96
97
98
def get_signed_coefficient(self):
    """Return the coefficient with its sign applied.

    Returns:
        ``+coefficient`` if the atom is positive, ``-coefficient`` otherwise.
    """
    return self.coefficient if self.positive_sign else -1 * self.coefficient

readable 

readable()

Return a human-readable string for the atom, e.g. ' + 2y_3'.

Returns:

Type Description

The signed, formatted term as a string.
Source code in pishield/qflra_requirements/classes.py 
100
101
102
103
104
105
106
107
108
109
110
def readable(self):
    """Return a human-readable string for the atom, e.g. ``' + 2y_3'``.

    Returns:
        The signed, formatted term as a string.
    """
    readable = ' + ' if self.positive_sign else ' - '
    readable += (f'{self.coefficient:.2f}' if self.coefficient != int(
        self.coefficient) else f'{self.coefficient:.0f}') if self.coefficient != 1 else ''
    readable += self.variable.readable()
    return readable

get_atom_attributes 

get_atom_attributes()

Return the atom's defining attributes.

Returns:

Type Description

A tuple (variable, coefficient, positive_sign).
Source code in pishield/qflra_requirements/classes.py 
112
113
114
115
116
117
118
def get_atom_attributes(self):
    """Return the atom's defining attributes.

    Returns:
        A tuple ``(variable, coefficient, positive_sign)``.
    """
    return self.variable, self.coefficient, self.positive_sign

Inequality 

Inequality(body: List[Atom], ineq_sign: str, constant: float)

A single linear inequality body <sign> constant.

Attributes:

Name Type Description
ineq_sign

The inequality sign, either '>' or '>='.
constant

The right-hand side constant.
body

List of :class:Atom objects forming the left-hand side.

Initialise the inequality.

Parameters:

Name Type Description Default
body List[Atom]

List of :class:Atom objects forming the left-hand side.

 required
ineq_sign str

Either '>' or '>='.

 required
constant float

The right-hand side constant.

 required

Raises:

Type Description
AssertionError

If ineq_sign is not '>' or '>='.
Source code in pishield/qflra_requirements/classes.py 
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
def __init__(self, body: List[Atom], ineq_sign: str, constant: float):
    """Initialise the inequality.

    Args:
        body: List of :class:`Atom` objects forming the left-hand side.
        ineq_sign: Either ``'>'`` or ``'>='``.
        constant: The right-hand side constant.

    Raises:
        AssertionError: If ``ineq_sign`` is not ``'>'`` or ``'>='``.
    """
    super().__init__()
    assert ineq_sign in ['>', '>=']
    self.ineq_sign = ineq_sign
    self.constant = constant
    self.body = body

readable 

readable()

Return a human-readable string for the inequality.

Returns:

Type Description

The rendered inequality, e.g. ' + y_1 - 2y_2 > 0'.
Source code in pishield/qflra_requirements/classes.py 
146
147
148
149
150
151
152
153
154
155
156
def readable(self):
    """Return a human-readable string for the inequality.

    Returns:
        The rendered inequality, e.g. ``' + y_1 - 2y_2 > 0'``.
    """
    readable_ineq = ''
    for elem in self.body:
        readable_ineq += elem.readable()
    readable_ineq += ' ' + self.ineq_sign + ' ' + str(self.constant)
    return readable_ineq

get_body_variables 

get_body_variables()

Return the variables appearing in the inequality body.

Returns:

Type Description

A list of :class:Variable objects, one per body atom.
Source code in pishield/qflra_requirements/classes.py 
158
159
160
161
162
163
164
165
166
167
def get_body_variables(self):
    """Return the variables appearing in the inequality body.

    Returns:
        A list of :class:`Variable` objects, one per body atom.
    """
    var_list = []
    for atom in self.body:
        var_list.append(atom.variable)
    return var_list

get_body_atoms 

get_body_atoms()

Return the atoms of the inequality body.

Returns:

Type Description

A list of the body :class:Atom objects.
Source code in pishield/qflra_requirements/classes.py 
169
170
171
172
173
174
175
176
177
178
def get_body_atoms(self):
    """Return the atoms of the inequality body.

    Returns:
        A list of the body :class:`Atom` objects.
    """
    atom_list = []
    for atom in self.body:
        atom_list.append(atom)
    return atom_list

get_x_complement_body_atoms 

get_x_complement_body_atoms(x: Variable) -> (List[Atom], Atom, bool)

Split the body into the atom of x and the remaining atoms.

Parameters:

Name Type Description Default
x Variable

The variable to isolate.

 required

Returns:

Type Description
(List[Atom], Atom, bool)

A tuple (complementary_atom_list, x_atom, constant, is_strict) where
(List[Atom], Atom, bool)

complementary_atom_list are the body atoms other than x,
(List[Atom], Atom, bool)

x_atom is the single atom of x (or an empty list if absent),
(List[Atom], Atom, bool)

constant is the inequality constant, and is_strict is True
(List[Atom], Atom, bool)

for a '>' inequality.

Raises:

Type Description
AssertionError

If x appears more than once in the body.
Source code in pishield/qflra_requirements/classes.py 
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
def get_x_complement_body_atoms(self, x: Variable) -> (List[Atom], Atom, bool):
    """Split the body into the atom of ``x`` and the remaining atoms.

    Args:
        x: The variable to isolate.

    Returns:
        A tuple ``(complementary_atom_list, x_atom, constant, is_strict)`` where
        ``complementary_atom_list`` are the body atoms other than ``x``,
        ``x_atom`` is the single atom of ``x`` (or an empty list if absent),
        ``constant`` is the inequality constant, and ``is_strict`` is ``True``
        for a ``'>'`` inequality.

    Raises:
        AssertionError: If ``x`` appears more than once in the body.
    """
    # given a constraint constr in which variable x appears,
    # return the body of the constraint (i.e. the left-hand side of the inequality)
    # from which x occurrences have been removed
    complementary_atom_list = []
    x_atom_occurrences = []
    for atom in self.body:
        if atom.variable.id != x.id:
            complementary_atom_list.append(atom)
        else:
            x_atom_occurrences.append(atom)
    assert len(x_atom_occurrences) <= 1, "variable {x.id} appears more than one time, function collapse_atoms() from compute_sets_of_constraints should be applied"
    if len(x_atom_occurrences) == 1:
        x_atom_occurrences = x_atom_occurrences[0]
    is_strict_inequality = True if self.ineq_sign == '>' else False
    return complementary_atom_list, x_atom_occurrences, self.constant, is_strict_inequality

get_ineq_attributes 

get_ineq_attributes()

Return the inequality's defining attributes.

Returns:

Type Description

A tuple (body, ineq_sign, constant).
Source code in pishield/qflra_requirements/classes.py 
212
213
214
215
216
217
218
def get_ineq_attributes(self):
    """Return the inequality's defining attributes.

    Returns:
        A tuple ``(body, ineq_sign, constant)``.
    """
    return self.body, self.ineq_sign, self.constant

contains_variable 

contains_variable(x: Variable)

Report whether the variable appears anywhere in the body.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x occurs in the body, False otherwise.
Source code in pishield/qflra_requirements/classes.py 
220
221
222
223
224
225
226
227
228
229
230
def contains_variable(self, x: Variable):
    """Report whether the variable appears anywhere in the body.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` occurs in the body, ``False`` otherwise.
    """
    body_variables = [elem.id for elem in self.get_body_variables()]
    return x.id in body_variables

contains_variable_only_positively 

contains_variable_only_positively(x: Variable)

Report whether the variable appears with a positive sign.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if a positive-sign atom of x is present.
Source code in pishield/qflra_requirements/classes.py 
232
233
234
235
236
237
238
239
240
241
242
def contains_variable_only_positively(self, x: Variable):
    """Report whether the variable appears with a positive sign.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if a positive-sign atom of ``x`` is present.
    """
    body_variables_ids = [elem.variable.id for elem in self.get_body_atoms() if elem.positive_sign]
    return x.id in body_variables_ids

contains_variable_only_negatively 

contains_variable_only_negatively(x: Variable)

Report whether the variable appears with a negative sign.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if a negative-sign atom of x is present.
Source code in pishield/qflra_requirements/classes.py 
244
245
246
247
248
249
250
251
252
253
254
def contains_variable_only_negatively(self, x: Variable):
    """Report whether the variable appears with a negative sign.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if a negative-sign atom of ``x`` is present.
    """
    body_variables_ids = [elem.variable.id for elem in self.get_body_atoms() if not elem.positive_sign]
    return x.id in body_variables_ids

contains_variable_both_positively_and_negatively 

contains_variable_both_positively_and_negatively(x: Variable)

Report mixed-sign occurrence of a variable.

A single inequality never contains a variable both positively and negatively; this is only possible for a disjunctive inequality.

Parameters:

Name Type Description Default
x Variable

The variable to look for (unused).

 required

Returns:

Type Description

Always False.
Source code in pishield/qflra_requirements/classes.py 
256
257
258
259
260
261
262
263
264
265
266
267
268
269
def contains_variable_both_positively_and_negatively(self, x: Variable):
    """Report mixed-sign occurrence of a variable.

    A single inequality never contains a variable both positively and
    negatively; this is only possible for a disjunctive inequality.

    Args:
        x: The variable to look for (unused).

    Returns:
        Always ``False``.
    """
    # this can only happen for a disjunctive inequality
    return False

get_ineq_with_pos_and_neg_var_y_and_complement 

get_ineq_with_pos_and_neg_var_y_and_complement(x: Variable)

Return positive/negative clauses of a variable (disjunction-only).

Only meaningful for a disjunctive inequality; a single inequality has no such split.

Parameters:

Name Type Description Default
x Variable

The variable to look for (unused).

 required

Returns:

Type Description

Always None.
Source code in pishield/qflra_requirements/classes.py 
271
272
273
274
275
276
277
278
279
280
281
282
283
284
def get_ineq_with_pos_and_neg_var_y_and_complement(self, x: Variable):
    """Return positive/negative clauses of a variable (disjunction-only).

    Only meaningful for a disjunctive inequality; a single inequality has no such
    split.

    Args:
        x: The variable to look for (unused).

    Returns:
        Always ``None``.
    """
    # this can only happen for a disjunctive inequality: i.e. one clause with pos x, another clause with neg x
    return None

get_ineq_with_var_y_and_complement 

get_ineq_with_var_y_and_complement(x: Variable)

Return this inequality if it contains the variable, else None.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

(self, []) if x occurs in the body (the complement is empty for a

single inequality), otherwise None.
Source code in pishield/qflra_requirements/classes.py 
286
287
288
289
290
291
292
293
294
295
296
297
298
def get_ineq_with_var_y_and_complement(self, x: Variable):
    """Return this inequality if it contains the variable, else ``None``.

    Args:
        x: The variable to look for.

    Returns:
        ``(self, [])`` if ``x`` occurs in the body (the complement is empty for a
        single inequality), otherwise ``None``.
    """
    if self.contains_variable(x):
        return self, []
    return None

check_satisfaction 

check_satisfaction(preds: Tensor) -> torch.Tensor

Evaluate satisfaction of the inequality on batched predictions.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description
Tensor

A boolean tensor of shape (B,) that is True for samples
Tensor

satisfying the inequality (within TOLERANCE).

Raises:

Type Description
NotImplementedError

If the inequality sign is unsupported.
Source code in pishield/qflra_requirements/classes.py 
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
def check_satisfaction(self, preds: torch.Tensor) -> torch.Tensor:
    """Evaluate satisfaction of the inequality on batched predictions.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        A boolean tensor of shape ``(B,)`` that is ``True`` for samples
        satisfying the inequality (within ``TOLERANCE``).

    Raises:
        NotImplementedError: If the inequality sign is unsupported.
    """
    eval_body_value = eval_atoms_list(self.body, preds)
    # note that preds might be batched
    # in general, if preds is of shape BxD, then the result will be of shape Bx1
    eval_body_value = eval_atoms_list(self.body, preds)
    if self.ineq_sign == '>':
        results = eval_body_value > self.constant - TOLERANCE
    elif self.ineq_sign == '>=':
        results = eval_body_value >= self.constant - TOLERANCE
    else:
        raise NotImplementedError
    return results

check_satisfaction_all 

check_satisfaction_all(preds: Tensor) -> bool

Report whether all samples satisfy the inequality.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description
bool

True if every sample satisfies the inequality.
Source code in pishield/qflra_requirements/classes.py 
325
326
327
328
329
330
331
332
333
334
def check_satisfaction_all(self, preds: torch.Tensor) -> bool:
    """Report whether all samples satisfy the inequality.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        ``True`` if every sample satisfies the inequality.
    """
    return self.check_satisfaction(preds).all()

eval_to_bool 

eval_to_bool(preds: Tensor) -> bool

Reduce per-sample satisfaction to a single boolean.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description
bool

True if every sample satisfies the inequality.
Source code in pishield/qflra_requirements/classes.py 
336
337
338
339
340
341
342
343
344
345
346
347
def eval_to_bool(self, preds: torch.Tensor) -> bool:
    """Reduce per-sample satisfaction to a single boolean.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        ``True`` if every sample satisfies the inequality.
    """
    sat_per_datapoint = self.check_satisfaction(preds)
    bool_eval_result = sat_per_datapoint.all()
    return bool_eval_result

DisjunctInequality 

DisjunctInequality(inequality_list: List[Inequality])

A disjunction ('or') of linear inequalities.

Attributes:

Name Type Description
list_inequalities

The :class:Inequality clauses; the disjunction is satisfied when at least one clause holds.

Initialise the disjunction.

Parameters:

Name Type Description Default
inequality_list List[Inequality]

The list of :class:Inequality clauses.

 required
Source code in pishield/qflra_requirements/classes.py 
366
367
368
369
370
371
372
def __init__(self, inequality_list: List[Inequality]):
    """Initialise the disjunction.

    Args:
        inequality_list: The list of :class:`Inequality` clauses.
    """
    self.list_inequalities = inequality_list

readable 

readable()

Return a multi-line human-readable string listing each disjunct.

Returns:

Type Description

A string with one disjunct i: line per clause.
Source code in pishield/qflra_requirements/classes.py 
374
375
376
377
378
379
380
381
382
383
def readable(self):
    """Return a multi-line human-readable string listing each disjunct.

    Returns:
        A string with one ``disjunct i:`` line per clause.
    """
    readable_ineq = ''
    for i,ineq in enumerate(self.list_inequalities):
        readable_ineq += f'disjunct {i}: {ineq.readable()}\n'
    return readable_ineq

verbose_readable 

verbose_readable()

Return a single-line human-readable string joining clauses with 'or'.

Returns:

Type Description

The clauses rendered and joined by ' or'.
Source code in pishield/qflra_requirements/classes.py 
385
386
387
388
389
390
391
392
393
394
def verbose_readable(self):
    """Return a single-line human-readable string joining clauses with 'or'.

    Returns:
        The clauses rendered and joined by ``' or'``.
    """
    readable_constr = self.list_inequalities[0].readable()
    for ineq in self.list_inequalities[1:]:
        readable_constr += ' or' + ineq.readable()
    return readable_constr

contains_variable 

contains_variable(x: Variable)

Report whether the variable appears in any clause.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x occurs in at least one clause.
Source code in pishield/qflra_requirements/classes.py 
396
397
398
399
400
401
402
403
404
405
406
407
408
def contains_variable(self, x: Variable):
    """Report whether the variable appears in any clause.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` occurs in at least one clause.
    """
    for ineq in self.list_inequalities:
        if ineq.contains_variable(x):
            return True
    return False

contains_variable_only_positively 

contains_variable_only_positively(x: Variable)

Report whether the variable occurs only positively across clauses.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears positively in some clause and never negatively.
Source code in pishield/qflra_requirements/classes.py 
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
def contains_variable_only_positively(self, x: Variable):
    """Report whether the variable occurs only positively across clauses.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears positively in some clause and never negatively.
    """
    pos_occurrence = False
    neg_occurrence = False
    for ineq in self.list_inequalities:
        if ineq.contains_variable_only_positively(x):
            pos_occurrence = True
        if ineq.contains_variable_only_negatively(x):
            neg_occurrence = True

    if pos_occurrence and not neg_occurrence:
        return True
    else:
        return False

contains_variable_only_negatively 

contains_variable_only_negatively(x: Variable)

Report whether the variable occurs only negatively across clauses.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears negatively in some clause and never positively.
Source code in pishield/qflra_requirements/classes.py 
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
def contains_variable_only_negatively(self, x: Variable):
    """Report whether the variable occurs only negatively across clauses.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears negatively in some clause and never positively.
    """
    pos_occurrence = False
    neg_occurrence = False
    for ineq in self.list_inequalities:
        if ineq.contains_variable_only_positively(x):
            pos_occurrence = True
        if ineq.contains_variable_only_negatively(x):
            neg_occurrence = True

    if neg_occurrence and not pos_occurrence:
        return True
    else:
        return False

contains_variable_both_positively_and_negatively 

contains_variable_both_positively_and_negatively(x: Variable)

Report whether the variable occurs both positively and negatively.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears positively in some clause and negatively in

another.
Source code in pishield/qflra_requirements/classes.py 
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
def contains_variable_both_positively_and_negatively(self, x: Variable):
    """Report whether the variable occurs both positively and negatively.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears positively in some clause and negatively in
        another.
    """
    pos_occurrence = False
    neg_occurrence = False
    for ineq in self.list_inequalities:
        if ineq.contains_variable_only_positively(x):
            pos_occurrence = True
        if ineq.contains_variable_only_negatively(x):
            neg_occurrence = True

    if neg_occurrence and pos_occurrence:
        return True
    else:
        return False

get_ineq_with_var_y_and_complement 

get_ineq_with_var_y_and_complement(x: Variable)

Find the clause containing a variable and the remaining clauses.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

A tuple (ineq_with_y, complement) where ineq_with_y is the clause

containing x and complement are the other clauses, or None if

no clause contains x.
Source code in pishield/qflra_requirements/classes.py 
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
def get_ineq_with_var_y_and_complement(self, x: Variable):
    """Find the clause containing a variable and the remaining clauses.

    Args:
        x: The variable to look for.

    Returns:
        A tuple ``(ineq_with_y, complement)`` where ``ineq_with_y`` is the clause
        containing ``x`` and ``complement`` are the other clauses, or ``None`` if
        no clause contains ``x``.
    """
    complement = []
    ineq_with_y = None
    for ineq in self.list_inequalities:
        if ineq.contains_variable(x):
            ineq_with_y = ineq
        else:
            complement.append(ineq)
    if ineq_with_y is None:
        return None
    else:
        return ineq_with_y, complement

get_ineq_with_pos_and_neg_var_y_and_complement 

get_ineq_with_pos_and_neg_var_y_and_complement(x: Variable)

Find the positive-x and negative-x clauses and the remaining clauses.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

A tuple (ineq_with_pos_y, ineq_with_neg_y, complement): the clause

where x appears positively, the clause where it appears negatively,

and the other clauses.

Raises:

Type Description
NotImplementedError

If either a positive-x or negative-x clause is missing.
Source code in pishield/qflra_requirements/classes.py 
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
def get_ineq_with_pos_and_neg_var_y_and_complement(self, x: Variable):
    """Find the positive-x and negative-x clauses and the remaining clauses.

    Args:
        x: The variable to look for.

    Returns:
        A tuple ``(ineq_with_pos_y, ineq_with_neg_y, complement)``: the clause
        where ``x`` appears positively, the clause where it appears negatively,
        and the other clauses.

    Raises:
        NotImplementedError: If either a positive-x or negative-x clause is
            missing.
    """
    complement = []
    ineq_with_pos_y = None
    ineq_with_neg_y = None

    for ineq in self.list_inequalities:
        if ineq.contains_variable(x):
            if ineq.contains_variable_only_positively(x):
                ineq_with_pos_y = ineq
            elif ineq.contains_variable_only_negatively(x):
                ineq_with_neg_y = ineq
        else:
            complement.append(ineq)
    if ineq_with_pos_y is None or ineq_with_neg_y is None:
        raise NotImplementedError
    else:
        return ineq_with_pos_y, ineq_with_neg_y, complement

get_body_variables 

get_body_variables()

Return the variables across all clause bodies.

Returns:

Type Description

A list of :class:Variable objects gathered from every clause body.
Source code in pishield/qflra_requirements/classes.py 
532
533
534
535
536
537
538
539
540
541
542
def get_body_variables(self):
    """Return the variables across all clause bodies.

    Returns:
        A list of :class:`Variable` objects gathered from every clause body.
    """
    var_list = []
    for body_elem in self.body:
        for atom in body_elem:
            var_list.append(atom.variable)
    return var_list

get_body_atoms 

get_body_atoms()

Return the atoms across all clause bodies.

Returns:

Type Description

A flat list of :class:Atom objects from every clause body.
Source code in pishield/qflra_requirements/classes.py 
544
545
546
547
548
549
550
551
552
553
554
def get_body_atoms(self):
    """Return the atoms across all clause bodies.

    Returns:
        A flat list of :class:`Atom` objects from every clause body.
    """
    atom_list = []
    for body_elem in self.body:
        for atom in body_elem:
            atom_list.append(atom)
    return atom_list

split_ineqs_with_and_without_x 

split_ineqs_with_and_without_x(x: Variable) -> (List[Inequality], List[Inequality])

Partition the clauses by whether they contain a variable.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description
(List[Inequality], List[Inequality])

A tuple (ineqs_with_x, ineqs_without_x) of clause lists.
Source code in pishield/qflra_requirements/classes.py 
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
def split_ineqs_with_and_without_x(self, x: Variable) -> (List[Inequality], List[Inequality]):
    """Partition the clauses by whether they contain a variable.

    Args:
        x: The variable to look for.

    Returns:
        A tuple ``(ineqs_with_x, ineqs_without_x)`` of clause lists.
    """
    # separate ineqs that contain x from those that do not contain x
    ineqs_with_x = []
    ineqs_without_x = []
    for ineq in self.list_inequalities:
        if ineq.contains_variable(x):
            ineqs_with_x.append(ineq)
        else:
            ineqs_without_x.append(ineq)

    return ineqs_with_x, ineqs_without_x

get_x_complement_body_atoms 

get_x_complement_body_atoms(x: Variable, sign_of_x: str) -> (List[Atom], Atom)

Select the clause with the requested sign of a variable and split it.

Picks the clause in which x occurs with sign_of_x (handling both the mixed-sign and single-occurrence cases) and delegates to that inequality's :meth:Inequality.get_x_complement_body_atoms.

Parameters:

Name Type Description Default
x Variable

The variable to isolate.

 required
sign_of_x str

Either 'positive' or 'negative'.

 required

Returns:

Type Description
(List[Atom], Atom)

The tuple returned by :meth:Inequality.get_x_complement_body_atoms
(List[Atom], Atom)

for the selected clause.

Raises:

Type Description
NotImplementedError

If sign_of_x is neither 'positive' nor 'negative'.
Source code in pishield/qflra_requirements/classes.py 
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
def get_x_complement_body_atoms(self, x: Variable, sign_of_x: str) -> (List[Atom], Atom):
    """Select the clause with the requested sign of a variable and split it.

    Picks the clause in which ``x`` occurs with ``sign_of_x`` (handling both the
    mixed-sign and single-occurrence cases) and delegates to that inequality's
    :meth:`Inequality.get_x_complement_body_atoms`.

    Args:
        x: The variable to isolate.
        sign_of_x: Either ``'positive'`` or ``'negative'``.

    Returns:
        The tuple returned by :meth:`Inequality.get_x_complement_body_atoms`
        for the selected clause.

    Raises:
        NotImplementedError: If ``sign_of_x`` is neither ``'positive'`` nor
            ``'negative'``.
    """
    try:
        ineq_with_pos_x, ineq_with_neg_x, complement = self.get_ineq_with_pos_and_neg_var_y_and_complement(x)
    except:
        ineq_with_y, complement = self.get_ineq_with_var_y_and_complement(x)
        ineq_with_y: Inequality
        if sign_of_x == 'positive':
            ineq_with_pos_x = ineq_with_y
            assert ineq_with_pos_x.contains_variable_only_positively(x)
        elif sign_of_x == 'negative':
            ineq_with_neg_x = ineq_with_y
            assert ineq_with_neg_x.contains_variable_only_negatively(x)
        else:
            raise NotImplementedError
    selected_ineq = ineq_with_pos_x if sign_of_x == 'positive' else ineq_with_neg_x
    return selected_ineq.get_x_complement_body_atoms(x)

check_satisfaction 

check_satisfaction(preds: Tensor) -> torch.Tensor

Evaluate the disjunction on batched predictions.

A sample satisfies the disjunction if it satisfies at least one clause.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description
Tensor

A boolean tensor of shape (B,) that is True for samples
Tensor

satisfying any clause.
Source code in pishield/qflra_requirements/classes.py 
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
def check_satisfaction(self, preds: torch.Tensor) -> torch.Tensor:
    """Evaluate the disjunction on batched predictions.

    A sample satisfies the disjunction if it satisfies at least one clause.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        A boolean tensor of shape ``(B,)`` that is ``True`` for samples
        satisfying any clause.
    """
    # returns True if all preds (i.e. all samples) satisfy at least one of the clauses of this DI

    clause_sat = []
    for ineq in self.list_inequalities:
        clause_sat.append(ineq.check_satisfaction(preds).unsqueeze(1))
    # disj res: B x num_ineqs
    clause_sat = torch.cat(clause_sat, dim=1)

    # disj_results: B
    batched_sat_results = clause_sat.any(dim=1)
    # print(preds[~batched_sat_results], 'Samples that do not satisfy any of the clauses in this DI')
    return batched_sat_results

check_satisfaction_all 

check_satisfaction_all(preds: Tensor) -> bool

Report whether all samples satisfy the disjunction.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description
bool

True if every sample satisfies at least one clause.
Source code in pishield/qflra_requirements/classes.py 
636
637
638
639
640
641
642
643
644
645
def check_satisfaction_all(self, preds: torch.Tensor) -> bool:
    """Report whether all samples satisfy the disjunction.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        ``True`` if every sample satisfies at least one clause.
    """
    return self.check_satisfaction(preds).all()

Constraint 

Constraint(inequality_list: List[Inequality])

A single QFLRA requirement: one inequality or a disjunction of them.

Most methods delegate to the underlying inequality (or disjunction). When the constraint holds a single inequality, disjunctive_inequality is that :class:Inequality; otherwise it is a :class:DisjunctInequality.

Attributes:

Name Type Description
list_inequalities

The inequalities making up the constraint.
disjunctive_inequality

The :class:DisjunctInequality (if more than one inequality) or the single :class:Inequality.

Initialise the constraint from its inequalities.

Parameters:

Name Type Description Default
inequality_list List[Inequality]

The :class:Inequality objects; if more than one, they form a disjunction.

 required
Source code in pishield/qflra_requirements/classes.py 
660
661
662
663
664
665
666
667
668
669
def __init__(self, inequality_list: List[Inequality]):
    """Initialise the constraint from its inequalities.

    Args:
        inequality_list: The :class:`Inequality` objects; if more than one, they
            form a disjunction.
    """
    super().__init__()
    self.list_inequalities = inequality_list
    self.disjunctive_inequality = DisjunctInequality(inequality_list) if len(inequality_list)>1 else inequality_list[0]

readable 

readable()

Return a human-readable string for the constraint.

Returns:

Type Description

The rendered constraint.
Source code in pishield/qflra_requirements/classes.py 
671
672
673
674
675
676
677
def readable(self):
    """Return a human-readable string for the constraint.

    Returns:
        The rendered constraint.
    """
    return self.disjunctive_inequality.readable()

verbose_readable 

verbose_readable()

Return a single-line human-readable string for the constraint.

Returns:

Type Description

The constraint rendered on one line (clauses joined with 'or').
Source code in pishield/qflra_requirements/classes.py 
679
680
681
682
683
684
685
def verbose_readable(self):
    """Return a single-line human-readable string for the constraint.

    Returns:
        The constraint rendered on one line (clauses joined with 'or').
    """
    return self.disjunctive_inequality.verbose_readable()

contains_variable 

contains_variable(x: Variable)

Report whether the constraint involves a variable.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears in the constraint.
Source code in pishield/qflra_requirements/classes.py 
687
688
689
690
691
692
693
694
695
696
def contains_variable(self, x: Variable):
    """Report whether the constraint involves a variable.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears in the constraint.
    """
    return self.disjunctive_inequality.contains_variable(x)

get_body_atoms 

get_body_atoms()

Return the atoms of the constraint body.

Returns:

Type Description

A list of :class:Atom objects.
Source code in pishield/qflra_requirements/classes.py 
698
699
700
701
702
703
704
def get_body_atoms(self):
    """Return the atoms of the constraint body.

    Returns:
        A list of :class:`Atom` objects.
    """
    return self.disjunctive_inequality.get_body_atoms()

check_satisfaction 

check_satisfaction(preds)

Report whether all samples satisfy the constraint.

Parameters:

Name Type Description Default
preds

Predictions tensor of shape (B, D).

 required

Returns:

Type Description

True if every sample satisfies the constraint.
Source code in pishield/qflra_requirements/classes.py 
706
707
708
709
710
711
712
713
714
715
def check_satisfaction(self, preds):
    """Report whether all samples satisfy the constraint.

    Args:
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        ``True`` if every sample satisfies the constraint.
    """
    return self.disjunctive_inequality.check_satisfaction_all(preds)

contains_variable_only_positively 

contains_variable_only_positively(x: Variable)

Report whether the variable occurs only positively.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears only positively in the constraint.
Source code in pishield/qflra_requirements/classes.py 
717
718
719
720
721
722
723
724
725
726
def contains_variable_only_positively(self, x: Variable):
    """Report whether the variable occurs only positively.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears only positively in the constraint.
    """
    return self.disjunctive_inequality.contains_variable_only_positively(x)

contains_variable_only_negatively 

contains_variable_only_negatively(x: Variable)

Report whether the variable occurs only negatively.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears only negatively in the constraint.
Source code in pishield/qflra_requirements/classes.py 
728
729
730
731
732
733
734
735
736
737
def contains_variable_only_negatively(self, x: Variable):
    """Report whether the variable occurs only negatively.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears only negatively in the constraint.
    """
    return self.disjunctive_inequality.contains_variable_only_negatively(x)

contains_variable_both_positively_and_negatively 

contains_variable_both_positively_and_negatively(x: Variable)

Report whether the variable occurs both positively and negatively.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

True if x appears both positively and negatively.
Source code in pishield/qflra_requirements/classes.py 
739
740
741
742
743
744
745
746
747
748
def contains_variable_both_positively_and_negatively(self, x: Variable):
    """Report whether the variable occurs both positively and negatively.

    Args:
        x: The variable to look for.

    Returns:
        ``True`` if ``x`` appears both positively and negatively.
    """
    return self.disjunctive_inequality.contains_variable_both_positively_and_negatively(x)

get_ineq_with_var_y_and_complement 

get_ineq_with_var_y_and_complement(x: Variable)

Return the inequality containing a variable and the remaining ones.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

The result of the underlying

meth:get_ineq_with_var_y_and_complement.
Source code in pishield/qflra_requirements/classes.py 
750
751
752
753
754
755
756
757
758
759
760
def get_ineq_with_var_y_and_complement(self, x: Variable):
    """Return the inequality containing a variable and the remaining ones.

    Args:
        x: The variable to look for.

    Returns:
        The result of the underlying
        :meth:`get_ineq_with_var_y_and_complement`.
    """
    return self.disjunctive_inequality.get_ineq_with_var_y_and_complement(x)

get_ineq_with_pos_and_neg_var_y_and_complement 

get_ineq_with_pos_and_neg_var_y_and_complement(x: Variable)

Return the positive-x and negative-x inequalities and the remainder.

Parameters:

Name Type Description Default
x Variable

The variable to look for.

 required

Returns:

Type Description

The result of the underlying

meth:get_ineq_with_pos_and_neg_var_y_and_complement.
Source code in pishield/qflra_requirements/classes.py 
762
763
764
765
766
767
768
769
770
771
772
def get_ineq_with_pos_and_neg_var_y_and_complement(self, x: Variable):
    """Return the positive-x and negative-x inequalities and the remainder.

    Args:
        x: The variable to look for.

    Returns:
        The result of the underlying
        :meth:`get_ineq_with_pos_and_neg_var_y_and_complement`.
    """
    return self.disjunctive_inequality.get_ineq_with_pos_and_neg_var_y_and_complement(x)

Normalisation

normalisation

Normalisation of QFLRA constraints with respect to a variable.

A constraint (a disjunction of linear inequalities) is put into a normal form in which a given variable occurs at most once positively and at most once negatively, by combining the inequalities where the variable appears with opposite signs.

normalise_constraint_wrt_selected_ineq 

normalise_constraint_wrt_selected_ineq(x: Variable, partially_normalised_inequality_list: List[Inequality], ineq_i: Inequality, signed_ineqs: list[Inequality], sign) -> List[Inequality]

Rewrite a set of inequalities relative to one selected inequality.

Given a selected inequality ineq_i in which variable x appears with the given sign, every other inequality in signed_ineqs (where x appears with the same sign) is rewritten by eliminating x against ineq_i. The selected inequality is kept as-is and the rewritten inequalities are appended to a copy of partially_normalised_inequality_list.

Parameters:

Name Type Description Default
x Variable

The variable being normalised away.

 required
partially_normalised_inequality_list List[Inequality]

Inequalities already accumulated for the new normalised constraint; copied, not mutated.

 required
ineq_i Inequality

The selected reference inequality containing x.

 required
signed_ineqs list[Inequality]

Inequalities in which x appears with the same sign as in ineq_i (including ineq_i itself, which is skipped).

 required
sign

Either 'positive' or 'negative', the sign of x in the selected inequality.

 required

Returns:

Type Description
List[Inequality]

The extended list of inequalities forming (part of) the normalised
List[Inequality]

constraint.

Raises:

Type Description
NotImplementedError

If sign is neither 'positive' nor 'negative'.
Source code in pishield/qflra_requirements/normalisation.py 
 18
 19
 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
def normalise_constraint_wrt_selected_ineq(x: Variable, partially_normalised_inequality_list: List[Inequality], ineq_i: Inequality, signed_ineqs: list[Inequality], sign) -> List[Inequality]:
    """Rewrite a set of inequalities relative to one selected inequality.

    Given a selected inequality ``ineq_i`` in which variable ``x`` appears with the
    given ``sign``, every other inequality in ``signed_ineqs`` (where ``x`` appears
    with the same sign) is rewritten by eliminating ``x`` against ``ineq_i``. The
    selected inequality is kept as-is and the rewritten inequalities are appended to
    a copy of ``partially_normalised_inequality_list``.

    Args:
        x: The variable being normalised away.
        partially_normalised_inequality_list: Inequalities already accumulated for
            the new normalised constraint; copied, not mutated.
        ineq_i: The selected reference inequality containing ``x``.
        signed_ineqs: Inequalities in which ``x`` appears with the same ``sign`` as
            in ``ineq_i`` (including ``ineq_i`` itself, which is skipped).
        sign: Either ``'positive'`` or ``'negative'``, the sign of ``x`` in the
            selected inequality.

    Returns:
        The extended list of inequalities forming (part of) the normalised
        constraint.

    Raises:
        NotImplementedError: If ``sign`` is neither ``'positive'`` nor ``'negative'``.
    """

    new_partially_normalised_inequality_list = []
    new_partially_normalised_inequality_list.extend(partially_normalised_inequality_list)

    # we want to add ineq_j and ineq_k as they are to the set of inequalities that will form the new, normalised constraint
    new_partially_normalised_inequality_list.append(ineq_i)

    # STEP B:
    # once we picked inequalities j and k, we want to rewrite the other constraints where x appears pos, resp. neg, according to j and k
    complementary_atoms_in_i, x_atom_in_i, constant_of_i, _ = ineq_i.get_x_complement_body_atoms(x)

    assert type(x_atom_in_i) != list, "there should be only one x occurrence in ineq_i"

    if sign == 'positive':
        assert x_atom_in_i.positive_sign == True, "x_atom in ineq_i should have positive sign"
    elif sign == 'negative':
        assert x_atom_in_i.positive_sign == False, "x_atom in ineq_i should have negative sign"
    else:
        raise NotImplementedError

    complementary_body_of_i = multiply_coefficients_of_atoms(complementary_atoms_in_i, 1. / x_atom_in_i.coefficient)
    negated_complementary_body_of_i = negate_atoms(complementary_body_of_i)

    for ineq_p in signed_ineqs:
        # discard ineq_i from this process
        if ineq_p.readable() == ineq_i.readable():
            continue

        complementary_atoms_in_p, x_atom_in_p, constant_of_p, is_p_ineq_strict = ineq_p.get_x_complement_body_atoms(x)
        assert type(x_atom_in_p) != list, "there should be only one x occurrence in ineq_p"
        if sign == 'positive':
            assert x_atom_in_p.positive_sign == True, "x_atom in ineq_p should have positive sign"
        elif sign == 'negative':
            assert x_atom_in_p.positive_sign == False, "x_atom in ineq_p should have negative sign"
        else:
            raise NotImplementedError

        complementary_body_of_p = multiply_coefficients_of_atoms(complementary_atoms_in_p, 1. / x_atom_in_p.coefficient)

        if sign == 'positive':
            complementary_body = negate_atoms(complementary_body_of_p)
            complementary_body.extend(complementary_body_of_i)
            complementary_body = collapse_atoms(complementary_body)
            new_constant = ineq_i.constant / x_atom_in_i.coefficient - ineq_p.constant / x_atom_in_p.coefficient

        elif sign == 'negative':
            complementary_body = complementary_body_of_p
            complementary_body.extend(negated_complementary_body_of_i)
            complementary_body = collapse_atoms(complementary_body)
            new_constant = ineq_p.constant / x_atom_in_p.coefficient - ineq_i.constant / x_atom_in_i.coefficient
        else:
            raise NotImplementedError

        new_ineq_sign = ineq_p.ineq_sign if ineq_i.ineq_sign != ineq_p.ineq_sign else '>'
        new_inequality = Inequality(complementary_body, new_ineq_sign, new_constant)

        new_partially_normalised_inequality_list.append(new_inequality)

    return new_partially_normalised_inequality_list

normalise_one_constraint 

normalise_one_constraint(x: Variable, constraint: Constraint) -> Constraint | list[Constraint]

Normalise a single constraint with respect to a variable.

If x already occurs at most once positively and at most once negatively (or not at all), the constraint needs no normalisation and is returned unchanged. Otherwise the inequalities where x appears positively are paired against those where it appears negatively, producing one or more normalised constraints.

Parameters:

Name Type Description Default
x Variable

The variable to normalise with respect to.

 required
constraint Constraint

The constraint (disjunction of inequalities) to normalise.

 required

Returns:

Type Description
Constraint | list[Constraint]

Either the original :class:Constraint (when no normalisation is needed) or
Constraint | list[Constraint]

a list of normalised :class:Constraint objects.
Source code in pishield/qflra_requirements/normalisation.py 
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
def normalise_one_constraint(x: Variable, constraint: Constraint) -> Constraint | list[Constraint]:
    """Normalise a single constraint with respect to a variable.

    If ``x`` already occurs at most once positively and at most once negatively (or
    not at all), the constraint needs no normalisation and is returned unchanged.
    Otherwise the inequalities where ``x`` appears positively are paired against
    those where it appears negatively, producing one or more normalised constraints.

    Args:
        x: The variable to normalise with respect to.
        constraint: The constraint (disjunction of inequalities) to normalise.

    Returns:
        Either the original :class:`Constraint` (when no normalisation is needed) or
        a list of normalised :class:`Constraint` objects.
    """
    # FIRST STEP:
    # check if we need to normalise the constraint
    if len(constraint.list_inequalities) <= 1:
        return constraint

    positive_sign_x = {}
    count_positive_occurrences = 0
    count_negative_occurrences = 0
    for ineq in constraint.list_inequalities:
        if ineq.contains_variable(x):
            body_atoms = ineq.get_body_atoms()
            for atom in body_atoms:
                if atom.variable.id == x.id:
                    positive_sign_x[ineq] = atom.positive_sign
                    if atom.positive_sign:
                        count_positive_occurrences +=1
                    else:
                        count_negative_occurrences +=1
        else:
            positive_sign_x[ineq] = 'null'
    # 3 possible cases for which we don't need to normalise the constraint:
    #   x does not occur in constraint,
    #   x occurs neg/pos once,
    #   x occurs neg and pos once
    # anything else would need normalising
    if count_positive_occurrences <= 1 and count_negative_occurrences <= 1:
        return constraint

    # SECOND STEP:
    # from here we know there is a need to normalise the given constraint w.r.t. variable x
    totally_normalised_constraint = []  # list_of_partially_normalised_constraints

    # STEP A:
    # pick an inequality from those where x appears positively, call it j
    # and pick an inequality from those where x appears negatively, call it k
    pos_ineq = list([ineq for ineq in positive_sign_x.keys() if positive_sign_x[ineq] == True])
    neg_ineq = list([ineq for ineq in positive_sign_x.keys() if positive_sign_x[ineq] == False])
    null_ineq = list([ineq for ineq in positive_sign_x.keys() if positive_sign_x[ineq] == 'null'])

    if len(pos_ineq) > 0 and len(neg_ineq) > 0:
        for ineq_j in pos_ineq:
            pos_partially_normalised_inequality_list = normalise_constraint_wrt_selected_ineq(x, [], ineq_j, pos_ineq, sign='positive')
            for ineq_k in neg_ineq:
                partially_normalised_inequality_list = normalise_constraint_wrt_selected_ineq(x, pos_partially_normalised_inequality_list, ineq_k, neg_ineq, sign='negative')

                # extend the partially_normalised_inequality_list with the ineqs in which x did not appear originally
                partially_normalised_inequality_list.extend(null_ineq)

                # finally return the normalised constraint
                partially_normalised_constraint = Constraint(partially_normalised_inequality_list)
                totally_normalised_constraint.append(partially_normalised_constraint)

    elif len(pos_ineq) > 0 and len(neg_ineq) == 0:
        for ineq_j in pos_ineq:
            partially_normalised_inequality_list = normalise_constraint_wrt_selected_ineq(x, [], ineq_j, pos_ineq, sign='positive')

            # extend the partially_normalised_inequality_list with the ineqs in which x did not appear originally
            partially_normalised_inequality_list.extend(null_ineq)

            # finally return the normalised constraint
            partially_normalised_constraint = Constraint(partially_normalised_inequality_list)
            totally_normalised_constraint.append(partially_normalised_constraint)

    elif len(neg_ineq) > 0 and len(pos_ineq) == 0:
        for ineq_k in neg_ineq:
            partially_normalised_inequality_list = normalise_constraint_wrt_selected_ineq(x, [], ineq_k, neg_ineq, sign='negative')

            # extend the partially_normalised_inequality_list with the ineqs in which x did not appear originally
            partially_normalised_inequality_list.extend(null_ineq)

            # finally return the normalised constraint
            partially_normalised_constraint = Constraint(partially_normalised_inequality_list)
            totally_normalised_constraint.append(partially_normalised_constraint)

    return totally_normalised_constraint

normalise 

normalise(x: Variable, constraints: list[Constraint]) -> list[Constraint]

Normalise every constraint in a list with respect to a variable.

Parameters:

Name Type Description Default
x Variable

The variable to normalise with respect to.

 required
constraints list[Constraint]

List of :class:Constraint objects to normalise.

 required

Returns:

Type Description
list[Constraint]

A flat list of normalised :class:Constraint objects (a single constraint
list[Constraint]

may expand into several after normalisation).
Source code in pishield/qflra_requirements/normalisation.py 
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
def normalise(x: Variable, constraints: list[Constraint]) -> list[Constraint]:
    """Normalise every constraint in a list with respect to a variable.

    Args:
        x: The variable to normalise with respect to.
        constraints: List of :class:`Constraint` objects to normalise.

    Returns:
        A flat list of normalised :class:`Constraint` objects (a single constraint
        may expand into several after normalisation).
    """
    normalised_constraints: list[Constraint] = []

    for constraint in constraints:
        normalised_constraint = normalise_one_constraint(x, constraint)
        if type(normalised_constraint) == list:
            normalised_constraints.extend(normalised_constraint)
        else:
            normalised_constraints.append(normalised_constraint)
    return normalised_constraints

Computing sets of constraints

compute_sets_of_constraints

Computation of per-variable constraint sets via variable elimination.

Following a variable ordering, this module derives, for each variable, the set of constraints that bound it once the higher-ranked variables have been eliminated by algebraic reduction (a resolution-style procedure over linear inequalities).

get_pos_pos_x_constr 

get_pos_pos_x_constr(y: Variable, pos_constr: List[Constraint], pos_neg_constr: List[Constraint])

Derive constraints by reducing positive-y against mixed-sign-y constraints.

For each constraint where y appears only positively and each constraint where y appears both positively and negatively, the positive inequality of the former is reduced against the negative inequality of the latter to eliminate y, building new constraints that retain the remaining inequalities.

Parameters:

Name Type Description Default
y Variable

The variable being eliminated.

 required
pos_constr List[Constraint]

Constraints in which y appears only positively.

 required
pos_neg_constr List[Constraint]

Constraints in which y appears both positively and negatively.

 required

Returns:

Type Description

A list of derived :class:Constraint objects, extended with the original

pos_constr list.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
17
18
19
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
def get_pos_pos_x_constr(y: Variable, pos_constr: List[Constraint], pos_neg_constr: List[Constraint]):
    """Derive constraints by reducing positive-y against mixed-sign-y constraints.

    For each constraint where ``y`` appears only positively and each constraint where
    ``y`` appears both positively and negatively, the positive inequality of the
    former is reduced against the negative inequality of the latter to eliminate
    ``y``, building new constraints that retain the remaining inequalities.

    Args:
        y: The variable being eliminated.
        pos_constr: Constraints in which ``y`` appears only positively.
        pos_neg_constr: Constraints in which ``y`` appears both positively and
            negatively.

    Returns:
        A list of derived :class:`Constraint` objects, extended with the original
        ``pos_constr`` list.
    """
    pos_pos_constr: List[Constraint] = []

    for p in pos_constr:
        p: Constraint
        ineq_from_p_with_pos_y, list_ineqs_from_p_without_y = p.get_ineq_with_var_y_and_complement(y)
        for q in pos_neg_constr:
            q: Constraint
            ineq_from_q_with_pos_y, ineq_from_q_with_neg_y, list_ineqs_from_q_without_y = q.get_ineq_with_pos_and_neg_var_y_and_complement(y)

            # reduce(pos_p_ineq, neg_q_ineq)
            new_inequality = reduce_two_ineqs(y, ineq_from_p_with_pos_y, ineq_from_q_with_neg_y)
            if type(new_inequality) == bool:
                if new_inequality == True:
                    continue
                else:
                    new_list_of_ineqs = []
            else:
                new_list_of_ineqs = [new_inequality]
            new_list_of_ineqs.extend([ineq_from_q_with_pos_y])
            new_list_of_ineqs.extend(list_ineqs_from_p_without_y)
            new_list_of_ineqs.extend(list_ineqs_from_q_without_y)
            pos_pos_constr.append(Constraint(new_list_of_ineqs))

    # finally, extend pos_pos_constr with pos_constr
    pos_pos_constr.extend(pos_constr)
    return pos_pos_constr

create_constr_by_reduction 

create_constr_by_reduction(y: Variable, constraints_with_y: List[Constraint])

Eliminate a variable by reducing pairs of constraints over it.

The constraints containing y are split by the sign of y; pairs of positive-y and negative-y constraints are then reduced to produce new constraints that no longer contain y.

Parameters:

Name Type Description Default
y Variable

The variable being eliminated.

 required
constraints_with_y List[Constraint]

Constraints that contain y.

 required

Returns:

Type Description

A list of derived :class:Constraint objects with y removed.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
 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
def create_constr_by_reduction(y: Variable, constraints_with_y: List[Constraint]):
    """Eliminate a variable by reducing pairs of constraints over it.

    The constraints containing ``y`` are split by the sign of ``y``; pairs of
    positive-y and negative-y constraints are then reduced to produce new
    constraints that no longer contain ``y``.

    Args:
        y: The variable being eliminated.
        constraints_with_y: Constraints that contain ``y``.

    Returns:
        A list of derived :class:`Constraint` objects with ``y`` removed.
    """
    red_constr = []
    # separate the constraints in two sets by the sign of y (pos or neg)
    pos_constr, neg_constr, pos_neg_constr = get_pos_neg_pn_x_constr(y, constraints_with_y)

    pos_pos_constr = get_pos_pos_x_constr(y, pos_constr, pos_neg_constr)

    # then obtain new constr by reduction on y from pairs of constr (p,q)
    # where p is from pos_constr and q is from neg_constr
    for p in pos_pos_constr:
        p: Constraint
        ineq_from_p_with_y, list_ineqs_from_p_without_y = p.get_ineq_with_var_y_and_complement(y)
        for q in neg_constr:
            q: Constraint
            ineq_from_q_with_y, list_ineqs_from_q_without_y = q.get_ineq_with_var_y_and_complement(y)

            new_inequality = reduce_two_ineqs(y, ineq_from_p_with_y, ineq_from_q_with_y)

            if type(new_inequality) == bool:
                if new_inequality == True:
                    continue
                else:
                    new_list_of_ineqs = []
            else:
                new_list_of_ineqs = [new_inequality]
            new_list_of_ineqs.extend(list_ineqs_from_p_without_y)
            new_list_of_ineqs.extend(list_ineqs_from_q_without_y)
            red_constr.append(Constraint(new_list_of_ineqs))

    return red_constr

reduce_two_ineqs 

reduce_two_ineqs(y, ineq_with_pos_y, ineq_with_neg_y)

Combine two inequalities to eliminate a shared variable.

Scales and adds the two inequalities (one with y positive, one with y negative) so that y cancels, yielding a new inequality on the remaining atoms. When all atoms cancel, the result is the boolean truth value of the resulting trivial inequality.

Parameters:

Name Type Description Default
y

The variable to eliminate.

 required
ineq_with_pos_y

An :class:Inequality where y appears positively.

 required
ineq_with_neg_y

An :class:Inequality where y appears negatively.

 required

Returns:

Type Description

A new :class:Inequality over the remaining atoms, or a bool giving the

satisfaction value when the reduced body is empty.

Raises:

Type Description
NotImplementedError

If the resulting inequality sign is unsupported.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
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
def reduce_two_ineqs(y, ineq_with_pos_y, ineq_with_neg_y):
    """Combine two inequalities to eliminate a shared variable.

    Scales and adds the two inequalities (one with ``y`` positive, one with ``y``
    negative) so that ``y`` cancels, yielding a new inequality on the remaining
    atoms. When all atoms cancel, the result is the boolean truth value of the
    resulting trivial inequality.

    Args:
        y: The variable to eliminate.
        ineq_with_pos_y: An :class:`Inequality` where ``y`` appears positively.
        ineq_with_neg_y: An :class:`Inequality` where ``y`` appears negatively.

    Returns:
        A new :class:`Inequality` over the remaining atoms, or a ``bool`` giving the
        satisfaction value when the reduced body is empty.

    Raises:
        NotImplementedError: If the resulting inequality sign is unsupported.
    """
    p_coeff, p_complementary_body = split_constr_atoms(y, ineq_with_pos_y)
    q_coeff, q_complementary_body = split_constr_atoms(y, ineq_with_neg_y)
    # if p_complementary_body == []:
    #     break
    # if q_complementary_body == []:
    #     continue
    # multiply all coeff in p by q_coeff
    complementary_body = multiply_coefficients_of_atoms(p_complementary_body, q_coeff / p_coeff)
    # take the union of the p and q lists of atoms,
    # excluding the atom corresponding to y (whose coefficient is now 0)
    complementary_body.extend(q_complementary_body)
    # merge any atom duplicates
    complementary_body = collapse_atoms(complementary_body)
    _, ineq_sign_p, constant_p = ineq_with_pos_y.get_ineq_attributes()
    _, ineq_sign_q, constant_q = ineq_with_neg_y.get_ineq_attributes()
    new_ineq_sign = '>' if ineq_sign_p != ineq_sign_q else ineq_sign_p
    new_constant = (constant_p * q_coeff / p_coeff) + constant_q
    if complementary_body != []:
        new_inequality = Inequality(complementary_body, new_ineq_sign, new_constant)
    elif complementary_body == []:
        if new_ineq_sign == '>':
            sat_val = 0 > new_constant
        elif new_ineq_sign == '>=':
            sat_val = 0 >= new_constant
        else:
            raise NotImplementedError
        return sat_val
    else:
        raise Exception
    return new_inequality

get_pos_neg_pn_x_constr 

get_pos_neg_pn_x_constr(y: Variable, constraints: List[Constraint])

Group constraints by how a variable occurs in them.

Parameters:

Name Type Description Default
y Variable

The variable to inspect.

 required
constraints List[Constraint]

Constraints to classify.

 required

Returns:

Type Description

A tuple (pos_constr, neg_constr, pos_neg_constr) of lists holding the

constraints where y appears only positively, only negatively, and both

positively and negatively, respectively.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
def get_pos_neg_pn_x_constr(y: Variable, constraints: List[Constraint]):
    """Group constraints by how a variable occurs in them.

    Args:
        y: The variable to inspect.
        constraints: Constraints to classify.

    Returns:
        A tuple ``(pos_constr, neg_constr, pos_neg_constr)`` of lists holding the
        constraints where ``y`` appears only positively, only negatively, and both
        positively and negatively, respectively.
    """
    pos_constr, neg_constr, pos_neg_constr = [], [], []
    for constr in constraints:
        # determine if y appears: (i) only pos, (ii) only neg, (iii) both pos and neg in the constr
        if constr.contains_variable_only_positively(y):
            pos_constr.append(constr)
        if constr.contains_variable_only_negatively(y):
            neg_constr.append(constr)
        if constr.contains_variable_both_positively_and_negatively(y):
            pos_neg_constr.append(constr)
    return pos_constr, neg_constr, pos_neg_constr

get_pos_neg_x_constr 

get_pos_neg_x_constr(y: Variable, constraints_with_y: List[Constraint])

Split constraints by the sign of a variable, discarding mixed-sign ones.

Constraints where y appears both positively and negatively are ignored.

Parameters:

Name Type Description Default
y Variable

The variable to inspect.

 required
constraints_with_y List[Constraint]

Constraints that contain y.

 required

Returns:

Type Description

A tuple (pos_constr, neg_constr) of lists holding constraints where y

appears only positively and only negatively, respectively.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
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
def get_pos_neg_x_constr(y: Variable, constraints_with_y: List[Constraint]):
    """Split constraints by the sign of a variable, discarding mixed-sign ones.

    Constraints where ``y`` appears both positively and negatively are ignored.

    Args:
        y: The variable to inspect.
        constraints_with_y: Constraints that contain ``y``.

    Returns:
        A tuple ``(pos_constr, neg_constr)`` of lists holding constraints where ``y``
        appears only positively and only negatively, respectively.
    """
    pos_constr, neg_constr = [], []
    for constr in constraints_with_y:
        # first determine if y appears: (i) only pos, (ii) only neg, (iii) both pos and neg in the constr

        # if (iii), discard this constr
        if constr.contains_variable_both_positively_and_negatively(y):
            continue
        # if (i), then add to pos_constr; if (ii), add to neg_constr
        if constr.contains_variable_only_positively(y):
            pos_constr.append(constr)
        if constr.contains_variable_only_negatively(y):
            neg_constr.append(constr)
    return pos_constr, neg_constr

compute_set_of_constraints_for_variable 

compute_set_of_constraints_for_variable(x: Variable, prev_x: Variable, normalised_constraints_at_previous_level: List[Constraint], verbose)

Compute the constraint set for the next variable in the ordering.

Constraints from the previous level that mention prev_x are reduced to eliminate prev_x; the result is unioned with the constraints that did not mention prev_x.

Parameters:

Name Type Description Default
x Variable

The variable for the current level (used for logging/context).

 required
prev_x Variable

The previously processed variable to be eliminated.

 required
normalised_constraints_at_previous_level List[Constraint]

Normalised constraints produced for prev_x.

 required
verbose

Whether to print verbose progress information.

 required

Returns:

Type Description

The list of (still unnormalised) :class:Constraint objects that no longer

contain prev_x.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
def compute_set_of_constraints_for_variable(x: Variable, prev_x: Variable, normalised_constraints_at_previous_level: List[Constraint], verbose):
    """Compute the constraint set for the next variable in the ordering.

    Constraints from the previous level that mention ``prev_x`` are reduced to
    eliminate ``prev_x``; the result is unioned with the constraints that did not
    mention ``prev_x``.

    Args:
        x: The variable for the current level (used for logging/context).
        prev_x: The previously processed variable to be eliminated.
        normalised_constraints_at_previous_level: Normalised constraints produced for
            ``prev_x``.
        verbose: Whether to print verbose progress information.

    Returns:
        The list of (still unnormalised) :class:`Constraint` objects that no longer
        contain ``prev_x``.
    """
    # create two sets starting from constraints_at_previous_level:
    # one containing only the constraints which variable prev_x appears in
    # and its complement
    unnormalised_constraints_without_prev = []
    normalised_constraints_with_prev = []

    for constr in normalised_constraints_at_previous_level:
        if constr.contains_variable(prev_x):
            normalised_constraints_with_prev.append(constr)
        else:
            unnormalised_constraints_without_prev.append(constr)

    # then compute a new set of constraints derived by algebraic manipulation on constraints containing prev_x
    # note that this new set of constraints will not have occurrences of prev_x by construction
    reduced_constr = create_constr_by_reduction(prev_x, normalised_constraints_with_prev)

    # finally, get the union of constraints which do not contain y (unnormalised_constraints_without_prev U reduced_constr)
    unnormalised_constraints_without_prev.extend(reduced_constr)

    # if verbose:
    #     print('\nLEVEL', x.readable())
    #     print('-------------------Constraints at this level:')
    #     for constr in unnormalised_constraints_without_prev:
    #         print(constr.readable())

    return unnormalised_constraints_without_prev

compute_sets_of_constraints 

compute_sets_of_constraints(ordering: List[Variable], constraints: List[Constraint], verbose) -> {Variable: List[Constraint]}

Compute the normalised constraint set bounding each variable.

Processes the variables in reverse order, eliminating each higher-ranked variable in turn so that the constraints associated with a variable only involve that variable and lower-ranked ones. This is the precomputation consumed by the prediction-correction pass.

Parameters:

Name Type Description Default
ordering List[Variable]

The variable ordering (ascending); processed in reverse.

 required
constraints List[Constraint]

The full list of parsed :class:Constraint objects.

 required
verbose

Whether to print verbose progress information.

 required

Returns:

Type Description
{Variable: List[Constraint]}

A dict mapping each :class:Variable to the list of normalised
{Variable: List[Constraint]}

class:Constraint objects that bound it at its level.
Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
def compute_sets_of_constraints(ordering: List[Variable], constraints: List[Constraint], verbose) -> {Variable: List[Constraint]}:
    """Compute the normalised constraint set bounding each variable.

    Processes the variables in reverse order, eliminating each higher-ranked
    variable in turn so that the constraints associated with a variable only involve
    that variable and lower-ranked ones. This is the precomputation consumed by the
    prediction-correction pass.

    Args:
        ordering: The variable ordering (ascending); processed in reverse.
        constraints: The full list of parsed :class:`Constraint` objects.
        verbose: Whether to print verbose progress information.

    Returns:
        A dict mapping each :class:`Variable` to the list of normalised
        :class:`Constraint` objects that bound it at its level.
    """
    print(f' *** ALL CONSTRAINTS ***')
    for constr in constraints:
        print(constr.readable())
    # reverse the ordering:
    ordering = list(reversed(ordering))
    prev_x = ordering[0]

    # add all constraints for the highest ranking variable w.r.t. ordering
    ordered_normalised_constraints = {prev_x: normalise(prev_x, constraints)}
    print(f' *** Normalised Constraints for {prev_x.readable()} ***')
    for constr in constraints:
        print(constr.readable())

    for x in ordering[1:]:
        normalised_constraints_at_previous_level = ordered_normalised_constraints[prev_x]
        set_of_constraints = compute_set_of_constraints_for_variable(x, prev_x, normalised_constraints_at_previous_level, verbose)
        print(f' *** Unnormalised Constraints for {x.readable()} ***')
        for constr in set_of_constraints:
            print(constr.readable())
        ordered_normalised_constraints[x] = normalise(x, set_of_constraints)
        print(f'\n *** Normalised Constraints for {x.readable()} ***')
        for constr in ordered_normalised_constraints[x]:
            print(constr.readable())
        prev_x = x

    # print('-'*80)
    # for x in ordering:
    #     print(f' *** Constraints for {x.readable()} ***')
    #     for i,constr in enumerate(ordered_normalised_constraints[x]):
    #         print(f'constr number {i}')
    #         print(constr.readable())
    #     if len(ordered_normalised_constraints[x]) == 0:
    #         print('empty set')
    #     print('***\n')
    print('-'*80)

    return ordered_normalised_constraints

main 

main()

Run a small demo: parse a constraints file and compute its constraint sets.

Source code in pishield/qflra_requirements/compute_sets_of_constraints.py 
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
def main():
    """Run a small demo: parse a constraints file and compute its constraint sets."""
    # ordering, constraints = parser.parse_constraints_file('../data/tiny_constraints.txt')
    ordering, constraints = parse_constraints_file('../data/heloc/heloc_constraints.txt')
    # for constr in constraints:
    #     print(constr.readable())
    #     # for elem in constr.inequality_list[-1].body:
    #     #     print('id', elem.get_variable_id())

    print('verbose constr')
    for constr in constraints:
        print(constr.verbose_readable())
    # print(constraints)

    print('compute sets of constraints')
    sets_of_constr = compute_sets_of_constraints(ordering, constraints, verbose=True)

Correcting predictions

correct_predictions

Differentiable correction of predictions against QFLRA requirements.

Given precomputed per-variable constraint sets, this module derives lower/upper bounds for each variable and clips predictions into the feasible region implied by the (possibly disjunctive) constraints, processing variables in the given ordering.

get_constr_at_level_x 

get_constr_at_level_x(x, sets_of_constr)

Look up the constraint set associated with a variable.

Parameters:

Name Type Description Default
x

The variable whose constraints are requested.

 required
sets_of_constr

Mapping from :class:Variable to its list of constraints.

 required

Returns:

Type Description

The list of :class:Constraint objects for the variable with the same id as

x, or None if no matching variable is present.
Source code in pishield/qflra_requirements/correct_predictions.py 
26
27
28
29
30
31
32
33
34
35
36
37
38
39
def get_constr_at_level_x(x, sets_of_constr):
    """Look up the constraint set associated with a variable.

    Args:
        x: The variable whose constraints are requested.
        sets_of_constr: Mapping from :class:`Variable` to its list of constraints.

    Returns:
        The list of :class:`Constraint` objects for the variable with the same id as
        ``x``, or ``None`` if no matching variable is present.
    """
    for var in sets_of_constr:
        if var.id == x.id:
            return sets_of_constr[var]

get_lb_from_one_constraint 

get_lb_from_one_constraint(x: Variable, constraint: Constraint, preds: Tensor, epsilon=1e-12)

Compute the per-sample lower bound on a variable from one constraint.

The constraint (in which x appears positively) is rearranged into the form x >= ... and evaluated on the batch. A small epsilon is added for strict inequalities.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
constraint Constraint

A constraint that bounds x from below.

 required
preds Tensor

Predictions tensor of shape (B, D).

 required
epsilon

Slack added for strict ('>') inequalities.

 1e-12

Returns:

Type Description

A tensor of shape (B,) with the lower bound on x per sample.
Source code in pishield/qflra_requirements/correct_predictions.py 
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
def get_lb_from_one_constraint(x: Variable, constraint: Constraint, preds: torch.Tensor, epsilon=1e-12):
    """Compute the per-sample lower bound on a variable from one constraint.

    The constraint (in which ``x`` appears positively) is rearranged into the form
    ``x >= ...`` and evaluated on the batch. A small ``epsilon`` is added for strict
    inequalities.

    Args:
        x: The variable to bound.
        constraint: A constraint that bounds ``x`` from below.
        preds: Predictions tensor of shape ``(B, D)``.
        epsilon: Slack added for strict ('>') inequalities.

    Returns:
        A tensor of shape ``(B,)`` with the lower bound on ``x`` per sample.
    """
    mask_sat_batch_elem = None  # NOTE: the mask should be reset when a new constraint is considered, regardless of its type (ineq or disj of ineq!)
    if len(constraint.list_inequalities) == 1:
        complement_body_atoms, x_atom, constr_constant, is_strict_inequality = constraint.disjunctive_inequality.get_x_complement_body_atoms(x)  #   this gets the get_x_complement_body_atoms from Ineq class
    else:
        complement_body_atoms, x_atom, constr_constant, is_strict_inequality = constraint.disjunctive_inequality.get_x_complement_body_atoms(x, sign_of_x='positive')
        # if x_atom is None: # this is not possible as the method is called on constr that contain x: either pos, neg or both pos and neg
        #     continue

    # if x is y1 and inequality is -y1>0, then add 0+bias to dependency_complements
    if len(complement_body_atoms) == 0:
        eval_body = torch.zeros(preds.shape[0])  # shape (B,)
    else:
        # evaluate the body of constr, after eliminating x occurrences from it
        eval_body = eval_atoms_list(complement_body_atoms, preds)  # shape (B,)

    # rewrite   ax + B >= c
    # to        x >= -B/a + c/a
    # to get lb = c*(1/a) - B*(1/a)
    lb = constr_constant * (1. / x_atom.coefficient) - eval_body * (1. / x_atom.coefficient)

    # then add/subtract epsilon if the ineq is strict: +epsilon if positive x, -epsilon otherwise
    if is_strict_inequality:
        lb += epsilon

    # if the constr is a disj of inqs, mask out the batch elements for which mask_sat_batch_elem is True
    if mask_sat_batch_elem is not None:
        lb[mask_sat_batch_elem] += -INFINITY
    return lb

get_ub_from_one_constraint 

get_ub_from_one_constraint(x: Variable, constraint: Constraint, preds: Tensor, epsilon=1e-12)

Compute the per-sample upper bound on a variable from one constraint.

The constraint (in which x appears negatively) is rearranged into the form x <= ... and evaluated on the batch. A small epsilon is subtracted for strict inequalities.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
constraint Constraint

A constraint that bounds x from above.

 required
preds Tensor

Predictions tensor of shape (B, D).

 required
epsilon

Slack subtracted for strict ('>') inequalities.

 1e-12

Returns:

Type Description

A tensor of shape (B,) with the upper bound on x per sample, or

None if x does not appear in the constraint with the expected sign.
Source code in pishield/qflra_requirements/correct_predictions.py 
 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
def get_ub_from_one_constraint(x: Variable, constraint: Constraint, preds: torch.Tensor, epsilon=1e-12):
    """Compute the per-sample upper bound on a variable from one constraint.

    The constraint (in which ``x`` appears negatively) is rearranged into the form
    ``x <= ...`` and evaluated on the batch. A small ``epsilon`` is subtracted for
    strict inequalities.

    Args:
        x: The variable to bound.
        constraint: A constraint that bounds ``x`` from above.
        preds: Predictions tensor of shape ``(B, D)``.
        epsilon: Slack subtracted for strict ('>') inequalities.

    Returns:
        A tensor of shape ``(B,)`` with the upper bound on ``x`` per sample, or
        ``None`` if ``x`` does not appear in the constraint with the expected sign.
    """
    mask_sat_batch_elem = None  # NOTE: the mask should be reset when a new constraint is considered, regardless of its type (ineq or disj of ineq!)
    if len(constraint.list_inequalities) == 1:
        complement_body_atoms, x_atom, constr_constant, is_strict_inequality = constraint.disjunctive_inequality.get_x_complement_body_atoms(x)  #  this gets the get_x_complement_body_atoms from Ineq class
    else:
        complement_body_atoms, x_atom, constr_constant, is_strict_inequality = constraint.disjunctive_inequality.get_x_complement_body_atoms(x, sign_of_x='negative')
        if x_atom is None: # this is not possible as the method is called on constr that contain x: either pos, neg or both pos and neg
            return None

    # if x is y1 and inequality is -y1>0, then add 0+bias to dependency_complements
    if len(complement_body_atoms) == 0:
        eval_body = torch.zeros(preds.shape[0])  # shape (B,)
    else:
        # evaluate the body of constr, after eliminating x occurrences from it
        eval_body = eval_atoms_list(complement_body_atoms, preds)  # shape (B,)

    # rewrite   -ax + B >= c        equiv. to ax - B <= -c
    # to        -x >= -B/a + c/a    equiv. to x <= B/a - c/a
    # to get ub = B*(1/a) - c*(1/a)
    ub = eval_body * (1. / x_atom.coefficient) - constr_constant * (1. / x_atom.coefficient)

    # then add/subtract epsilon if the ineq is strict: +epsilon if positive x, -epsilon otherwise
    if is_strict_inequality:
        ub -= epsilon

    # if the constr is a disj of inqs, mask out the batch elements for which mask_sat_batch_elem is True
    if mask_sat_batch_elem is not None:
        ub[mask_sat_batch_elem] += INFINITY
    return ub

get_lower_bounds 

get_lower_bounds(x: Variable, x_constraints: List[Constraint], preds: Tensor, epsilon=1e-12) -> torch.Tensor

Collect the lower bounds on a variable from all relevant constraints.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
x_constraints List[Constraint]

Constraints that bound x from below.

 required
preds Tensor

Predictions tensor of shape (B, D).

 required
epsilon

Slack passed through to :func:get_lb_from_one_constraint.

 1e-12

Returns:

Type Description
Tensor

A tensor of shape (B, M) stacking the M lower bounds per sample, or
Tensor

-INFINITY when there are no constraints.
Source code in pishield/qflra_requirements/correct_predictions.py 
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
def get_lower_bounds(x: Variable, x_constraints: List[Constraint], preds: torch.Tensor, epsilon=1e-12) -> torch.Tensor:
    """Collect the lower bounds on a variable from all relevant constraints.

    Args:
        x: The variable to bound.
        x_constraints: Constraints that bound ``x`` from below.
        preds: Predictions tensor of shape ``(B, D)``.
        epsilon: Slack passed through to :func:`get_lb_from_one_constraint`.

    Returns:
        A tensor of shape ``(B, M)`` stacking the ``M`` lower bounds per sample, or
        ``-INFINITY`` when there are no constraints.
    """
    if len(x_constraints) == 0:
        return -INFINITY

    lbs = [] # size: num_atom_dependencies x B (i.e. B=batch size)
    for constr in x_constraints:
        lb = get_lb_from_one_constraint(x, constr, preds, epsilon)
        lbs.append(lb)

    if len(lbs) > 1:
        lbs = torch.stack(lbs, dim=1)
    elif len(lbs) == 1:
        lbs = lbs[0].unsqueeze(1)
    else:
        # if no lb is found, return -inf as lower bound (i.e., x>-inf)
        return -INFINITY
    return lbs

get_upper_bounds 

get_upper_bounds(x: Variable, x_constraints: List[Constraint], preds: Tensor, epsilon=1e-12) -> torch.Tensor

Collect the upper bounds on a variable from all relevant constraints.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
x_constraints List[Constraint]

Constraints that bound x from above.

 required
preds Tensor

Predictions tensor of shape (B, D).

 required
epsilon

Slack passed through to :func:get_ub_from_one_constraint.

 1e-12

Returns:

Type Description
Tensor

A tensor of shape (B, M) stacking the M upper bounds per sample, or
Tensor

INFINITY when there are no constraints (or none yield a bound).
Source code in pishield/qflra_requirements/correct_predictions.py 
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
def get_upper_bounds(x: Variable, x_constraints: List[Constraint], preds: torch.Tensor, epsilon=1e-12) -> torch.Tensor:
    """Collect the upper bounds on a variable from all relevant constraints.

    Args:
        x: The variable to bound.
        x_constraints: Constraints that bound ``x`` from above.
        preds: Predictions tensor of shape ``(B, D)``.
        epsilon: Slack passed through to :func:`get_ub_from_one_constraint`.

    Returns:
        A tensor of shape ``(B, M)`` stacking the ``M`` upper bounds per sample, or
        ``INFINITY`` when there are no constraints (or none yield a bound).
    """
    if len(x_constraints) == 0:
        return INFINITY

    ubs = []  # size: num_atom_dependencies x B (i.e. B=batch size)
    for constr in x_constraints:
        ub = get_ub_from_one_constraint(x, constr, preds, epsilon)
        if ub is None:
            continue
        ubs.append(ub)

    if len(ubs) > 1:
        ubs = torch.stack(ubs, dim=1)
    elif len(ubs) == 1:
        ubs = ubs[0].unsqueeze(1)
    else:
        # if no ub is found, return +inf as upper bound (i.e., x<inf equiv. to -x > -inf)
        return INFINITY
    return ubs

get_final_x_correction 

get_final_x_correction(initial_x_val: Tensor, lower_bounds: Tensor, upper_bounds: Tensor) -> torch.Tensor

Clip a variable's values into the feasible interval given its bounds.

The initial value is raised to the lower bound and then lowered to the upper bound (per sample). Infinite bounds are treated as no constraint. Used for the purely conjunctive (non-disjunctive) case.

Parameters:

Name Type Description Default
initial_x_val Tensor

Tensor of shape (B,) with the current value of x.

 required
lower_bounds Tensor

Greatest lower bound per sample, or a non-tensor sentinel when there is no lower bound.

 required
upper_bounds Tensor

Least upper bound per sample, or a non-tensor sentinel when there is no upper bound.

 required

Returns:

Type Description
Tensor

A tensor of shape (B,) with the corrected, feasible values of x.
Source code in pishield/qflra_requirements/correct_predictions.py 
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
def get_final_x_correction(initial_x_val: torch.Tensor, lower_bounds: torch.Tensor, upper_bounds: torch.Tensor) -> torch.Tensor:
    """Clip a variable's values into the feasible interval given its bounds.

    The initial value is raised to the lower bound and then lowered to the upper
    bound (per sample). Infinite bounds are treated as no constraint. Used for the
    purely conjunctive (non-disjunctive) case.

    Args:
        initial_x_val: Tensor of shape ``(B,)`` with the current value of ``x``.
        lower_bounds: Greatest lower bound per sample, or a non-tensor sentinel when
            there is no lower bound.
        upper_bounds: Least upper bound per sample, or a non-tensor sentinel when
            there is no upper bound.

    Returns:
        A tensor of shape ``(B,)`` with the corrected, feasible values of ``x``.
    """

    if type(lower_bounds) is not torch.Tensor:
        lb_constrained_result = initial_x_val
    else:
        # print(initial_x_val, pos_x_corrected)
        lower_bounds = lower_bounds.where(~(lower_bounds == INFINITY), initial_x_val)
        # keep_initial_pos_mask = pos_x_corrected.isinf()
        # pos_x_corrected1 = pos_x_corrected.clone()
        # pos_x_corrected2 = pos_x_corrected.clone()
        # pos_x_corrected3 = pos_x_corrected.clone()
        # pos_x_corrected1[keep_initial_pos_mask] = initial_x_val[keep_initial_pos_mask]
        # pos_x_corrected2 = torch.where(pos_x_corrected == INFINITY, initial_x_val, pos_x_corrected)
        # pos_x_corrected3 = pos_x_corrected.where(~(pos_x_corrected == INFINITY), initial_x_val)
        #
        # assert (pos_x_corrected1 == pos_x_corrected2).all(), (pos_x_corrected1, pos_x_corrected2, pos_x_corrected)
        # assert (pos_x_corrected1 == pos_x_corrected3).all(), (pos_x_corrected1, pos_x_corrected3, pos_x_corrected)
        lb_constrained_result = torch.cat([initial_x_val.unsqueeze(1), lower_bounds.unsqueeze(1)], dim=1).amax(dim=1)

    if type(upper_bounds) is not torch.Tensor:
        ub_constrained_result = lb_constrained_result
    else:
        # keep_initial_neg_mask = neg_x_corrected.isinf()
        # neg_x_corrected[keep_initial_neg_mask] = initial_x_val[keep_initial_neg_mask]
        upper_bounds = upper_bounds.where(~(upper_bounds == INFINITY), initial_x_val)
        ub_constrained_result = torch.cat([lb_constrained_result.unsqueeze(1), upper_bounds.unsqueeze(1)], dim=1).amin(dim=1)

    final_constrained_result = ub_constrained_result
    return final_constrained_result

get_right_bounds 

get_right_bounds(x: Variable, partially_corrected_preds: Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor

Compute the right (lower) bounds on a variable.

Right bounds are the lower bounds on x (values x must lie to the right of), obtained from constraints where x appears positively.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
partially_corrected_preds Tensor

Predictions tensor of shape (B, D) with corrections from previously processed variables.

 required
constraints_at_level_x List[Constraint]

Constraints bounding x from below.

 required

Returns:

Type Description
Tensor

The lower bounds tensor (or sentinel) returned by :func:get_lower_bounds.
Source code in pishield/qflra_requirements/correct_predictions.py 
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
def get_right_bounds(x: Variable, partially_corrected_preds: torch.Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor:
    """Compute the right (lower) bounds on a variable.

    Right bounds are the lower bounds on ``x`` (values ``x`` must lie to the right
    of), obtained from constraints where ``x`` appears positively.

    Args:
        x: The variable to bound.
        partially_corrected_preds: Predictions tensor of shape ``(B, D)`` with
            corrections from previously processed variables.
        constraints_at_level_x: Constraints bounding ``x`` from below.

    Returns:
        The lower bounds tensor (or sentinel) returned by :func:`get_lower_bounds`.
    """
    all_right_bounds = get_lower_bounds(x, constraints_at_level_x, partially_corrected_preds)
    return all_right_bounds

get_left_bounds 

get_left_bounds(x: Variable, partially_corrected_preds: Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor

Compute the left (upper) bounds on a variable.

Left bounds are the upper bounds on x (values x must lie to the left of), obtained from constraints where x appears negatively.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
partially_corrected_preds Tensor

Predictions tensor of shape (B, D) with corrections from previously processed variables.

 required
constraints_at_level_x List[Constraint]

Constraints bounding x from above.

 required

Returns:

Type Description
Tensor

The upper bounds tensor (or sentinel) returned by :func:get_upper_bounds.
Source code in pishield/qflra_requirements/correct_predictions.py 
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
def get_left_bounds(x: Variable, partially_corrected_preds: torch.Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor:
    """Compute the left (upper) bounds on a variable.

    Left bounds are the upper bounds on ``x`` (values ``x`` must lie to the left
    of), obtained from constraints where ``x`` appears negatively.

    Args:
        x: The variable to bound.
        partially_corrected_preds: Predictions tensor of shape ``(B, D)`` with
            corrections from previously processed variables.
        constraints_at_level_x: Constraints bounding ``x`` from above.

    Returns:
        The upper bounds tensor (or sentinel) returned by :func:`get_upper_bounds`.
    """
    all_left_bounds = get_upper_bounds(x, constraints_at_level_x, partially_corrected_preds)
    return all_left_bounds

get_closest_left_bound 

get_closest_left_bound(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)

Pick the feasible left (upper) bound closest to a variable's value.

Among the candidate left bounds, those that would still violate some constraint are discarded; of the remaining ones, the bound closest to the current value of x is returned (per sample).

Parameters:

Name Type Description Default
x

The variable to bound.

 required
partially_corrected_preds_for_x

Predictions tensor of shape (B, D).

 required
left_bounds

Candidate left bounds tensor of shape (B, M), or a non-tensor sentinel (returned as-is).

 required
right_bounds

Unused in this routine (kept for signature symmetry).

 required
constraints_at_level_x

Constraints used to test feasibility of each bound.

 required

Returns:

Type Description

A tensor of shape (B,) with the closest feasible left bound per sample,

or the left_bounds sentinel when it is not a tensor.
Source code in pishield/qflra_requirements/correct_predictions.py 
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
def get_closest_left_bound(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x):
    """Pick the feasible left (upper) bound closest to a variable's value.

    Among the candidate left bounds, those that would still violate some constraint
    are discarded; of the remaining ones, the bound closest to the current value of
    ``x`` is returned (per sample).

    Args:
        x: The variable to bound.
        partially_corrected_preds_for_x: Predictions tensor of shape ``(B, D)``.
        left_bounds: Candidate left bounds tensor of shape ``(B, M)``, or a non-tensor
            sentinel (returned as-is).
        right_bounds: Unused in this routine (kept for signature symmetry).
        constraints_at_level_x: Constraints used to test feasibility of each bound.

    Returns:
        A tensor of shape ``(B,)`` with the closest feasible left bound per sample,
        or the ``left_bounds`` sentinel when it is not a tensor.
    """
    if type(left_bounds) is not torch.Tensor:
        return left_bounds
    else:
        mask_samples_violating_req = []
        initial_x_val = partially_corrected_preds_for_x[:, x.id].clone()

        for b in range(0, left_bounds.shape[-1]):
            preds_with_left_bounds_for_x = partially_corrected_preds_for_x.clone()
            preds_with_left_bounds_for_x[:, x.id] = left_bounds[:, b]

            mask_samples_violating_req_for_bound_b = get_samples_violating_constraints(constraints_at_level_x, preds_with_left_bounds_for_x)
            mask_samples_violating_req.append(mask_samples_violating_req_for_bound_b)

        mask_samples_violating_req = torch.stack(mask_samples_violating_req, dim=1)
        valid_left_bounds = torch.where(~mask_samples_violating_req, left_bounds, torch.inf)
        distance_of_bounds_from_x = torch.abs(valid_left_bounds - initial_x_val.unsqueeze(1))
        mask_bounds_of_minimum_distance = distance_of_bounds_from_x == distance_of_bounds_from_x.amin(dim=1, keepdim=True)

        closest_left_bound_wrt_x = torch.where(mask_bounds_of_minimum_distance, valid_left_bounds, torch.inf).amin(dim=1)
        return closest_left_bound_wrt_x

get_closest_right_bound 

get_closest_right_bound(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)

Pick the feasible right (lower) bound closest to a variable's value.

Among the candidate right bounds, those that would still violate some constraint are discarded; of the remaining ones, the bound closest to the current value of x is returned (per sample).

Parameters:

Name Type Description Default
x

The variable to bound.

 required
partially_corrected_preds_for_x

Predictions tensor of shape (B, D).

 required
left_bounds

Unused in this routine (kept for signature symmetry).

 required
right_bounds

Candidate right bounds tensor of shape (B, M), or a non-tensor sentinel (returned as-is).

 required
constraints_at_level_x

Constraints used to test feasibility of each bound.

 required

Returns:

Type Description

A tensor of shape (B,) with the closest feasible right bound per sample,

or the right_bounds sentinel when it is not a tensor.
Source code in pishield/qflra_requirements/correct_predictions.py 
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
def get_closest_right_bound(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x):
    """Pick the feasible right (lower) bound closest to a variable's value.

    Among the candidate right bounds, those that would still violate some constraint
    are discarded; of the remaining ones, the bound closest to the current value of
    ``x`` is returned (per sample).

    Args:
        x: The variable to bound.
        partially_corrected_preds_for_x: Predictions tensor of shape ``(B, D)``.
        left_bounds: Unused in this routine (kept for signature symmetry).
        right_bounds: Candidate right bounds tensor of shape ``(B, M)``, or a
            non-tensor sentinel (returned as-is).
        constraints_at_level_x: Constraints used to test feasibility of each bound.

    Returns:
        A tensor of shape ``(B,)`` with the closest feasible right bound per sample,
        or the ``right_bounds`` sentinel when it is not a tensor.
    """
    if type(right_bounds) is not torch.Tensor:
        return right_bounds
    else:
        mask_samples_violating_req = []
        initial_x_val = partially_corrected_preds_for_x[:, x.id].clone()

        for b in range(0, right_bounds.shape[-1]):
            preds_with_right_bounds_for_x = partially_corrected_preds_for_x.clone()
            preds_with_right_bounds_for_x[:, x.id] = right_bounds[:, b]

            mask_samples_violating_req_for_bound_b = get_samples_violating_constraints(constraints_at_level_x, preds_with_right_bounds_for_x)
            mask_samples_violating_req.append(mask_samples_violating_req_for_bound_b)

        mask_samples_violating_req = torch.stack(mask_samples_violating_req, dim=1)
        valid_right_bounds = torch.where(~mask_samples_violating_req, right_bounds, torch.inf)
        distance_of_bounds_from_x = torch.abs(valid_right_bounds - initial_x_val.unsqueeze(1))
        mask_bounds_of_minimum_distance = distance_of_bounds_from_x == distance_of_bounds_from_x.amin(dim=1, keepdim=True)

        closest_right_bound_wrt_x = torch.where(mask_bounds_of_minimum_distance, valid_right_bounds, torch.inf).amin(dim=1) # shape Bx1
        return closest_right_bound_wrt_x

get_closest_left_bound_wv 

get_closest_left_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)

Pick the smallest feasible left bound greater than the closest right bound.

Alternative bound-selection variant that first finds the greatest feasible right bound not exceeding x, then returns the smallest left bound strictly above it. Note: this variant does not treat vacuous constraints.

Parameters:

Name Type Description Default
x

The variable to bound.

 required
partially_corrected_preds_for_x

Predictions tensor of shape (B, D).

 required
left_bounds

Candidate left bounds tensor of shape (B, M), or a non-tensor sentinel.

 required
right_bounds

Candidate right bounds tensor of shape (B, M), or a non-tensor sentinel.

 required
constraints_at_level_x

Constraints used to test feasibility of each bound.

 required

Returns:

Type Description

A tensor of shape (B,) (or the left_bounds sentinel) with the

selected left bound per sample.
Source code in pishield/qflra_requirements/correct_predictions.py 
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
def get_closest_left_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x):
    """Pick the smallest feasible left bound greater than the closest right bound.

    Alternative bound-selection variant that first finds the greatest feasible right
    bound not exceeding ``x``, then returns the smallest left bound strictly above
    it. Note: this variant does not treat vacuous constraints.

    Args:
        x: The variable to bound.
        partially_corrected_preds_for_x: Predictions tensor of shape ``(B, D)``.
        left_bounds: Candidate left bounds tensor of shape ``(B, M)``, or a non-tensor
            sentinel.
        right_bounds: Candidate right bounds tensor of shape ``(B, M)``, or a
            non-tensor sentinel.
        constraints_at_level_x: Constraints used to test feasibility of each bound.

    Returns:
        A tensor of shape ``(B,)`` (or the ``left_bounds`` sentinel) with the
        selected left bound per sample.
    """
    # does not treat vacuous constraints!
    initial_x_val = partially_corrected_preds_for_x[:, x.id].clone()

    if type(right_bounds) is not torch.Tensor:
        greatest_right_bound_le_x = right_bounds
    else:

        mask_samples_violating_req = []
        for b in range(0, right_bounds.shape[-1]):
            preds_with_right_bounds_for_x = partially_corrected_preds_for_x.clone()
            preds_with_right_bounds_for_x[:, x.id] = right_bounds[:, b]

            mask_samples_violating_req_for_bound_b = get_samples_violating_constraints(constraints_at_level_x, preds_with_right_bounds_for_x)
            mask_samples_violating_req.append(mask_samples_violating_req_for_bound_b)

        mask_samples_violating_req = torch.stack(mask_samples_violating_req, dim=1)
        greatest_right_bound_le_x = torch.where((right_bounds < initial_x_val.unsqueeze(1)) * ~mask_samples_violating_req, right_bounds, -torch.inf).amax(dim=1)  # shape Bx1

    if type(greatest_right_bound_le_x) is torch.Tensor:
        greatest_right_bound_le_x = greatest_right_bound_le_x.unsqueeze(dim=1)
    smallest_left_bound_gt_r = left_bounds if type(left_bounds) is not torch.Tensor else torch.where(left_bounds > greatest_right_bound_le_x, left_bounds, torch.inf).amin(dim=1)  # shape Bx1
    return smallest_left_bound_gt_r

get_closest_right_bound_wv 

get_closest_right_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)

Pick the greatest feasible right bound less than the closest left bound.

Alternative bound-selection variant that first finds the smallest feasible left bound strictly above x, then returns the greatest right bound below it. Note: this variant does not treat vacuous constraints.

Parameters:

Name Type Description Default
x

The variable to bound.

 required
partially_corrected_preds_for_x

Predictions tensor of shape (B, D).

 required
left_bounds

Candidate left bounds tensor of shape (B, M), or a non-tensor sentinel.

 required
right_bounds

Candidate right bounds tensor of shape (B, M), or a non-tensor sentinel.

 required
constraints_at_level_x

Constraints used to test feasibility of each bound.

 required

Returns:

Type Description

A tensor of shape (B,) (or the right_bounds sentinel) with the

selected right bound per sample.
Source code in pishield/qflra_requirements/correct_predictions.py 
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
def get_closest_right_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x):
    """Pick the greatest feasible right bound less than the closest left bound.

    Alternative bound-selection variant that first finds the smallest feasible left
    bound strictly above ``x``, then returns the greatest right bound below it. Note:
    this variant does not treat vacuous constraints.

    Args:
        x: The variable to bound.
        partially_corrected_preds_for_x: Predictions tensor of shape ``(B, D)``.
        left_bounds: Candidate left bounds tensor of shape ``(B, M)``, or a non-tensor
            sentinel.
        right_bounds: Candidate right bounds tensor of shape ``(B, M)``, or a
            non-tensor sentinel.
        constraints_at_level_x: Constraints used to test feasibility of each bound.

    Returns:
        A tensor of shape ``(B,)`` (or the ``right_bounds`` sentinel) with the
        selected right bound per sample.
    """
    # does not treat vacuous constraints!
    initial_x_val = partially_corrected_preds_for_x[:, x.id].clone()

    if type(left_bounds) is not torch.Tensor:
        smallest_left_bound_gt_x = left_bounds
    else:

        mask_samples_violating_req = []
        for b in range(0, left_bounds.shape[-1]):
            preds_with_left_bounds_for_x = partially_corrected_preds_for_x.clone()
            preds_with_left_bounds_for_x[:, x.id] = left_bounds[:, b]

            mask_samples_violating_req_for_bound_b = get_samples_violating_constraints(constraints_at_level_x, preds_with_left_bounds_for_x)
            mask_samples_violating_req.append(mask_samples_violating_req_for_bound_b)

        mask_samples_violating_req = torch.stack(mask_samples_violating_req, dim=1)
        smallest_left_bound_gt_x = torch.where((left_bounds > initial_x_val.unsqueeze(1)) * ~mask_samples_violating_req, left_bounds, torch.inf).amin(dim=1)  # shape Bx1

    if type(smallest_left_bound_gt_x) is torch.Tensor:
        smallest_left_bound_gt_x = smallest_left_bound_gt_x.unsqueeze(dim=1)
    greatest_right_bound_le_l = right_bounds if type(right_bounds) is not torch.Tensor else torch.where(right_bounds < smallest_left_bound_gt_x, right_bounds, -torch.inf).amax(dim=1)  # shape Bx1
    return greatest_right_bound_le_l

get_closest_left_and_right_bounds 

get_closest_left_and_right_bounds(x: Variable, partially_corrected_preds_for_x: Tensor, constraints_at_level_x: List[Constraint]) -> Tuple[torch.Tensor, torch.Tensor]

Compute the closest feasible left and right bounds for a variable.

Splits the constraints by the sign of x, computes the candidate left and right bounds, then selects the feasible bound closest to x on each side.

Parameters:

Name Type Description Default
x Variable

The variable to bound.

 required
partially_corrected_preds_for_x Tensor

Predictions tensor of shape (B, D).

 required
constraints_at_level_x List[Constraint]

Constraints bounding x at its level.

 required

Returns:

Type Description
Tuple[Tensor, Tensor]

A tuple (closest_left_bound, closest_right_bound) of per-sample bounds.
Source code in pishield/qflra_requirements/correct_predictions.py 
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
def get_closest_left_and_right_bounds(x: Variable, partially_corrected_preds_for_x: torch.Tensor, constraints_at_level_x: List[Constraint]) -> Tuple[torch.Tensor, torch.Tensor]:
    """Compute the closest feasible left and right bounds for a variable.

    Splits the constraints by the sign of ``x``, computes the candidate left and
    right bounds, then selects the feasible bound closest to ``x`` on each side.

    Args:
        x: The variable to bound.
        partially_corrected_preds_for_x: Predictions tensor of shape ``(B, D)``.
        constraints_at_level_x: Constraints bounding ``x`` at its level.

    Returns:
        A tuple ``(closest_left_bound, closest_right_bound)`` of per-sample bounds.
    """
    pos_x_constr, neg_x_constr, pos_neg_x_constr = get_pos_neg_pn_x_constr(x, constraints_at_level_x)
    constr_for_right_bounds = pos_x_constr + pos_neg_x_constr
    constr_for_left_bounds = neg_x_constr + pos_neg_x_constr

    left_bounds = get_left_bounds(x, partially_corrected_preds_for_x, constr_for_left_bounds)  # shape BxM, M is num of constraints
    right_bounds = get_right_bounds(x, partially_corrected_preds_for_x, constr_for_right_bounds) # shape BxM

    # get the closest left boundary
    # closest_left_bound = get_closest_left_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)
    closest_left_bound = get_closest_left_bound(x, partially_corrected_preds_for_x, left_bounds, None, constraints_at_level_x)
    # get the closest right boundary
    # closest_right_bound = get_closest_right_bound_wv(x, partially_corrected_preds_for_x, left_bounds, right_bounds, constraints_at_level_x)
    closest_right_bound = get_closest_right_bound(x, partially_corrected_preds_for_x, None, right_bounds, constraints_at_level_x)

    return closest_left_bound, closest_right_bound

get_closest_bound 

get_closest_bound(x_vals_violating_req: Tensor, left_bounds: Tensor, right_bounds: Tensor) -> torch.Tensor

Snap violating values to whichever of two bounds is nearer.

Parameters:

Name Type Description Default
x_vals_violating_req Tensor

Tensor of current x values that violate constraints.

 required
left_bounds Tensor

Per-sample left bound candidates.

 required
right_bounds Tensor

Per-sample right bound candidates.

 required

Returns:

Type Description
Tensor

A tensor with each value replaced by the closer of its left or right bound.
Source code in pishield/qflra_requirements/correct_predictions.py 
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
def get_closest_bound(x_vals_violating_req: torch.Tensor, left_bounds: torch.Tensor, right_bounds: torch.Tensor) -> torch.Tensor:
    """Snap violating values to whichever of two bounds is nearer.

    Args:
        x_vals_violating_req: Tensor of current ``x`` values that violate constraints.
        left_bounds: Per-sample left bound candidates.
        right_bounds: Per-sample right bound candidates.

    Returns:
        A tensor with each value replaced by the closer of its left or right bound.
    """
    # METHOD 1
    dist_from_right = torch.abs(x_vals_violating_req - right_bounds)
    dist_from_left = torch.abs(x_vals_violating_req - left_bounds)
    mask_right_smaller_than_left_dist = dist_from_right < dist_from_left
    corrected_x_vals = torch.where(mask_right_smaller_than_left_dist, right_bounds, left_bounds)

    # METHOD 2
    # corrected_x_vals = torch.min(x_vals_violating_req - right_bounds, left_bounds - x_vals_violating_req)
    return corrected_x_vals

compute_DRL 

compute_DRL(x: Variable, partially_corrected_preds: Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor

Correct a variable against disjunctive constraints.

Identifies samples violating the (disjunctive) constraints at x's level and moves only those values to the nearest feasible bound, leaving satisfying samples unchanged.

Parameters:

Name Type Description Default
x Variable

The variable being corrected.

 required
partially_corrected_preds Tensor

Predictions tensor of shape (B, D) including corrections to previously processed variables.

 required
constraints_at_level_x List[Constraint]

Constraints bounding x at its level (at least one of which is disjunctive).

 required

Returns:

Type Description
Tensor

A tensor of shape (B,) with the corrected values of x.
Source code in pishield/qflra_requirements/correct_predictions.py 
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
def compute_DRL(x: Variable, partially_corrected_preds: torch.Tensor, constraints_at_level_x: List[Constraint]) -> torch.Tensor:
    """Correct a variable against disjunctive constraints.

    Identifies samples violating the (disjunctive) constraints at ``x``'s level and
    moves only those values to the nearest feasible bound, leaving satisfying samples
    unchanged.

    Args:
        x: The variable being corrected.
        partially_corrected_preds: Predictions tensor of shape ``(B, D)`` including
            corrections to previously processed variables.
        constraints_at_level_x: Constraints bounding ``x`` at its level (at least one
            of which is disjunctive).

    Returns:
        A tensor of shape ``(B,)`` with the corrected values of ``x``.
    """
    # the partially_corrected_preds should contain the corrections made at the prev analysed vars!

    x_id = x.id
    initial_x_val = partially_corrected_preds[:, x_id].clone()

    # STEP 1
    # check if the partially_corrected_preds satisfy the requirements
    mask_samples_violating_req = get_samples_violating_constraints(constraints_at_level_x, partially_corrected_preds)
    if not mask_samples_violating_req.any():
        return initial_x_val
    partially_corrected_preds_for_wrong_x = partially_corrected_preds[mask_samples_violating_req]
    x_vals_violating_req = initial_x_val.clone()[mask_samples_violating_req]
    # x_vals_sat_req = initial_x_val.clone()[~mask_samples_violating_req]

    # correct x where the constraints are violated
    # compute right and left bounds
    closest_left_bounds, closest_right_bounds = get_closest_left_and_right_bounds(x, partially_corrected_preds_for_wrong_x, constraints_at_level_x)
    corrected_x_vals = get_closest_bound(x_vals_violating_req, closest_left_bounds, closest_right_bounds)

    # refill initial_x_val where values violate the constr with the corrected values
    initial_x_val[mask_samples_violating_req] = corrected_x_vals

    return initial_x_val

correct_preds 

correct_preds(preds: Tensor, ordering: List[Variable], sets_of_constr: {Variable: List[Constraint]})

Correct predictions so they satisfy all QFLRA requirements.

Processes the variables in the given ordering, correcting each variable into the feasible region implied by its constraint set given the already-corrected values of the earlier variables. Purely conjunctive levels are handled by simple interval clipping; levels with disjunctions are handled by :func:compute_DRL. Infinite corrected values are replaced by a large finite sentinel.

Parameters:

Name Type Description Default
preds Tensor

Predictions tensor of shape (B, D) (one column per variable).

 required
ordering List[Variable]

The variable ordering driving the correction sweep.

 required
sets_of_constr {Variable: List[Constraint]}

Mapping from each :class:Variable to its constraint set, as produced by :func:compute_sets_of_constraints.

 required

Returns:

Type Description

A tensor of shape (B, D) with predictions corrected to satisfy the

constraints.
Example

sets_of_constr = compute_sets_of_constraints(ordering, constraints, verbose=False) corrected = correct_preds(preds, ordering, sets_of_constr)

Source code in pishield/qflra_requirements/correct_predictions.py 
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
def correct_preds(preds: torch.Tensor, ordering: List[Variable], sets_of_constr: {Variable: List[Constraint]}):
    """Correct predictions so they satisfy all QFLRA requirements.

    Processes the variables in the given ``ordering``, correcting each variable into
    the feasible region implied by its constraint set given the already-corrected
    values of the earlier variables. Purely conjunctive levels are handled by simple
    interval clipping; levels with disjunctions are handled by :func:`compute_DRL`.
    Infinite corrected values are replaced by a large finite sentinel.

    Args:
        preds: Predictions tensor of shape ``(B, D)`` (one column per variable).
        ordering: The variable ordering driving the correction sweep.
        sets_of_constr: Mapping from each :class:`Variable` to its constraint set, as
            produced by :func:`compute_sets_of_constraints`.

    Returns:
        A tensor of shape ``(B, D)`` with predictions corrected to satisfy the
        constraints.

    Example:
        >>> sets_of_constr = compute_sets_of_constraints(ordering, constraints, verbose=False)
        >>> corrected = correct_preds(preds, ordering, sets_of_constr)
    """
    # given a NN's preds [h1, h2, .., hn],
    # an ordering of the n variables and
    # a set of constraints computed at each variable w.r.t. descending order of the provided ordering
    # correct the preds according to the constraints in ascending order w.r.t. provided ordering
    corrected_preds = preds.clone()

    for x in ordering:
        pos = x.id
        x_constr = get_constr_at_level_x(x, sets_of_constr)
        if len(x_constr) == 0:
            continue

        if not any_disjunctions_in_constraint_set(x_constr):
            # print(x.id, [e.readable() for e in x_constr], 'KKKK')  # .readable()],'@@@')
            pos_x_constr, neg_x_constr, pos_neg_x_constr = get_pos_neg_pn_x_constr(x, x_constr)

            constr_for_lbs = pos_x_constr + pos_neg_x_constr
            constr_for_ubs = neg_x_constr + pos_neg_x_constr

            lower_bounds = get_lower_bounds(x, constr_for_lbs, preds)
            greatest_lbs = lower_bounds if type(lower_bounds) is not torch.Tensor else lower_bounds.amax(dim=1)

            upper_bounds = get_upper_bounds(x, constr_for_ubs, preds)
            least_ubs = upper_bounds if type(upper_bounds) is not torch.Tensor else upper_bounds.amin(dim=1)

            # print('pos', [e.readable() for e in pos_x_constr], preds[pos], pos_x_corrected)
            # print('neg', [e.readable() for e in neg_x_constr], preds[pos], neg_x_corrected)

            corrected_preds[:,pos] = get_final_x_correction(preds[:, pos], greatest_lbs, least_ubs)

        else:
            corrected_preds[:,pos] = compute_DRL(x, preds, x_constr)

        preds = corrected_preds.clone()
        corrected_preds = preds.clone()

    corrected_preds = torch.where(corrected_preds == torch.inf, INFINITY_NP, corrected_preds)
    corrected_preds = torch.where(corrected_preds == -torch.inf, -INFINITY_NP, corrected_preds)

    return corrected_preds

check_all_constraints_sat 

check_all_constraints_sat(corrected_preds, constraints, error_raise=True)

Check that corrected predictions satisfy every constraint.

Parameters:

Name Type Description Default
corrected_preds

The corrected predictions tensor.

 required
constraints

The constraints to verify.

 required
error_raise

If True, raise an exception on the first violated constraint instead of merely flagging it.

 True

Returns:

Type Description

True if all constraints are satisfied, False otherwise (when

error_raise is False).

Raises:

Type Description
Exception

If error_raise is True and a constraint is violated.
Source code in pishield/qflra_requirements/correct_predictions.py 
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
def check_all_constraints_sat(corrected_preds, constraints, error_raise=True):
    """Check that corrected predictions satisfy every constraint.

    Args:
        corrected_preds: The corrected predictions tensor.
        constraints: The constraints to verify.
        error_raise: If ``True``, raise an exception on the first violated
            constraint instead of merely flagging it.

    Returns:
        ``True`` if all constraints are satisfied, ``False`` otherwise (when
        ``error_raise`` is ``False``).

    Raises:
        Exception: If ``error_raise`` is ``True`` and a constraint is violated.
    """
    all_sat_after_correction = True
    for constr in constraints:
        sat = constr.check_satisfaction(corrected_preds)
        if not sat:
            all_sat_after_correction = False
            if error_raise:
                constr: Constraint
                batched_sat_results = constr.disjunctive_inequality.check_satisfaction(corrected_preds)
                samples_violating_constr = corrected_preds[~batched_sat_results]
                raise Exception('Not satisfied!', constr.readable(), samples_violating_constr[0][3], samples_violating_constr[0][10], samples_violating_constr[0][11])
    return all_sat_after_correction

example_predictions_custom 

example_predictions_custom()

Build a small example batch of predictions for demonstration.

Returns:

Type Description

A tensor of shape (2, 2) with two hand-crafted prediction samples.
Source code in pishield/qflra_requirements/correct_predictions.py 
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
def example_predictions_custom():
    """Build a small example batch of predictions for demonstration.

    Returns:
        A tensor of shape ``(2, 2)`` with two hand-crafted prediction samples.
    """
    y_0= -2
    y_1 = 2
    p1 = torch.tensor(eval('['+','.join(['y_'+str(i) for i in range(2)])+']')).unsqueeze(0)   # constraints_disj1: Corrected predictions tensor([-10.,  10.,  -2.,   3.,   1.,   2.,  -1.], grad_fn=<CopySlices>) True

    y_0 = 2
    y_1 = -2.
    p2 = torch.tensor(eval('['+','.join(['y_'+str(i) for i in range(2)])+']')).unsqueeze(0)

    predictions = torch.cat([p1,p2],dim=0)
    return predictions

main 

main()

Run an end-to-end demo: parse constraints, correct example preds, report.

Source code in pishield/qflra_requirements/correct_predictions.py 
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
def main():
    """Run an end-to-end demo: parse constraints, correct example preds, report."""
    # ordering, constraints = parse_constraints_file('../data/constraints_disj1.txt')
    # ordering, constraints = parse_constraints_file('../data/url_constraints.txt')
    # ordering, constraints = parse_constraints_file('../data/lcld/lcld_constraints.txt')
    ordering, constraints = parse_constraints_file('../custom_constr.txt')

    # set ordering to random
    ordering = set_random_ordering(ordering)

    print('verbose constr')
    for constr in constraints:
        print(constr.verbose_readable())

    print('compute sets of constraints')
    sets_of_constr = compute_sets_of_constraints(ordering, constraints, verbose=True)

    # preds = example_predictions()
    # preds = example_predictions_lcld()
    preds = example_predictions_custom()
    print('\n\nPreds', preds)

    preds.requires_grad = True
    t1 = time.time()
    corrected_preds = correct_preds(preds, ordering, sets_of_constr)
    print('Original predictions', preds[0])

    print('Corrected predictions', corrected_preds[0], corrected_preds.requires_grad)

    check_all_constraints_are_sat(constraints, preds, corrected_preds)

    print('Time to correct preds', time.time() - t1)

    compute_sat_stats(preds, constraints, mask_out_missing_values=True)
    print(corrected_preds, 'corrected')

Feature orderings

feature_orderings

Selection of the variable ordering used to correct predictions.

The ordering determines the sequence in which variables are corrected by the Shield Layer; it can be taken as given or randomised.

set_random_ordering 

set_random_ordering(ordering: List[Variable])

Shuffle a variable ordering in place.

Parameters:

Name Type Description Default
ordering List[Variable]

List of :class:Variable objects to shuffle.

 required

Returns:

Type Description

The same list, shuffled in place.
Source code in pishield/qflra_requirements/feature_orderings.py 
15
16
17
18
19
20
21
22
23
24
25
def set_random_ordering(ordering: List[Variable]):
    """Shuffle a variable ordering in place.

    Args:
        ordering: List of :class:`Variable` objects to shuffle.

    Returns:
        The same list, shuffled in place.
    """
    random.shuffle(ordering) # in-place shuffling
    return ordering

set_ordering 

set_ordering(ordering: List[Variable], label_ordering_choice: str)

Select a variable ordering according to a choice string.

Parameters:

Name Type Description Default
ordering List[Variable]

The base list of :class:Variable objects.

 required
label_ordering_choice str

Either 'random' (shuffle the ordering) or 'given' (keep the provided ordering).

 required

Returns:

Type Description

The chosen ordering as a list of :class:Variable objects.
Source code in pishield/qflra_requirements/feature_orderings.py 
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
def set_ordering(ordering: List[Variable], label_ordering_choice: str):
    """Select a variable ordering according to a choice string.

    Args:
        ordering: The base list of :class:`Variable` objects.
        label_ordering_choice: Either ``'random'`` (shuffle the ordering) or
            ``'given'`` (keep the provided ordering).

    Returns:
        The chosen ordering as a list of :class:`Variable` objects.
    """
    if label_ordering_choice == 'random':
        ordering = set_random_ordering(ordering)
        return ordering
    elif label_ordering_choice == 'given':
        return ordering

# def set_ordering(use_case, ordering: List[Variable] | List[str], label_ordering_choice: str, model_type: str, data_partition='test'):
#     if label_ordering_choice == 'random':
#         ordering = set_random_ordering(ordering)
#     elif label_ordering_choice == 'predefined':
#         ordering = list(map(lambda x: Variable(x), ordering.split()))
#     else:
#         json_filename = f'feature_ordering/feature_orderings.json'
#         with open(json_filename, "r") as f:
#             data = json.load(f)
#
#         if label_ordering_choice == 'causal':
#             ordering = data["feature_orderings"][use_case]['general'][label_ordering_choice]['train']
#             ordering = list(map(lambda x: Variable(x), ordering.split()))
#         else:
#             model_type = model_type.lower()
#             ordering = data["feature_orderings"][use_case][model_type][label_ordering_choice][data_partition]
#             ordering = list(map(lambda x: Variable(x), ordering.split()))

    readable_ordering = [e.readable() for e in ordering]
    print(f'Using *{label_ordering_choice}* feature ordering:\n', readable_ordering, 'len:', len(readable_ordering))
    return ordering

Atom utilities

utils_atoms

Helper functions for manipulating lists of linear inequality atoms.

These utilities merge, scale and negate the :class:Atom objects that make up the body (left-hand side) of QFLRA inequalities.

collapse_atoms 

collapse_atoms(atom_list)

Merge duplicated atoms that refer to the same variable.

Atoms that share a variable are combined by summing their signed coefficients. Any atom whose coefficients cancel out (resulting coefficient of zero) is dropped.

Parameters:

Name Type Description Default
atom_list

List of :class:Atom objects, possibly with several atoms per variable.

 required

Returns:

Type Description

A list of :class:Atom objects with at most one atom per variable.
Source code in pishield/qflra_requirements/utils_atoms.py 
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
def collapse_atoms(atom_list):
    """Merge duplicated atoms that refer to the same variable.

    Atoms that share a variable are combined by summing their signed coefficients.
    Any atom whose coefficients cancel out (resulting coefficient of zero) is dropped.

    Args:
        atom_list: List of :class:`Atom` objects, possibly with several atoms per
            variable.

    Returns:
        A list of :class:`Atom` objects with at most one atom per variable.
    """
    # merge any duplicated atoms in a atom list
    merged_atoms = {}
    merged_atoms: {int: Atom}
    for atom in atom_list:
        var = atom.variable.id
        if var not in merged_atoms.keys():
            merged_atoms[var] = atom
        else:
            variable, coefficient, positive_sign = merged_atoms[var].get_atom_attributes()
            existing_coeff = coefficient if positive_sign else -coefficient
            current_coeff = atom.coefficient if atom.positive_sign else -atom.coefficient
            new_coefficient = existing_coeff + current_coeff
            if new_coefficient != 0:
                new_atom = Atom(variable, float(np.abs(new_coefficient)), True if new_coefficient > 0 else False)
                merged_atoms[var] = new_atom
    return list(merged_atoms.values())

multiply_coefficients_of_atoms 

multiply_coefficients_of_atoms(atoms: List[Atom], coeff: float)

Scale every atom's coefficient by a constant factor.

Parameters:

Name Type Description Default
atoms List[Atom]

List of :class:Atom objects to scale.

 required
coeff float

Multiplicative factor applied to each atom's coefficient.

 required

Returns:

Type Description

A new list of :class:Atom objects with scaled coefficients (the signs are

preserved).
Source code in pishield/qflra_requirements/utils_atoms.py 
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
def multiply_coefficients_of_atoms(atoms: List[Atom], coeff: float):
    """Scale every atom's coefficient by a constant factor.

    Args:
        atoms: List of :class:`Atom` objects to scale.
        coeff: Multiplicative factor applied to each atom's coefficient.

    Returns:
        A new list of :class:`Atom` objects with scaled coefficients (the signs are
        preserved).
    """
    new_atoms = []
    for atom in atoms:
        variable, coefficient, positive_sign = atom.get_atom_attributes()
        new_atom = Atom(variable, coefficient*coeff, positive_sign)
        new_atoms.append(new_atom)
    return new_atoms

negate_atoms 

negate_atoms(atoms: List[Atom])

Flip the sign of every atom in a list.

Parameters:

Name Type Description Default
atoms List[Atom]

List of :class:Atom objects to negate.

 required

Returns:

Type Description

A new list of :class:Atom objects with each positive sign toggled.
Source code in pishield/qflra_requirements/utils_atoms.py 
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
def negate_atoms(atoms: List[Atom]):
    """Flip the sign of every atom in a list.

    Args:
        atoms: List of :class:`Atom` objects to negate.

    Returns:
        A new list of :class:`Atom` objects with each positive sign toggled.
    """
    new_atoms = []
    for atom in atoms:
        variable, coefficient, positive_sign = atom.get_atom_attributes()
        new_atom = Atom(variable, coefficient, not positive_sign)
        new_atoms.append(new_atom)
    return new_atoms

Function utilities

utils_functions

Evaluation and statistics helpers for QFLRA constraints.

Functions here evaluate inequality atoms on batched predictions, detect missing values and disjunctions, and report constraint-satisfaction statistics.

eval_atoms_list 

eval_atoms_list(atoms_list: List[Atom], preds: Tensor, reduction='sum')

Evaluate a list of atoms on batched predictions and reduce them.

Each atom is evaluated at the predicted value of its variable, then the per-atom results are combined according to reduction.

Parameters:

Name Type Description Default
atoms_list List[Atom]

The :class:Atom objects forming an inequality body.

 required
preds Tensor

Predictions tensor of shape (B, D); column id holds the value of the variable with that id.

 required
reduction

How to combine atoms across the body. Only 'sum' is supported.

 'sum'

Returns:

Type Description

A tensor of shape (B,) with the reduced body value per sample; an

all-zero tensor if atoms_list is empty.

Raises:

Type Description
Exception

If reduction is not 'sum'.
Source code in pishield/qflra_requirements/utils_functions.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
def eval_atoms_list(atoms_list: List['Atom'], preds: torch.Tensor, reduction='sum'):
    """Evaluate a list of atoms on batched predictions and reduce them.

    Each atom is evaluated at the predicted value of its variable, then the
    per-atom results are combined according to ``reduction``.

    Args:
        atoms_list: The :class:`Atom` objects forming an inequality body.
        preds: Predictions tensor of shape ``(B, D)``; column ``id`` holds the value
            of the variable with that id.
        reduction: How to combine atoms across the body. Only ``'sum'`` is supported.

    Returns:
        A tensor of shape ``(B,)`` with the reduced body value per sample; an
        all-zero tensor if ``atoms_list`` is empty.

    Raises:
        Exception: If ``reduction`` is not ``'sum'``.
    """
    evaluated_atoms = []
    for atom in atoms_list:
        atom_value = preds[:, atom.variable.id]
        evaluated_atoms.append(atom.eval(atom_value))

    if evaluated_atoms == []:
        return torch.zeros(preds.shape[0])

    evaluated_atoms = torch.stack(evaluated_atoms, dim=1)
    if reduction == 'sum':
        result = evaluated_atoms.sum(dim=1)
    else:
        raise Exception(f'{reduction} reduction not implemented!')
    return result

any_disjunctions_in_constraint_set 

any_disjunctions_in_constraint_set(constraints: List[Constraint])

Report whether any constraint is a disjunction of inequalities.

Parameters:

Name Type Description Default
constraints List[Constraint]

The constraints to inspect.

 required

Returns:

Type Description

True if at least one constraint has more than one inequality (i.e. an

'or'), False otherwise.
Source code in pishield/qflra_requirements/utils_functions.py 
56
57
58
59
60
61
62
63
64
65
66
67
68
69
def any_disjunctions_in_constraint_set(constraints: List['Constraint']):
    """Report whether any constraint is a disjunction of inequalities.

    Args:
        constraints: The constraints to inspect.

    Returns:
        ``True`` if at least one constraint has more than one inequality (i.e. an
        'or'), ``False`` otherwise.
    """
    for constraint in constraints:
        if len(constraint.list_inequalities) > 1:
            return True
    return False

get_missing_mask 

get_missing_mask(ineq_atoms: List[Atom], preds: Tensor)

Identify samples whose involved variable values indicate missing data.

A sample is flagged as missing when the product of the raw values of the relevant variables falls below -TOLERANCE (the convention used to encode missing values in this codebase).

Parameters:

Name Type Description Default
ineq_atoms List[Atom]

Atoms (or list of atom lists) whose variables are checked.

 required
preds Tensor

Predictions tensor of shape (B, D).

 required

Returns:

Type Description

A boolean tensor of shape (B,) that is True for samples with missing

values.
Source code in pishield/qflra_requirements/utils_functions.py 
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
def get_missing_mask(ineq_atoms: List['Atom'], preds: torch.Tensor):
    """Identify samples whose involved variable values indicate missing data.

    A sample is flagged as missing when the product of the raw values of the
    relevant variables falls below ``-TOLERANCE`` (the convention used to encode
    missing values in this codebase).

    Args:
        ineq_atoms: Atoms (or list of atom lists) whose variables are checked.
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        A boolean tensor of shape ``(B,)`` that is ``True`` for samples with missing
        values.
    """
    raw_variable_values = []
    if type(ineq_atoms[0]) != list:
        ineq_atoms = [ineq_atoms]
    for atoms_list in ineq_atoms:
        for atom in atoms_list:
            raw_variable_values.append(preds[:, atom.variable.id])

    raw_variable_values = torch.stack(raw_variable_values, dim=1)
    missing_values_mask = raw_variable_values.prod(dim=1) < -classes.TOLERANCE
    return missing_values_mask

split_constr_atoms 

split_constr_atoms(y: Variable, constr: Constraint)

Separate the atom of a variable from the rest of a constraint body.

Parameters:

Name Type Description Default
y Variable

The variable to extract.

 required
constr Constraint

The constraint whose body atoms are split.

 required

Returns:

Type Description

A tuple (red_coefficient, complementary_atoms) where red_coefficient

is the (positive) coefficient of y and complementary_atoms are the

remaining body atoms.
Source code in pishield/qflra_requirements/utils_functions.py 
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
def split_constr_atoms(y: 'Variable', constr: 'Constraint'):
    """Separate the atom of a variable from the rest of a constraint body.

    Args:
        y: The variable to extract.
        constr: The constraint whose body atoms are split.

    Returns:
        A tuple ``(red_coefficient, complementary_atoms)`` where ``red_coefficient``
        is the (positive) coefficient of ``y`` and ``complementary_atoms`` are the
        remaining body atoms.
    """
    complementary_atoms = []
    for atom in constr.get_body_atoms():
        if atom.variable.id == y.id:
            red_coefficient = atom.coefficient  # note this is a positive real constant
        else:
            complementary_atoms.append(atom)
    return red_coefficient, complementary_atoms

get_samples_violating_constraints 

get_samples_violating_constraints(constraints, preds)

Flag samples that violate at least one constraint.

Parameters:

Name Type Description Default
constraints

The constraints to check.

 required
preds

Predictions tensor of shape (B, D).

 required

Returns:

Type Description

A boolean tensor of shape (B,) that is True for samples violating any

constraint.
Source code in pishield/qflra_requirements/utils_functions.py 
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
def get_samples_violating_constraints(constraints, preds):
    """Flag samples that violate at least one constraint.

    Args:
        constraints: The constraints to check.
        preds: Predictions tensor of shape ``(B, D)``.

    Returns:
        A boolean tensor of shape ``(B,)`` that is ``True`` for samples violating any
        constraint.
    """
    samples_violating_req = []
    for constr in constraints:
        samples_sat_req = constr.disjunctive_inequality.check_satisfaction(preds)  # shape Bx1
        samples_violating_req.append(~samples_sat_req)

    samples_violating_req = torch.stack(samples_violating_req, dim=1)
    mask_samples_violating_req = samples_violating_req.any(dim=1)
    return mask_samples_violating_req

check_all_constraints_are_sat 

check_all_constraints_are_sat(constraints, preds, corrected_preds)

Print which constraints are violated before and after correction.

Parameters:

Name Type Description Default
constraints

The constraints to check.

 required
preds

The original predictions tensor.

 required
corrected_preds

The predictions after correction.

 required

Returns:

Type Description

True if all constraints are satisfied by corrected_preds, False

otherwise.
Source code in pishield/qflra_requirements/utils_functions.py 
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
def check_all_constraints_are_sat(constraints, preds, corrected_preds):
    """Print which constraints are violated before and after correction.

    Args:
        constraints: The constraints to check.
        preds: The original predictions tensor.
        corrected_preds: The predictions after correction.

    Returns:
        ``True`` if all constraints are satisfied by ``corrected_preds``, ``False``
        otherwise.
    """
    # print('sat req?:')
    for constr in constraints:
        sat = constr.check_satisfaction(preds)
        if not sat:
            print('Not satisfied!', constr.readable())

    # print('*' * 80)
    all_sat_after_correction = True
    for constr in constraints:
        sat = constr.check_satisfaction(corrected_preds)
        if not sat:
            all_sat_after_correction = False
            print('Not satisfied!', constr.readable())
    if all_sat_after_correction:
        print('All constraints are satisfied after correction!')
    else:
        print('There are still constraint violations!!!')
    return all_sat_after_correction

compute_sat_stats 

compute_sat_stats(real_data, constraints, mask_out_missing_values=False)

Compute per-constraint and overall constraint-satisfaction statistics.

Parameters:

Name Type Description Default
real_data

Tensor of data/predictions of shape (B, D).

 required
constraints

The constraints to evaluate.

 required
mask_out_missing_values

If True, samples flagged as missing (see :func:get_missing_mask) are excluded from the satisfaction rates.

 False

Returns:

Type Description

A tuple (sat_rate_per_constr, percentage_of_samples_violating_constraints)

of pandas DataFrames: per-constraint satisfaction rates (as percentages) and

the overall percentage of samples violating constraints.
Source code in pishield/qflra_requirements/utils_functions.py 
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
def compute_sat_stats(real_data, constraints, mask_out_missing_values=False):
    """Compute per-constraint and overall constraint-satisfaction statistics.

    Args:
        real_data: Tensor of data/predictions of shape ``(B, D)``.
        constraints: The constraints to evaluate.
        mask_out_missing_values: If ``True``, samples flagged as missing (see
            :func:`get_missing_mask`) are excluded from the satisfaction rates.

    Returns:
        A tuple ``(sat_rate_per_constr, percentage_of_samples_violating_constraints)``
        of pandas DataFrames: per-constraint satisfaction rates (as percentages) and
        the overall percentage of samples violating constraints.
    """
    real_data = pd.DataFrame(real_data.detach().numpy())
    sat_rate_per_constr = {i: [] for i in range(len(constraints))}
    percentage_of_samples_sat_constraints = []

    samples_sat_constr = torch.ones(real_data.shape[0]) == 1.
    # real_data = real_data.iloc[:, :-1].to_numpy()
    real_data = torch.tensor(real_data.to_numpy())

    for j, constr in enumerate(constraints):
        sat_per_datapoint = constr.disjunctive_inequality.check_satisfaction(real_data)
        if mask_out_missing_values:
            missing_values_mask = get_missing_mask(constr.disjunctive_inequality.body, real_data)
        else:
            missing_values_mask = torch.ones(real_data.shape[0]) == 0.
        sat_per_datapoint[missing_values_mask] = True
        sat_rate = sat_per_datapoint[~missing_values_mask].sum() / (~missing_values_mask).sum()
        # print('Real sat_rate is', sat_rate, sat_per_datapoint.sum(), len(sat_per_datapoint), sat_per_datapoint)
        sat_rate_per_constr[j].append(sat_rate)
        # sat_rate_per_constr[j].append(sat_per_datapoint.sum() / len(sat_per_datapoint))
        samples_sat_constr = samples_sat_constr & sat_per_datapoint

    percentage_of_samples_sat_constraints.append(sum(samples_sat_constr) / len(samples_sat_constr))
    sat_rate_per_constr = {i: [sum(sat_rate_per_constr[i]) / len(sat_rate_per_constr[i]) * 100.0] for i in
                           range(len(constraints))}
    percentage_of_samples_violating_constraints = 100.0 - sum(percentage_of_samples_sat_constraints) / len(
        percentage_of_samples_sat_constraints) * 100.0
    print('REAL', 'sat_rate_per_constr', sat_rate_per_constr)
    print('REAL', 'percentage_of_samples_violating_constraints', percentage_of_samples_violating_constraints)

    sat_rate_per_constr = pd.DataFrame(sat_rate_per_constr, columns=list(range(len(constraints))))

    percentage_of_samples_violating_constraints = pd.DataFrame(
        {'real_percentage_of_samples_violating_constraints': [percentage_of_samples_violating_constraints]},
        columns=['real_percentage_of_samples_violating_constraints'])

    return sat_rate_per_constr, percentage_of_samples_violating_constraints