vj-sim 0.2.0

//! `dist` constraints (plan task C6; IEEE 1800-2023 18.5.3).
//!
//! # Encoding
//!
//! `x dist { v1 := w1, [lo:hi] :/ w2, default :/ w3 }` is a *membership*
//! constraint plus a *weighting*. The builder gives each `dist` a hidden
//! selector variable `K` (an id from [`SELECTOR_BASE`] up, renumbered densely
//! by the registry) with one code per item, and emits the conjunct
//!
//! ```text
//!   OR_i ( K == i  &&  x is in item i )
//! ```
//!
//! so the solution space is exactly "x is in some item" (an item never listed
//! excludes its values, 18.5.3), and every other constraint, guard and `solve
//! before` sees an ordinary constraint. The weighting is applied when the
//! solution is *drawn* ([`super::solve::Weighted`]): `K` is chosen with
//! probability proportional to `weight_i * (feasible values of x in item i)`,
//! then `x` is drawn uniformly over those values, so the probability of a
//! feasible value `v` is proportional to the sum of the per-value weights of
//! the items containing `v`. That is the LRM's rule: `:=` gives every value of
//! the item the weight, `:/` divides it among the item's values, items that
//! overlap add, a value excluded by another constraint just drops out (the
//! rest renormalise), and a value of weight 0 is never chosen. `default :/ w`
//! is the item of every value no explicit item names. An item without a
//! weight has weight `:= 1`.
//!
//! The weights and the value counts are expressions over *state* variables
//! (bounds and weights are evaluated by [`Dist::weights`] at each
//! `randomize()`), so `x dist { [lo:hi] :/ n }` with `lo`, `hi` and `n` fields
//! of the object works. A random variable in a bound or a weight is rejected
//! by the builder.
//!
//! # Limits (also in the plan's notes)
//!
//! * Several `dist`s on coupled variables are applied one after the other
//!   (each is exact on its own, their product is not the joint weighting).
//! * A `dist` under a guard whose predicate mentions a random variable still
//!   always satisfies the constraint, but its weights only approximately shape
//!   the distribution (the selector is drawn before the guard's variable).
//! * For a subject that is not a single variable the selector is weighted by
//!   the number of *tuples* each item leaves, not of subject values.

use super::ir::{Assignment, ConstraintEvalError, Expr, IrError, Ty, VarId, eval};
use super::solve::Weight;
use core::fmt;
use num_bigint::BigInt;
use num_bigint::BigUint;
use num_traits::{One, Zero};

/// The first selector id. Selector `j` is `SELECTOR_BASE + j`; the builder
/// never allocates a random-variable id this large, and the registry
/// substitutes the dense ids before anything is compiled.
pub const SELECTOR_BASE: VarId = 1 << 30;

/// The values of one `dist` item, as expressions of the item's comparison
/// type [`Item::ty`] over state variables and constants.
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub enum Span {
    /// A single value.
    Point(Expr),
    /// `[lo:hi]` (inclusive); `None` is `$`, the subject type's own extreme.
    Range {
        /// The low bound.
        lo: Option<Expr>,
        /// The high bound.
        hi: Option<Expr>,
    },
}

/// One explicit item of a `dist`.
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Item {
    /// The one-bit predicate "the subject is in this item" (over the subject's
    /// variables and states).
    pub member: Expr,
    /// The type the subject is compared with the bounds in (LRM 11.8: the
    /// common type of the subject and the bound).
    pub ty: Ty,
    /// The item's values.
    pub span: Span,
    /// The weight expression (over states and constants).
    pub weight: Expr,
    /// `:/` (the weight is divided among the item's values) rather than `:=`.
    pub per_range: bool,
}

/// `default :/ w` (or `:= w`): the weight of the values no item names.
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct DefaultWeight {
    /// The weight expression.
    pub weight: Expr,
    /// `:/` rather than `:=`.
    pub per_range: bool,
}

