Module classify_into_lia 

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

The conversion generally works as described in ../general_to_lia.rs.

This module implements the logic that after successfully splitting the expression into pairs of atoms and rational factors, brings all variables to the left and collects all parameter factor pairs and constants on the right.

Then the module converts them into the appropriate LIAVariableConstraint type, i.e., either a SingleAtomConstraint, SumAtomConstraint or ComparisonConstraint.

Functions

canonicalize_comp_op 🔒

Translate the constraints into constraints over the canonical thresholds

combine_pair_iterators 🔒

Combine two iterators over pairs of tuples over (T, Fraction) into a single map from T to Fraction, where all entries from negated_it are inserted negated

parse_guard_type 🔒

split_pairs_into_atom_and_threshold 🔒

This function is designed to rewrite an comparison expression into a form where the returned HashMap<T, Fraction> forms the new lhs of the equation and the returned threshold is the right hand side of the equation