Method try_from

src/analysis/numerical/linear_constraint.rs:429–555

(value: Rc<SymbolicValue>)

impl TryFrom<Rc<SymbolicValue>> for LinearConstraintSystem {
    type Error = &'static str;
    fn try_from(value: Rc<SymbolicValue>) -> Result<Self, &'static str> {
        debug!(
            "Converting symbolic value into LinearConstraintSystem: {:?}",
            value
        );

        let res =
            match &value.expression {
                Expression::And { left, right } => {
                    let lcsts = LinearConstraintSystem::try_from(left.clone());
                    let rcsts = LinearConstraintSystem::try_from(right.clone());
                    if let (Ok(lcsts), Ok(rcsts)) = (lcsts, rcsts) {
                        lcsts.join(rcsts)
                    } else {
                        return Err("Error when converting And expression");
                    }
                }
                // Constant, so it must be either true or false
                Expression::CompileTimeConstant(const_value) => {
                    match const_value.as_bool_if_known() {
                    Some(true) => LinearConstraint::new_true().into(),
                    Some(false) => LinearConstraint::new_false().into(),
                    None => unreachable!("Converting a constant symbolic value into linear constraint but the value is neither true nor false"),
                }
                }
                // A single variable, equivalent to `var == true`
                Expression::Variable { path, .. } => {
                    let mut expr = LinearExpression::default();
                    expr = expr + path.clone() - Integer::from(1);
                    LinearConstraint::Equality(expr).into()
                }
                // A single numerical variable, equivalent to `var == true`
                Expression::Numerical(path) => {
                    let mut expr = LinearExpression::default();
                    expr = expr + path.clone() - Integer::from(1);
                    LinearConstraint::Equality(expr).into()
                }
                Expression::Widen { operand, .. } => {
                    Self::try_from(operand.clone()).unwrap().into()
                }
                // An expression `lhs <= rhs`, equivalent to `lhs - rhs <= 0`
                Expression::LessOrEqual { left, right } => {
                    let left_expr = symbolic_to_expression(left.clone());
                    let right_expr = symbolic_to_expression(right.clone());
                    if let (Ok(left_expr), Ok(right_expr)) = (left_expr, right_expr) {
                        LinearConstraint::LessEq(left_expr - right_expr).into()
                    } else {
                        return Err("Error when converting LessOrEqual expression");
                    }
                }
                // An expression `lhs < rhs`, equivalent to `lhs - rhs < 0`
                Expression::LessThan { left, right } => {
                    let left_expr = symbolic_to_expression(left.clone());
                    let right_expr = symbolic_to_expression(right.clone());
                    if let (Ok(left_expr), Ok(right_expr)) = (left_expr, right_expr) {
                        LinearConstraint::LessThan(left_expr - right_expr).into()
                    } else {
                        return Err("Error when converting LessThan expression");