Module general_to_lia 

Logic to try to convert a GeneralThresholdAutomaton into a LIAThresholdAutomaton.

This module contains the logic to transform a GeneralThresholdAutomaton into a LIAThresholdAutomaton, i.e., into a threshold automaton where all expressions are in linear arithmetic.

The transformation works in the following way:

First boolean negations are removed by pushing them inwards. This logic can be found in the remove_boolean_neg module. This step converts BooleanExpression into remove_boolean_neg::NonNegatedBooleanExpression.

Next, the integer expressions in the boolean expressions are transformed. First, any subtractions are removed by transforming them into additions with a negative number or by adding a factor -1. This logic can be found in the remove_minus module. This step converts IntegerExpressions into NonMinusIntegerExpr.

Next, divisions are removed by transforming them into multiplications with rational factors. This is the first incomplete step, as this is only possible if there are no atoms appearing in a divisor. This logic can be found in the remove_div module. This step converts NonMinusIntegerExpr into NonDivIntegerExpr.

If all expressions could be transformed we can now transform integer expressions into weighted sums, with rational factors. This is the form assumed by many papers in the formal definition of threshold automata. This is done in the module split_pairs.

The final step in processing integer expressions is to bring all variables to the left side of the equation, and then classify them into the 3 LIAGuard types. This logic can be found in the classify_into_lia module.

Afterwards, the guards can finally be assembled back into the LIAVariableConstraint type, which is a boolean combination of the 3 guard types.

Modules

classify_into_lia 🔒

This module contains the logic to transform a general boolean expression over variables into a super::LIAVariableConstraint.

remove_boolean_neg 🔒

Logic to remove boolean negations from an expression

remove_div 🔒

Module for removing divisions by replacing them with multiplications by fractions.

remove_minus 🔒

Remove unary negations and subtractions from integer expressions

split_pair 🔒

This module contains the logic to split an integer expression into pairs of factors and an atom / parameter or constant.