vj-sim 0.3.0

//! `unique` constraints for the [`Builder`] (plan task C10; IEEE 1800-2023
//! 18.5.4).
//!
//! `unique { a, b, c[2:3] }` constrains every member of the group to a value no
//! other member has. Each member is a singular integral variable or an
//! unpacked-array variable or slice; an array contributes its *leaf* elements,
//! walked outermost dimension first in the array's declared index order, so
//! the group is a flat list of scalars. The group becomes one
//! [`Expr::AllDistinct`] conjunct over that list.
//!
//! * "If a `unique` constraint is applied to a single item or to a slice with
//!   one member, the constraint shall have no effect and shall not cause a
//!   constraint contradiction": a group of fewer than two members adds
//!   nothing. Two members that are one variable (`unique { x, x }`) are two
//!   members, so that group is unsatisfiable.
//! * Members must be of equivalent type (6.22.1; checked by slang's own
//!   predicate, and by IR type as defence in depth) and no `randc` variable
//!   may appear: both are [`BuildError::BadUnique`], as is anything that is
//!   not a variable (an expression, a constant, a bit- or part-select).
//! * A non-`rand` member is a state variable: a constant of the group, so the
//!   random members avoid its value (18.3).
//! * A `real` member needs a pairwise-distinct constraint in the real-domain
//!   solver, which has none: [`BuildError::RealConstraint`], by name.
//! * An element of a `rand` fixed-size array property (or of an array member
//!   of a struct property) is an IR variable declared by
//!   [`Builder::declare_rand_aggregate`] (`super::aggregate`); a non-`rand`
//!   one is a state variable. A random element nobody declared is
//!   [`BuildError::Unsupported`] naming it. A whole dynamic array or queue is a member too (its
//!   length is known only at run time): the group becomes one
//!   [`ArrayNode::Distinct`], expanded to an [`Expr::AllDistinct`] over the
//!   elements once the sizes are chosen. Selects of dynamic arrays,
//!   associative arrays and run-time indices are a limit: their elements exist
//!   only at run time, as array-level IR (`super::arrays`).

use super::aggregate::{Chain, RawStep, aggregate_chain};
use super::real::{real_kind, strip_conversions};
use super::*;
use crate::constraints::ir::{ArrayId, ArrayNode};

/// What a `unique` member selects from one array dimension.
#[derive(Clone, Copy, Debug)]
enum Sel {
    /// `a[i]`.
    Index(i64),
    /// `a[l:r]`, `a[i +: w]`, `a[i -: w]`: the declared indices `lo..=hi`.
    /// `asc` is the direction a `[l:r]` slice is written in (`None` for the
    /// indexed forms, which take the array's own).
    Slice { lo: i64, hi: i64, asc: Option<bool> },
}

fn bad(what: impl Into<String>) -> BuildError {
    BuildError::BadUnique { what: what.into() }
}

/// `a[2][1]`: the name of the element of `base` at index path `idx`.
fn element_name(base: &str, idx: &[i64]) -> String {
    let mut s = base.to_string();
    for i in idx {
        s.push_str(&format!("[{i}]"));
    }
    s
}

/// The declared bounds `(left, right)` and element type of the outermost
/// dimension of the fixed-size unpacked array `ty`; `None` if `ty` is not an
/// unpacked array. A dynamic array, queue or associative array has no
/// elements before run time, so it is [`BuildError::Unsupported`].
fn dimension<'d>(ty: Type<'d>, what: &str) -> Result<Option<(i64, i64, Type<'d>)>, BuildError> {
    let c = ty.canonical();
    if c.is_dynamically_sized_array() || c.is_queue() || c.is_associative_array() {
        return Err(unsupported(
            format!(
                "`{what}`, whose size is only known at run time (a dynamic array, queue or \
                 associative array), as a `unique` member"
            ),
            "C14",
        ));
    }
    if !c.is_unpacked_array() {
        return Ok(None);
    }
    let r = c.fixed_range();
    let elem = c.element_type().ok_or_else(|| BuildError::Missing {
        what: format!("element type of the array `{what}`"),
    })?;
    Ok(Some((i64::from(r.left), i64::from(r.right), elem)))
}

