sv_sim_sim/constraints/
reduce.rs

1//! A program with some constraint blocks left out (IEEE 1800-2023 18.9).
2//!
3//! `constraint_mode(0)` makes a block inactive: nothing it holds applies to the
4//! call. That is its boolean constraints, and also every `dist`, `solve ...
5//! before` ordering, constraint over `real` variables and `disable soft` it
6//! contains, and the `soft` constraints it declares (a `disable soft` of an
7//! inactive block no longer discards the softs it named). [`without_blocks`]
8//! builds the [`Program`] one call then solves: every table that holds block
9//! content has the blocks' entries removed and the hidden variables that name
10//! entries by position (the selector of `dist` `j`, the discard flag of soft
11//! `k`) are renumbered, so the solver never sees what was switched off, not
12//! even as an unused weight to evaluate.
13
14use super::dist::SELECTOR_BASE;
15use super::ir::Expr;
16use super::priority::SOFT_BASE;
17use super::registry::{Outcome, ProgBlock, Program};
18use std::ops::Range;
19
20/// What a constraint block holds besides boolean conjuncts: a range of each
21/// table of its program (or of the builder's [`ConstraintSet`], empty when the
22/// block added nothing to that table).
23///
24/// [`ConstraintSet`]: super::build::ConstraintSet
25#[derive(Clone, Debug, PartialEq, Eq, Default, serde::Serialize, serde::Deserialize)]
26pub struct BlockItems {
27    /// `dist`s ([`Program::dists`]), those of the block's `soft` constraints
28    /// included.
29    pub dists: Range<usize>,
30    /// `soft` constraints ([`Program::softs`]).
31    pub softs: Range<usize>,
32    /// `solve ... before` edges over integral variables ([`Program::before`]).
33    pub before: Range<usize>,
34    /// Constraints over real variables (`real.conds` of the program).
35    pub real_conds: Range<usize>,
36    /// Real `dist`s (`real.dists` of the program).
37    pub real_dists: Range<usize>,
38    /// `solve ... before` edges over real variables (`real.before` of the
39    /// program).
40    pub real_before: Range<usize>,
41    /// `disable soft`s: indices into the table [`super::priority::Soft::disabled_by`]
42    /// names ([`Program::n_disables`] counts it).
43    pub disables: Range<usize>,
44}
45
46impl BlockItems {
47    /// These ranges moved by `by`: the block's items in a table the member's own
48    /// table was appended to at `by`.
49    pub(super) fn shifted(&self, by: &ItemOffsets) -> BlockItems {
50        let mv = |r: &Range<usize>, n: usize| r.start + n..r.end + n;
51        BlockItems {
52            dists: mv(&self.dists, by.dists),
53            softs: mv(&self.softs, by.softs),
54            before: mv(&self.before, by.before),
55            real_conds: mv(&self.real_conds, 0),
56            real_dists: mv(&self.real_dists, 0),
57            real_before: mv(&self.real_before, 0),
58            disables: mv(&self.disables, by.disables),
59        }
60    }
61}
62
63/// Where a program's tables start inside a merged program's ([`BlockItems::shifted`]).
64/// The real tables are never merged (a joint solve refuses real variables).
65pub(super) struct ItemOffsets {
66    pub dists: usize,
67    pub softs: usize,
68    pub before: usize,
69    pub disables: usize,
70}
71
72/// Which entries of a table of `len` entries the `ranges` cover.
73fn covered<'a>(
74    len: usize,
75    ranges: impl Iterator<Item = &'a Range<usize>>,
76) -> Result<Vec<bool>, Outcome> {
77    let mut gone = vec![false; len];
78    for r in ranges {
79        gone.get_mut(r.clone()).ok_or(Outcome::Failed)?.fill(true);
80    }
81    Ok(gone)
82}
83
84/// The new position of every entry of a table after the `gone` ones are
85/// removed.
86fn renumber(gone: &[bool]) -> Vec<Option<u32>> {
87    let mut next = 0u32;
88    gone.iter()
89        .map(|&g| {
90            (!g).then(|| {
91                next += 1;
92                next - 1
93            })
94        })
95        .collect()
96}
97
98/// The entries of `items` not marked in `gone`.
99fn keep<T: Clone>(items: &[T], gone: &[bool]) -> Vec<T> {
100    items
101        .iter()
102        .zip(gone)
103        .filter(|&(_, &g)| !g)
104        .map(|(x, _)| x.clone())
105        .collect()
106}
107
108/// `program` without what the constraint blocks `off` hold (module docs).
109/// The result has no blocks: it is for one call. [`Outcome::Failed`] when the
110/// program is malformed (a range outside its table, a constraint that names a
111/// `dist` or soft of a block that is not in `off`'s company).
112pub(super) fn without_blocks(program: &Program, off: &[&ProgBlock]) -> Result<Program, Outcome> {
113    let gone_conj = covered(program.conjuncts.len(), off.iter().map(|b| &b.conjuncts))?;
114    let gone_dist = covered(program.dists.len(), off.iter().map(|b| &b.items.dists))?;
115    let gone_soft = covered(program.softs.len(), off.iter().map(|b| &b.items.softs))?;
116    let gone_before = covered(program.before.len(), off.iter().map(|b| &b.items.before))?;
117    let gone_rc = covered(
118        program.real.conds.len(),
119        off.iter().map(|b| &b.items.real_conds),
120    )?;
121    let gone_rd = covered(
122        program.real.dists.len(),
123        off.iter().map(|b| &b.items.real_dists),
124    )?;
125    let gone_rb = covered(
126        program.real.before.len(),
127        off.iter().map(|b| &b.items.real_before),
128    )?;
129    let gone_disable = covered(program.n_disables, off.iter().map(|b| &b.items.disables))?;
130    let conj_at = renumber(&gone_conj);
131    let dist_at = renumber(&gone_dist);
132    let soft_at = renumber(&gone_soft);
133
134    // The hidden variables of the surviving conjuncts, renumbered to the
135    // surviving tables.
136    let mut dangling = false;
137    let mut conjuncts: Vec<Expr> = Vec::with_capacity(program.conjuncts.len());
138    for (c, _) in program
139        .conjuncts
140        .iter()
141        .zip(&gone_conj)
142        .filter(|&(_, &g)| !g)
143    {
144        conjuncts.push(c.substitute_vars(&mut |v, t| {
145            let (base, at) = if v >= SOFT_BASE {
146                (SOFT_BASE, &soft_at)
147            } else if v >= SELECTOR_BASE {
148                (SELECTOR_BASE, &dist_at)
149            } else {
150                return Expr::Var(v, t);
151            };
152            match at.get((v - base) as usize).copied().flatten() {
153                Some(n) => Expr::Var(base + n, t),
154                None => {
155                    dangling = true;
156                    Expr::Var(v, t)
157                }
158            }
159        }));
160    }
161    if dangling {
162        return Err(Outcome::Failed);
163    }
164
165    let mut out = program.clone();
166    out.conjuncts = conjuncts;
167    for v in &mut out.vars {
168        if let Some(d) = v.domain_conjunct {
169            // an enum-domain conjunct belongs to no block
170            v.domain_conjunct =
171                Some(conj_at.get(d).copied().flatten().ok_or(Outcome::Failed)? as usize);
172        }
173    }
174    out.before = keep(&program.before, &gone_before);
175    out.dists = keep(&program.dists, &gone_dist);
176    out.softs = Vec::with_capacity(program.softs.len());
177    for (s, _) in program.softs.iter().zip(&gone_soft).filter(|&(_, &g)| !g) {
178        let mut s = s.clone();
179        s.dists = s
180            .dists
181            .iter()
182            .map(|&d| dist_at.get(d as usize).copied().flatten())
183            .collect::<Option<_>>()
184            .ok_or(Outcome::Failed)?;
185        // a `disable soft` of an inactive block discards nothing
186        s.disabled = s
187            .disabled_by
188            .iter()
189            .any(|&d| gone_disable.get(d as usize) == Some(&false));
190        out.softs.push(s);
191    }
192    out.real.conds = keep(&program.real.conds, &gone_rc);
193    out.real.dists = keep(&program.real.dists, &gone_rd);
194    out.real.before = keep(&program.real.before, &gone_rb);
195    out.blocks = Vec::new();
196    Ok(out)
197}
sv_sim_sim/constraints/reduce.rs

sv_sim_sim/constraints/
reduce.rs