/// One `dist` expression.
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Dist {
    /// The type of the distributed expression.
    pub subject_ty: Ty,
    /// The distributed variable, when the expression is exactly one random
    /// variable (the case the weighting is exact for).
    pub plain_var: Option<VarId>,
    /// Every random variable the distributed expression reads, ascending.
    pub vars: Vec<VarId>,
    /// The explicit items, in source order; code `i` is item `i`.
    pub items: Vec<Item>,
    /// The `default` item; its code follows the explicit items'.
    pub default: Option<DefaultWeight>,
    /// `Some(subject)` marks a *template*: a `dist` written inside a `foreach`
    /// over a dynamic array or queue (LRM 18.5.7.1, 18.5.3), which must hold
    /// once per element. Its expressions are array-level IR over the loop
    /// variable and cannot be weighed as they stand: `array::expand` makes one
    /// instance of the dist, with a selector of its own, per iteration (module
    /// docs of `super::array`), expanding `subject` (the array-level distributed
    /// expression), the bounds and the weights for that iteration. A template
    /// keeps its selector slot in the program but is never planned itself.
    pub subject: Option<Expr>,
}

/// Why [`Dist::weights`] failed.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum DistError {
    /// A bound or weight could not be evaluated (an X/Z state, a division by
    /// zero).
    Eval(ConstraintEvalError),
    /// A weight evaluated to a negative number (LRM 18.5.3: weights are
    /// non-negative).
    NegativeWeight,
}

impl fmt::Display for DistError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            DistError::Eval(e) => write!(f, "in a `dist` weight or bound: {e}"),
            DistError::NegativeWeight => f.write_str("a `dist` weight is negative"),
        }
    }
}

impl std::error::Error for DistError {}

impl From<ConstraintEvalError> for DistError {
    fn from(e: ConstraintEvalError) -> Self {
        DistError::Eval(e)
    }
}

fn numeric(v: &BigUint, t: Ty) -> BigInt {
    if t.signed && v.bit(u64::from(t.width) - 1) {
        BigInt::from(v.clone()) - (BigInt::one() << t.width)
    } else {
        BigInt::from(v.clone())
    }
}

/// The values the subject `s` can take, as numbers in the comparison space
/// `t`: a signed comparison sees a signed subject's signed values, anything
/// else the subject's bit patterns (LRM 11.8.2: an unsigned context
/// zero-extends).
fn subject_range_in(t: Ty, s: Ty) -> (BigInt, BigInt) {
    if t.signed && s.signed {
        let half = BigInt::one() << (s.width - 1);
        (-half.clone(), half - BigInt::one())
    } else {
        (BigInt::zero(), (BigInt::one() << s.width) - BigInt::one())
    }
}

/// The subject values `lo <= S && S <= hi` selects when the two bounds are
/// compared in different types (18.5.3: each bound is compared in the common
/// type of the subject and that bound, so a signed subject with one signed and
/// one unsigned bound mixes a numeric and a bit-pattern comparison). Returns
/// disjoint intervals of the subject's own numeric values.
fn mixed_bound_cover(
    s: Ty,
    (lo, lo_ty): (&BigInt, Ty),
    (hi, hi_ty): (&BigInt, Ty),
) -> Vec<(BigInt, BigInt)> {
    let w = s.width;
    let (nmin, nmax) = if s.signed {
        let half = BigInt::one() << (w - 1);
        (-half.clone(), half - BigInt::one())
    } else {
        (BigInt::zero(), (BigInt::one() << w) - BigInt::one())
    };
    // One bound's side as intervals of the subject's numeric values.
    let side = |v: &BigInt, t: Ty, is_lo: bool| -> Vec<(BigInt, BigInt)> {
        if t.signed || !s.signed {
            // Numeric comparison (both signed, or the subject is unsigned and
            // its numeric value is its pattern).
            let (a, b) = if is_lo {
                (v.clone().max(nmin.clone()), nmax.clone())
            } else {
                (nmin.clone(), v.clone().min(nmax.clone()))
            };
            return if a <= b { vec![(a, b)] } else { Vec::new() };
        }
        // Unsigned comparison of a signed subject's bit pattern: an interval
        // of patterns, whose upper half is the negative numbers.
        let pmax = (BigInt::one() << w) - BigInt::one();
        let (a, b) = if is_lo {
            (v.clone().max(BigInt::zero()), pmax.clone())
        } else {
            (BigInt::zero(), v.clone().min(pmax.clone()))
        };
        if a > b {
            return Vec::new();
        }
        let half = BigInt::one() << (w - 1);
        let full = BigInt::one() << w;
        let mut out = Vec::new();
        if a < half {
            out.push((a.clone(), (&half - BigInt::one()).min(b.clone())));
        }
        if b >= half {
            out.push((a.max(half) - &full, b - &full));
        }
        out
    };
    let (ls, hs) = (side(lo, lo_ty, true), side(hi, hi_ty, false));
    let mut out = Vec::new();
    for (a, b) in &ls {
        for (c, d) in &hs {
            let (x, y) = (a.max(c).clone(), b.min(d).clone());
            if x <= y {
                out.push((x, y));
            }
        }
    }
    out
}