/// Appends to `out` the index path of every leaf element `sels` selects from a
/// value of type `ty` (every element of a dimension `sels` does not reach),
/// in declared index order, and returns the leaf type.
fn expand<'d>(
    ty: Type<'d>,
    sels: &[Sel],
    name: &str,
    prefix: &mut Vec<i64>,
    out: &mut Vec<Vec<i64>>,
) -> Result<Type<'d>, BuildError> {
    let Some((left, right, elem)) = dimension(ty, name)? else {
        if !sels.is_empty() {
            return Err(bad(format!(
                "`{name}` is selected into below an unpacked array, which is a bit- or \
                 part-select and not a variable"
            )));
        }
        out.push(prefix.clone());
        return Ok(ty);
    };
    let desc = left >= right;
    let (lower, upper) = (left.min(right), left.max(right));
    let check = |i: i64| {
        if (lower..=upper).contains(&i) {
            Ok(())
        } else {
            Err(BuildError::OutOfRangeSelect {
                what: format!("`{name}` index {i} outside [{left}:{right}]"),
            })
        }
    };
    // The array's own index order: `[7:0]` runs 7, 6, ... 0.
    let ordered = |lo: i64, hi: i64| -> Vec<i64> {
        if desc {
            (lo..=hi).rev().collect()
        } else {
            (lo..=hi).collect()
        }
    };
    let indices = match sels.first() {
        Some(Sel::Index(i)) => {
            check(*i)?;
            vec![*i]
        }
        Some(Sel::Slice { lo, hi, asc }) => {
            check(*lo)?;
            check(*hi)?;
            if let Some(asc) = asc
                && lo != hi
                && *asc == desc
            {
                return Err(bad(format!(
                    "the slice of `{name}` is written against the array's declared \
                     direction [{left}:{right}]"
                )));
            }
            ordered(*lo, *hi)
        }
        None => ordered(lower, upper),
    };
    let rest = sels.get(1..).unwrap_or(&[]);
    let mut leaf = None;
    for i in indices {
        prefix.push(i);
        let t = expand(elem, rest, name, prefix, out)?;
        prefix.pop();
        leaf = Some(t);
    }
    leaf.ok_or_else(|| BuildError::Missing {
        what: format!("elements of the array `{name}`"),
    })
}

/// A `unique` group member: the variable it names, what it selects from it,
/// and the leaf elements that is.
struct Member<'d> {
    /// The named value (conversions removed).
    root: Expression<'d>,
    /// The property (or struct member or array element of one) the name
    /// denotes, when it is one of this class (a member read through an object
    /// handle is not).
    chain: Option<Chain<'d>>,
    /// The variable's name as written.
    name: String,
    /// The type of every leaf.
    leaf: Type<'d>,
    /// Each leaf's index path (empty for a scalar variable).
    paths: Vec<Vec<i64>>,
}