/// Total size of the union of the inclusive intervals.
fn union_len(mut iv: Vec<(BigInt, BigInt)>) -> BigInt {
    iv.sort();
    let mut total = BigInt::zero();
    let mut cur: Option<(BigInt, BigInt)> = None;
    for (a, b) in iv {
        cur = match cur {
            Some((ca, cb)) if a <= &cb + BigInt::one() => Some((ca, if b > cb { b } else { cb })),
            Some((ca, cb)) => {
                total += cb - ca + BigInt::one();
                Some((a, b))
            }
            None => Some((a, b)),
        };
    }
    if let Some((a, b)) = cur {
        total += b - a + BigInt::one();
    }
    total
}

impl Dist {
    /// Checks every expression of the dist against the IR's typing rules and
    /// that the weights and bounds read no random variable.
    pub fn validate(&self) -> Result<(), IrError> {
        let state_only = |e: &Expr| -> Result<(), IrError> {
            e.validate()?;
            let mut has_var = false;
            e.for_each_var(&mut |_, _| has_var = true);
            if has_var {
                return Err(IrError::IllTyped {
                    what: "a `dist` weight or bound reads a random variable".into(),
                });
            }
            Ok(())
        };
        for it in &self.items {
            it.member.validate()?;
            state_only(&it.weight)?;
            match &it.span {
                Span::Point(v) => state_only(v)?,
                Span::Range { lo, hi } => {
                    for b in [lo, hi].into_iter().flatten() {
                        state_only(b)?;
                    }
                }
            }
        }
        if let Some(d) = &self.default {
            state_only(&d.weight)?;
        }
        Ok(())
    }

    /// The number of selector codes: one per item, plus the default's.
    pub fn codes(&self) -> usize {
        self.items.len() + usize::from(self.default.is_some())
    }

    /// The selector variable's type: just wide enough for [`Self::codes`].
    pub fn selector_ty(&self) -> Ty {
        let top = self.codes().saturating_sub(1) as u64;
        Ty::unsigned((64 - top.leading_zeros()).max(1))
    }

    /// The conjunct `OR_i (sel == i && member_i)` (the default's member is
    /// "no explicit item holds").
    pub fn conjunct(&self, sel: VarId) -> Expr {
        let kt = self.selector_ty();
        let bin = |op, a: Expr, b: Expr| Expr::Binary(op, Box::new(a), Box::new(b), Ty::BIT);
        let code = |i: usize| {
            bin(
                super::ir::BinOp::Eq,
                Expr::Var(sel, kt),
                Expr::constant(kt, i as u64),
            )
        };
        let mut terms: Vec<Expr> = self
            .items
            .iter()
            .enumerate()
            .map(|(i, it)| bin(super::ir::BinOp::LogAnd, code(i), it.member.clone()))
            .collect();
        if self.default.is_some() {
            let any = self
                .items
                .iter()
                .map(|it| it.member.clone())
                .reduce(|a, b| bin(super::ir::BinOp::LogOr, a, b));
            let none = match any {
                Some(a) => Expr::Unary(super::ir::UnOp::LogNot, Box::new(a), Ty::BIT),
                None => Expr::Const(Ty::BIT, BigUint::one()),
            };
            terms.push(bin(super::ir::BinOp::LogAnd, code(self.items.len()), none));
        }
        terms
            .into_iter()
            .reduce(|a, b| bin(super::ir::BinOp::LogOr, a, b))
            .unwrap_or(Expr::Const(Ty::BIT, BigUint::zero()))
    }