impl Builder<'_> {
    /// The root named value of a `unique` member and what is selected from it.
    fn unique_target<'d>(e: Expression<'d>) -> Result<(Expression<'d>, Vec<Sel>), BuildError> {
        let e = strip_conversions(e);
        match e.kind() {
            ExpressionKind::NamedValue
            | ExpressionKind::HierarchicalValue
            | ExpressionKind::MemberAccess => Ok((e, Vec::new())),
            ExpressionKind::ElementSelect | ExpressionKind::RangeSelect => {
                let base =
                    e.select_value()
                        .map(strip_conversions)
                        .ok_or_else(|| BuildError::Missing {
                            what: "base of a select".into(),
                        })?;
                let bt = base.expr_type().ok_or_else(|| BuildError::Missing {
                    what: "type of a select base".into(),
                })?;
                if dimension(bt, "the selected array")?.is_none() {
                    return Err(bad(
                        "a bit- or part-select of a packed value is not a variable",
                    ));
                }
                let (root, mut sels) = Self::unique_target(base)?;
                if matches!(sels.last(), Some(Sel::Slice { .. })) {
                    return Err(unsupported(
                        "a select of an array slice as a `unique` member",
                        "C14",
                    ));
                }
                let run_time = || {
                    unsupported(
                        "a `unique` member selected by a run time index or bound (array \
                         elements are only variables at fixed indices)",
                        "C14",
                    )
                };
                let const_of = |x: Expression<'_>| x.constant_value().and_then(|c| c.as_i64());
                if e.kind() == ExpressionKind::ElementSelect {
                    let i = e.selector().and_then(const_of).ok_or_else(run_time)?;
                    sels.push(Sel::Index(i));
                    return Ok((root, sels));
                }
                let kind = e
                    .range_selection_kind()
                    .ok_or_else(|| BuildError::Missing {
                        what: "kind of a range select".into(),
                    })?;
                let (Some(l), Some(r)) = (e.range_left(), e.range_right()) else {
                    return Err(BuildError::Missing {
                        what: "bounds of a range select".into(),
                    });
                };
                let l = const_of(l).ok_or_else(run_time)?;
                let r = const_of(r).ok_or_else(run_time)?;
                sels.push(if kind == 0 {
                    Sel::Slice {
                        lo: l.min(r),
                        hi: l.max(r),
                        asc: Some(l <= r),
                    }
                } else if r < 1 {
                    return Err(BuildError::Missing {
                        what: "constant width of an indexed part select".into(),
                    });
                } else if kind == 1 {
                    Sel::Slice {
                        lo: l,
                        hi: l + r - 1,
                        asc: None,
                    }
                } else {
                    Sel::Slice {
                        lo: l - r + 1,
                        hi: l,
                        asc: None,
                    }
                });
                Ok((root, sels))
            }
            other => Err(bad(format!("a `{other:?}` expression is not a variable"))),
        }
    }

    /// Resolves one group member to its leaves.
    fn unique_member<'d>(&self, item: Expression<'d>) -> Result<Member<'d>, BuildError> {
        let (root, sels) = Self::unique_target(item)?;
        let chain = aggregate_chain(root, &self.forced_roots);
        let (sym, local) = match root.kind() {
            ExpressionKind::MemberAccess => {
                let base = Self::operand(root, "a member access")?;
                let is_this = base.kind() == ExpressionKind::NamedValue
                    && base.referenced_symbol().is_some_and(|s| s.name() == "this");
                let member = root.member_symbol().ok_or_else(|| BuildError::Missing {
                    what: "member symbol of a member access".into(),
                })?;
                (member, is_this)
            }
            ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => (
                root.referenced_symbol()
                    .ok_or_else(|| BuildError::Missing {
                        what: "symbol of a named value".into(),
                    })?,
                true,
            ),
            other => unreachable!(
                "unique_target returns only named values and member accesses, got {other:?}"
            ),
        };
        let name = sym.name().to_string();
        let ty = root.expr_type().ok_or_else(|| BuildError::Missing {
            what: format!("type of `{name}`"),
        })?;
        let mut paths = Vec::new();
        let leaf = expand(ty, &sels, &name, &mut Vec::new(), &mut paths)?;
        let local = local || chain.is_some();
        if !local && paths.iter().any(|p| !p.is_empty()) {
            return Err(unsupported(
                format!(
                    "array elements of `{name}`, read through an object handle, as `unique` members"
                ),
                "C17 follow-up",
            ));
        }
        Ok(Member {
            root,
            chain,
            name,
            leaf,
            paths,
        })
    }

    /// The group's expression for the leaf at `path` of `m`.
    fn unique_leaf(&mut self, m: &Member<'_>, path: &[i64]) -> Result<Expr, BuildError> {
        let ex = if path.is_empty() {
            self.expr(m.root)?
        } else {
            let mut chain = m.chain.clone().ok_or_else(|| BuildError::Missing {
                what: format!("property symbol of `{}`", m.name),
            })?;
            chain.steps.extend(path.iter().map(|&i| RawStep::Const(i)));
            let ty = ty_of(Some(m.leaf), &format!("`{}`", m.name))?;
            self.aggregate_value(chain, ty)?
        };
        match &ex {
            Expr::Var(id, _) if self.vars[*id as usize].randc => Err(bad(format!(
                "`{}` is a `randc` variable, which may not appear in a `unique` group",
                element_name(&m.name, path)
            ))),
            Expr::Var(..) | Expr::State(..) => Ok(ex),
            _ => Err(bad(format!(
                "`{}` is not a variable (it folds to a constant)",
                element_name(&m.name, path)
            ))),
        }
    }

    /// For a group member that is a whole dynamic array or queue (named by a
    /// variable, with no select): its name and element type; `None` for any
    /// other member.
    fn dynamic_member<'d>(
        &self,
        item: Expression<'d>,
    ) -> Option<Result<(String, Type<'d>), BuildError>> {
        let e = strip_conversions(item);
        if !matches!(
            e.kind(),
            ExpressionKind::NamedValue
                | ExpressionKind::HierarchicalValue
                | ExpressionKind::MemberAccess
        ) {
            return None;
        }
        let t = e.expr_type()?.canonical();
        if !(t.is_dynamically_sized_array() || t.is_queue()) {
            return None;
        }
        let name = e
            .referenced_symbol()
            .or_else(|| e.member_symbol())
            .map(|s| s.name().to_string())
            .unwrap_or_default();
        let elem = t.element_type();
        Some(
            elem.map(|el| (name.clone(), el))
                .ok_or_else(|| BuildError::Missing {
                    what: format!("element type of the array `{name}`"),
                }),
        )
    }

    /// One `unique { ... }` constraint (LRM 18.5.4): its conjuncts (none for a
    /// group of fewer than two members).
    pub(super) fn unique(&mut self, c: Constraint<'_>) -> Result<Vec<Expr>, BuildError> {
        let mut group = Vec::new();
        // Whole dynamic arrays or queues: (name, element type, array).
        let mut dyns: Vec<(String, Type<'_>, ArrayId)> = Vec::new();
        for k in c.children() {
            let item = k.as_expression().ok_or_else(|| BuildError::Missing {
                what: "expression member of a `unique` constraint".into(),
            })?;
            if let Some(t) = self.dynamic_member(item) {
                let (name, leaf) = t?;
                self.arrays_allowed("a dynamic array as a `unique` member")?;
                dyns.push((name, leaf, self.array_of(item)?));
                continue;
            }
            group.push(self.unique_member(item)?);
        }
        if dyns.is_empty() && group.iter().map(|m| m.paths.len()).sum::<usize>() < 2 {
            return Ok(Vec::new());
        }
        for (name, leaf, _) in &dyns {
            if real_kind(Some(*leaf)).is_some() {
                return Err(BuildError::RealConstraint {
                    what: format!(
                        "`unique` over the real elements of `{name}`: the real-domain solver \
                         has no pairwise-distinct constraint (IEEE 1800-2023 18.5.4 allows \
                         real members)"
                    ),
                });
            }
            if !leaf.is_integral() {
                return Err(bad(format!(
                    "the elements of `{name}` are not of an integral or real type (they are `{}`)",
                    leaf.to_sv_string()
                )));
            }
        }
        let mut members = Vec::new();
        for m in &group {
            if real_kind(Some(m.leaf)).is_some() {
                return Err(BuildError::RealConstraint {
                    what: format!(
                        "`unique` over the real value `{}`: the real-domain solver has no \
                         pairwise-distinct constraint (IEEE 1800-2023 18.5.4 allows real members)",
                        m.name
                    ),
                });
            }
            if !m.leaf.is_integral() {
                return Err(bad(format!(
                    "`{}` is not a variable of an integral or real type (it is `{}`)",
                    m.name,
                    m.leaf.to_sv_string()
                )));
            }
            for p in &m.paths {
                members.push(self.unique_leaf(m, p)?);
            }
        }
        let leaves: Vec<(&str, Type<'_>)> = group
            .iter()
            .map(|m| (m.name.as_str(), m.leaf))
            .chain(dyns.iter().map(|(n, l, _)| (n.as_str(), *l)))
            .collect();
        let (first_name, first_leaf) = leaves[0];
        for &(name, leaf) in &leaves[1..] {
            if !first_leaf.is_equivalent(&leaf) {
                return Err(bad(format!(
                    "`{first_name}` (`{}`) and `{name}` (`{}`) are not of equivalent types \
                     (IEEE 1800-2023 6.22.1)",
                    first_leaf.to_sv_string(),
                    leaf.to_sv_string()
                )));
            }
        }
        if !dyns.is_empty() {
            // The dynamic arrays' length is known only at run time: the group
            // expands once the sizes are (`ArrayNode::Distinct`).
            let arrays: Vec<ArrayId> = dyns.iter().map(|d| d.2).collect();
            let elem = self.arrays[arrays[0] as usize].elem_ty;
            if members.iter().any(|e| e.ty() != elem)
                || arrays
                    .iter()
                    .any(|&a| self.arrays[a as usize].elem_ty != elem)
            {
                return Err(bad(
                    "the members are not of equivalent types (their solved widths or signedness differ)",
                ));
            }
            return Ok(vec![Expr::Array(ArrayNode::Distinct {
                scalars: members,
                arrays,
            })]);
        }
        let ty = members[0].ty();
        if members.iter().any(|e| e.ty() != ty) {
            return Err(bad(
                "the members are not of equivalent types (their solved widths or signedness differ)",
            ));
        }
        Ok(vec![Expr::AllDistinct(members)])
    }
}