    /// The per-value weight of every selector code under the current values of
    /// the state variables: item `i`'s weight (`:=`) or its weight divided by
    /// the number of values of the item (`:/`), and likewise for the default
    /// over the values no explicit item names. A weight of an empty item is 0.
    pub fn weights(&self, states: &[Option<BigUint>]) -> Result<Vec<Weight>, DistError> {
        let a = Assignment {
            vars: Vec::new(),
            states: states.to_vec(),
        };
        let weight_of = |e: &Expr| -> Result<BigUint, DistError> {
            let v = numeric(&eval(e, &a)?, e.ty());
            v.to_biguint().ok_or(DistError::NegativeWeight)
        };
        let per = |w: BigUint, per_range: bool, n: &BigInt| -> Weight {
            if !per_range {
                return Weight::int(w);
            }
            match n.to_biguint() {
                Some(n) if !n.is_zero() => Weight { num: w, den: n },
                _ => Weight::int(0u32),
            }
        };
        let mut out = Vec::with_capacity(self.codes());
        let mut covered: Vec<(BigInt, BigInt)> = Vec::new();
        for it in &self.items {
            let (smin, smax) = subject_range_in(it.ty, self.subject_ty);
            let bound = |e: &Option<Expr>, dflt: &BigInt| -> Result<BigInt, DistError> {
                match e {
                    Some(e) => Ok(numeric(&eval(e, &a)?, e.ty())),
                    None => Ok(dflt.clone()),
                }
            };
            let (lo, hi) = match &it.span {
                Span::Point(v) => {
                    let n = numeric(&eval(v, &a)?, v.ty());
                    (n.clone(), n)
                }
                Span::Range { lo, hi } => (bound(lo, &smin)?, bound(hi, &smax)?),
            };
            let n = if hi >= lo {
                &hi - &lo + 1
            } else {
                BigInt::zero()
            };
            out.push(per(weight_of(&it.weight)?, it.per_range, &n));
            // The subject values the item covers, clipped to what the subject
            // can hold, as intervals of its own numeric values.
            if let Span::Range {
                lo: Some(l),
                hi: Some(h),
            } = &it.span
                && l.ty() != h.ty()
            {
                covered.extend(mixed_bound_cover(
                    self.subject_ty,
                    (&lo, l.ty()),
                    (&hi, h.ty()),
                ));
                continue;
            }
            let (a_, b_) = (lo.max(smin), hi.min(smax));
            if a_ > b_ {
                continue;
            }
            if self.subject_ty.signed && !it.ty.signed {
                // Bit patterns of a signed subject: the upper half of the
                // pattern range is the negative numbers.
                let half = BigInt::one() << (self.subject_ty.width - 1);
                let full = BigInt::one() << self.subject_ty.width;
                if a_ < half {
                    covered.push((a_.clone(), (&half - BigInt::one()).min(b_.clone())));
                }
                if b_ >= half {
                    covered.push((a_.max(half) - &full, b_ - &full));
                }
            } else {
                covered.push((a_, b_));
            }
        }
        if let Some(d) = &self.default {
            let width = self.subject_ty.width;
            let n = (BigInt::one() << width) - union_len(covered);
            out.push(per(weight_of(&d.weight)?, d.per_range, &n));
        }
        Ok(out)
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::constraints::ir::BinOp;

    fn u(w: u32) -> Ty {
        Ty::unsigned(w)
    }
    fn k(t: Ty, v: u64) -> Expr {
        Expr::constant(t, v)
    }
    fn bin(op: BinOp, a: Expr, b: Expr) -> Expr {
        Expr::Binary(op, Box::new(a), Box::new(b), Ty::BIT)
    }
    fn item(x: &Expr, lo: u64, hi: u64, w: u64, per_range: bool) -> Item {
        let t = x.ty();
        Item {
            member: bin(
                BinOp::LogAnd,
                bin(BinOp::Ge, x.clone(), k(t, lo)),
                bin(BinOp::Le, x.clone(), k(t, hi)),
            ),
            ty: t,
            span: Span::Range {
                lo: Some(k(t, lo)),
                hi: Some(k(t, hi)),
            },
            weight: k(u(32), w),
            per_range,
        }
    }
    fn dist(subject_ty: Ty, items: Vec<Item>, default: Option<DefaultWeight>) -> Dist {
        Dist {
            subject_ty,
            plain_var: Some(0),
            vars: vec![0],
            items,
            default,
            subject: None,
        }
    }
    fn w(num: u32, den: u32) -> Weight {
        Weight {
            num: num.into(),
            den: den.into(),
        }
    }

    #[test]
    fn the_selector_has_one_code_per_item_and_the_default() {
        let x = Expr::Var(0, u(8));
        let d = dist(u(8), vec![item(&x, 1, 1, 1, false)], None);
        assert_eq!((d.codes(), d.selector_ty()), (1, u(1)));
        let d = dist(
            u(8),
            vec![item(&x, 1, 1, 1, false), item(&x, 2, 2, 1, false)],
            None,
        );
        assert_eq!((d.codes(), d.selector_ty()), (2, u(1)));
        let d = dist(
            u(8),
            vec![item(&x, 1, 1, 1, false), item(&x, 2, 2, 1, false)],
            Some(DefaultWeight {
                weight: k(u(32), 1),
                per_range: true,
            }),
        );
        assert_eq!((d.codes(), d.selector_ty()), (3, u(2)));
    }

    #[test]
    fn per_value_and_per_range_weights() {
        // `[0:3] := 5, [4:11] :/ 8`: 5 per value; 8 / 8 = 1 per value.
        let x = Expr::Var(0, u(8));
        let d = dist(
            u(8),
            vec![item(&x, 0, 3, 5, false), item(&x, 4, 11, 8, true)],
            None,
        );
        assert_eq!(d.weights(&[]).unwrap(), vec![w(5, 1), w(8, 8)]);
    }

    #[test]
    fn the_default_weight_spreads_over_the_values_no_item_names() {
        // 4-bit subject, items [0:3] and [2:5] overlap and cover 0..=5: the
        // default owns the other 10 values.
        let x = Expr::Var(0, u(4));
        let d = dist(
            u(4),
            vec![item(&x, 0, 3, 1, false), item(&x, 2, 5, 1, false)],
            Some(DefaultWeight {
                weight: k(u(32), 20),
                per_range: true,
            }),
        );
        assert_eq!(d.weights(&[]).unwrap()[2], w(20, 10));
    }

    #[test]
    fn an_item_beyond_the_subjects_range_does_not_shrink_the_default() {
        // [10:40] on a 4-bit subject covers 10..=15 only (6 values), the
        // default owns the other 10; the item itself still has 31 values.
        // The bounds are in the 32-bit comparison type of the `int` literals.
        let wide = Item {
            member: Expr::Const(Ty::BIT, BigUint::one()),
            ty: u(32),
            span: Span::Range {
                lo: Some(k(u(32), 10)),
                hi: Some(k(u(32), 40)),
            },
            weight: k(u(32), 31),
            per_range: true,
        };
        let d = dist(
            u(4),
            vec![wide],
            Some(DefaultWeight {
                weight: k(u(32), 10),
                per_range: true,
            }),
        );
        assert_eq!(d.weights(&[]).unwrap(), vec![w(31, 31), w(10, 10)]);
    }

    #[test]
    fn an_empty_range_and_a_full_default_have_weight_zero_not_a_zero_divisor() {
        let x = Expr::Var(0, u(2));
        // `[3:1] :/ 4` is empty; `[0:3]` covers every value, so the default
        // is empty too.
        let d = dist(
            u(2),
            vec![item(&x, 3, 1, 4, true), item(&x, 0, 3, 1, false)],
            Some(DefaultWeight {
                weight: k(u(32), 9),
                per_range: true,
            }),
        );
        assert_eq!(d.weights(&[]).unwrap(), vec![w(0, 1), w(1, 1), w(0, 1)]);
    }

    #[test]
    fn weights_and_bounds_read_state_variables() {
        // `[lo:hi] :/ s` with states lo = 0, hi = 9, s = 20.
        let st = |i: u32| Expr::State(i, u(8));
        let d = dist(
            u(8),
            vec![Item {
                member: Expr::Const(Ty::BIT, BigUint::one()),
                ty: u(8),
                span: Span::Range {
                    lo: Some(st(0)),
                    hi: Some(st(1)),
                },
                weight: st(2),
                per_range: true,
            }],
            None,
        );
        let states = [Some(0u32.into()), Some(9u32.into()), Some(20u32.into())];
        assert_eq!(d.weights(&states).unwrap(), vec![w(20, 10)]);
        // An X state is the usual loud error, never a silent 0.
        let unknown = [Some(0u32.into()), None, Some(20u32.into())];
        assert_eq!(
            d.weights(&unknown),
            Err(DistError::Eval(ConstraintEvalError::StateUnknown(1)))
        );
    }

    #[test]
    fn a_negative_weight_is_an_error() {
        let x = Expr::Var(0, u(8));
        let mut it = item(&x, 1, 1, 1, false);
        it.weight = Expr::constant(Ty::signed(8), 0xFFu32); // -1
        let d = dist(u(8), vec![it], None);
        assert_eq!(d.weights(&[]), Err(DistError::NegativeWeight));
    }

    #[test]
    fn a_signed_subject_counts_negative_values_in_the_default() {
        // 4-bit signed subject (-8..=7), item [-2:1] (4 values) in a signed
        // comparison: the default owns the other 12.
        let t = Ty::signed(4);
        let neg2 = Expr::constant(t, 0xEu32);
        let one = Expr::constant(t, 1u32);
        let d = dist(
            t,
            vec![Item {
                member: Expr::Const(Ty::BIT, BigUint::one()),
                ty: t,
                span: Span::Range {
                    lo: Some(neg2),
                    hi: Some(one),
                },
                weight: k(u(32), 1),
                per_range: false,
            }],
            Some(DefaultWeight {
                weight: k(u(32), 12),
                per_range: true,
            }),
        );
        assert_eq!(d.weights(&[]).unwrap(), vec![w(1, 1), w(12, 12)]);
    }

    #[test]
    fn range_bounds_of_different_types_cover_the_intersection() {
        // 18.5.3: a 4-bit signed subject with `[-2 : 4'd12]`: the low bound is
        // a signed comparison (S >= -2), the high bound an unsigned one on the
        // bit pattern (pattern <= 12, i.e. S in 0..=7 or -8..=-4). Hand-derived
        // intersection: 0..=7, 8 values, so the default owns the other 8.
        let t = Ty::signed(4);
        let d = dist(
            t,
            vec![Item {
                member: Expr::Const(Ty::BIT, BigUint::one()),
                ty: t,
                span: Span::Range {
                    lo: Some(Expr::constant(t, 0xEu32)),
                    hi: Some(Expr::constant(u(4), 12u32)),
                },
                weight: k(u(32), 1),
                per_range: false,
            }],
            Some(DefaultWeight {
                weight: k(u(32), 8),
                per_range: true,
            }),
        );
        assert_eq!(d.weights(&[]).unwrap(), vec![w(1, 1), w(8, 8)]);
    }

    #[test]
    fn the_conjunct_is_membership_of_exactly_one_item() {
        // `x dist { 1 := 1, 2 := 1, default :/ 1 }` over a 2-bit x with the
        // selector K (var 1): a model needs K to name an item holding x, and
        // K == 2 (default) holds only for the values no item names (0 and 3).
        let x = Expr::Var(0, u(2));
        let d = dist(
            u(2),
            vec![item(&x, 1, 1, 1, false), item(&x, 2, 2, 1, false)],
            Some(DefaultWeight {
                weight: k(u(32), 1),
                per_range: true,
            }),
        );
        let c = d.conjunct(1);
        let kt = d.selector_ty();
        let ok = |xv: u64, kv: u64| {
            let a = Assignment {
                vars: vec![xv.into(), kv.into()],
                states: vec![],
            };
            eval(&c, &a).unwrap() == BigUint::one()
        };
        for xv in 0..4 {
            for kv in 0..(1u64 << kt.width) {
                let want = match kv {
                    0 => xv == 1,
                    1 => xv == 2,
                    2 => xv == 0 || xv == 3,
                    _ => false,
                };
                assert_eq!(ok(xv, kv), want, "x={xv} K={kv}");
            }
        }
    }
}