probl_engine/
symbolic.rs

1//! Experimental: answering finite Boolean programs with decision diagrams
2//! instead of worlds (docs/design/symbolic-inference.md, stage 1).
3//!
4//! Each draw is a variable, each Boolean a diagram over the variables, and
5//! the evidence one diagram. A report is then weighted model counts: of the
6//! worlds that reach it with its value true, and with it false. Enumeration
7//! would keep a world for each assignment of the draws that are still live,
8//! which can be all of them; a diagram shares what the assignments have in
9//! common. The results are the same, up to rounding.
10//!
11//! It runs programs whose top level is made of draws from Boolean laws
12//! (like `bernoulli(1%)`, or a law that depends on Booleans, like
13//! `if sick { bernoulli(95%) } else { bernoulli(8%) }`), Boolean
14//! expressions, assignments, `if`, observations, `score` and reports
15//! without `by`. Values other than Booleans, like probabilities and laws,
16//! are constants, or one constant in each of a few sets of worlds. Anything
17//! else, and any operation that fails, is unsupported: the engine
18//! enumerates such a program instead, or, with `Symbolic::Only`, says what
19//! isn't supported.
20
21mod bdd;
22
23use crate::dist::{Budget, Dist};
24use crate::error::{OpError, OpResult, RuntimeError};
25use crate::ops;
26use crate::report::Sink;
27use crate::value::Value;
28use crate::weight::Weight;
29use bdd::{Bdd, Counts, Manager, Stop};
30use probl_sema::Builtin;
31use probl_sema::ir::{Block, Expr, ExprKind, Lit, Program, SlotId, StmtKind, TypeSpec};
32use probl_syntax::Span;
33use probl_syntax::ast::{BinOp, UnOp};
34use rustc_hash::FxHashMap;
35use std::sync::Arc;
36use std::sync::atomic::{AtomicBool, Ordering};
37
38/// Whether a program is answered with decision diagrams (docs/design/
39/// symbolic-inference.md). Experimental, and off by default.
40#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
41pub enum Symbolic {
42    /// Enumerate worlds.
43    #[default]
44    Off,
45    /// Use decision diagrams for the programs they support, and enumerate
46    /// the others, and those whose diagrams outgrow `Limits::max_nodes`.
47    Prefer,
48    /// Use decision diagrams, and fail on a program they don't support.
49    Only,
50}
51
52/// The size of a run's decision diagrams.
53#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
54pub struct Diagrams {
55    /// One for each trial that wasn't certain.
56    pub variables: u64,
57    pub nodes: u64,
58}
59
60/// What the diagrams found: what enumeration would have.
61pub(crate) struct Answer {
62    pub sinks: Vec<Sink>,
63    /// The weight of the worlds that finish: the evidence.
64    pub finished: Weight,
65    /// Whether an `observe` was reached.
66    pub observed: bool,
67    /// The last `observe` that ruled out a world.
68    pub last_ruling_out: Option<Span>,
69    pub diagrams: Diagrams,
70}
71
72/// Why diagrams didn't answer.
73pub(crate) enum Fallback {
74    /// The program uses something they don't support.
75    Unsupported(RuntimeError),
76    /// They would have more nodes than allowed.
77    TooLarge(RuntimeError),
78    /// The run stops: it was cancelled.
79    Stopped(RuntimeError),
80}
81
82fn unsupported(what: impl std::fmt::Display, span: Span) -> Fallback {
83    Fallback::Unsupported(
84        OpError::unsupported(format!("{what} isn't supported by the symbolic backend"))
85            .help("it's experimental: it supports draws from Boolean laws like `bernoulli(30%)`, booleans, `if`, `observe`, `score` and reports without `by`, at the top level")
86            .at(span),
87    )
88}
89
90/// Answer `program` with decision diagrams of at most `max_nodes` nodes.
91pub(crate) fn run(
92    program: &Program,
93    budget: Budget,
94    max_nodes: usize,
95    cancel: Option<Arc<AtomicBool>>,
96) -> Result<Answer, Fallback> {
97    let main = program.main();
98    check_block(&main.body)?;
99    let mut run = Run {
100        dd: Manager::new(max_nodes, cancel.clone()),
101        weights: Vec::new(),
102        slots: vec![Sym::Unset; main.n_slots()],
103        log: Vec::new(),
104        evidence: Bdd::TRUE,
105        observed: false,
106        last_ruling_out: None,
107        sinks: vec![Sink::default(); program.reports.len()],
108        counts: Counts::default(),
109        budget,
110        cancel,
111        max_nodes,
112    };
113    run.block(&main.body, Bdd::TRUE)?;
114    let (finished, _) = run.dd.count(run.evidence, &run.weights, &mut run.counts);
115    Ok(Answer {
116        sinks: run.sinks,
117        finished,
118        observed: run.observed,
119        last_ruling_out: run.last_ruling_out,
120        diagrams: Diagrams {
121            variables: run.dd.vars() as u64,
122            nodes: run.dd.nodes() as u64,
123        },
124    })
125}
126
127// ── What's supported ─────────────────────────────────────────────────────
128
129/// Whether a block uses only what diagrams support, checked before running
130/// it. Running it can still find values they don't, like a probability out
131/// of range.
132fn check_block(block: &Block) -> Result<(), Fallback> {
133    for stmt in &block.stmts {
134        let span = stmt.span;
135        match &stmt.kind {
136            StmtKind::Set { place, value }
137            | StmtKind::Update { place, value, .. }
138            | StmtKind::Draw { place, dist: value } => {
139                if !place.path.is_empty() {
140                    return Err(unsupported("assigning part of a variable", span));
141                }
142                check_expr(value)?;
143            }
144            StmtKind::If { cond, then, otherwise } => {
145                check_expr(cond)?;
146                check_block(then)?;
147                check_block(otherwise)?;
148            }
149            StmtKind::Observe { value, from } => {
150                check_expr(value)?;
151                from.iter().try_for_each(check_expr)?;
152            }
153            StmtKind::Report { value, key: None, .. } => check_expr(value)?,
154            StmtKind::Report { key: Some(k), .. } => return Err(unsupported("a report with `by`", k.span)),
155            StmtKind::Check { .. } => {}
156            StmtKind::Take { .. } => return Err(unsupported("taking from a bag", span)),
157            StmtKind::Call { .. } => return Err(unsupported("calling a function", span)),
158            StmtKind::Chance { .. } => return Err(unsupported("`chance`", span)),
159            StmtKind::Loop { .. } => return Err(unsupported("a loop", span)),
160            StmtKind::Break | StmtKind::Continue | StmtKind::Return(_) => {
161                return Err(unsupported("leaving a block early", span));
162            }
163            StmtKind::Fail { .. } => return Err(unsupported("an error", span)),
164            StmtKind::Try { .. } => return Err(unsupported("`try`", span)),
165        }
166    }
167    Ok(())
168}
169
170/// The built-ins diagrams support: Boolean laws, and the tests the
171/// lowering of `and` and `or` makes.
172fn supported(b: Builtin) -> bool {
173    matches!(
174        b,
175        Builtin::Bernoulli | Builtin::ScoreLaw | Builtin::BooleanLaw | Builtin::IsTrue | Builtin::IsFalse
176    )
177}
178
179fn check_expr(e: &Expr) -> Result<(), Fallback> {
180    match &e.kind {
181        ExprKind::Lit(Lit::Dice { .. }) => Err(unsupported("dice", e.span)),
182        ExprKind::Lit(Lit::Enum { .. }) => Err(unsupported("an enum", e.span)),
183        ExprKind::Lit(_) | ExprKind::Slot(_) => Ok(()),
184        ExprKind::Unary(UnOp::Typeof, _) => Err(unsupported("`typeof`", e.span)),
185        ExprKind::Unary(_, x) => check_expr(x),
186        ExprKind::Binary(_, a, b) => {
187            check_expr(a)?;
188            check_expr(b)
189        }
190        ExprKind::Builtin { func, args, named } if supported(*func) && named.is_empty() => {
191            args.iter().try_for_each(check_expr)
192        }
193        ExprKind::Builtin { func, .. } => Err(unsupported(format_args!("`{}`", func.name()), e.span)),
194        ExprKind::List(_) | ExprKind::Map(_) | ExprKind::Record { .. } | ExprKind::With(..) => {
195            Err(unsupported("a collection", e.span))
196        }
197        ExprKind::Field(..) | ExprKind::Index(..) => Err(unsupported("a field or an index", e.span)),
198        ExprKind::Closure { .. } | ExprKind::Bind { .. } => Err(unsupported("a function value", e.span)),
199        ExprKind::Simulate { .. } => Err(unsupported("`simulate`", e.span)),
200        ExprKind::Interp(_) => Err(unsupported("string interpolation", e.span)),
201        ExprKind::Input(_) => Err(unsupported("data", e.span)),
202    }
203}
204
205// ── Running ──────────────────────────────────────────────────────────────
206
207/// A variable's value in every world on the current path.
208#[derive(Clone, Debug, PartialEq)]
209enum Sym {
210    /// Not assigned on this path.
211    Unset,
212    Bool(Bdd),
213    /// A value other than a Boolean in each set of worlds: a probability, a
214    /// law… The sets don't overlap, and together they're every world where
215    /// the variable is assigned. A constant is one value in every world.
216    Values(Vec<(Bdd, Value)>),
217    /// A Boolean on some paths, and another value on others.
218    Mixed,
219}
220
221impl Sym {
222    fn fact(b: bool) -> Sym {
223        Sym::Bool(if b { Bdd::TRUE } else { Bdd::FALSE })
224    }
225
226    fn constant(v: Value) -> Sym {
227        Sym::Values(vec![(Bdd::TRUE, v)])
228    }
229}
230
231struct Run {
232    dd: Manager,
233    /// Each variable's weight when false and when true.
234    weights: Vec<(Weight, Weight)>,
235    slots: Vec<Sym>,
236    /// What each assignment replaced, oldest first, to undo a branch.
237    log: Vec<(SlotId, Sym)>,
238    evidence: Bdd,
239    observed: bool,
240    last_ruling_out: Option<Span>,
241    sinks: Vec<Sink>,
242    counts: Counts,
243    budget: Budget,
244    cancel: Option<Arc<AtomicBool>>,
245    max_nodes: usize,
246}
247
248impl Run {
249    /// Run a block in the worlds where `guard` holds.
250    fn block(&mut self, block: &Block, guard: Bdd) -> Result<(), Fallback> {
251        for stmt in &block.stmts {
252            let span = stmt.span;
253            // Like enumeration, run nothing where no world is left: the
254            // values of the variables don't matter there.
255            if self.dd.and(guard, self.evidence) == Bdd::FALSE {
256                return Ok(());
257            }
258            match &stmt.kind {
259                StmtKind::Set { place, value } | StmtKind::Update { place, value, .. } => {
260                    let v = self.eval(value)?;
261                    self.assign(place.slot, v);
262                }
263                StmtKind::Draw { place, dist } => {
264                    let d = self.eval(dist)?;
265                    let v = self.draw(d, dist.span)?;
266                    self.assign(place.slot, v);
267                }
268                StmtKind::If { cond, then, otherwise } => {
269                    let c = self.eval(cond)?;
270                    let c = self.condition(c, cond.span)?;
271                    self.branch(c, then, otherwise, guard)?;
272                }
273                StmtKind::Observe { value, from } => {
274                    let v = self.eval(value)?;
275                    let Sym::Bool(b) = v else {
276                        return Err(unsupported("observing something other than a boolean", value.span));
277                    };
278                    // The worlds that keep their weight, or part of it, and
279                    // those that are ruled out.
280                    let (kept, ruled_out) = match from {
281                        None => (b, b.not()),
282                        Some(d) => {
283                            let d = self.eval(d)?;
284                            self.likelihood(b, d, span)?
285                        }
286                    };
287                    self.observe(guard, kept, ruled_out, span);
288                }
289                StmtKind::Report { site, value, .. } => {
290                    let v = self.eval(value)?;
291                    self.report(*site as usize, v, guard, value.span)?;
292                }
293                StmtKind::Check { slot, ty } => {
294                    let fits = |v: &Value| {
295                        matches!(
296                            (v, ty),
297                            (Value::Unit, TypeSpec::Unit)
298                                | (Value::Int(_), TypeSpec::Int)
299                                | (Value::Float(_), TypeSpec::Float)
300                                | (Value::Prob(_), TypeSpec::Prob)
301                                | (Value::Str(_), TypeSpec::Str)
302                        )
303                    };
304                    let ok = match (&self.slots[*slot as usize], ty) {
305                        (Sym::Bool(_), TypeSpec::Bool) => true,
306                        (Sym::Values(vs), _) => vs.iter().all(|(_, v)| fits(v)),
307                        _ => false,
308                    };
309                    if !ok {
310                        return Err(unsupported("this type check", span));
311                    }
312                }
313                _ => unreachable!("checked before running"),
314            }
315            self.check(span)?;
316        }
317        Ok(())
318    }
319
320    /// Stop if the diagrams outgrew their budget, or the run was cancelled.
321    fn check(&self, span: Span) -> Result<(), Fallback> {
322        let cancelled = || self.cancel.as_ref().is_some_and(|c| c.load(Ordering::Relaxed));
323        match self.dd.stopped() {
324            Some(Stop::TooLarge) => Err(Fallback::TooLarge(RuntimeError::limit(
325                span,
326                format!("the decision diagrams would need more than {} nodes", self.max_nodes),
327            ))),
328            Some(Stop::Cancelled) => Err(Fallback::Stopped(RuntimeError::limit(span, "the run was cancelled"))),
329            None if cancelled() => Err(Fallback::Stopped(RuntimeError::limit(span, "the run was cancelled"))),
330            None => Ok(()),
331        }
332    }
333
334    fn assign(&mut self, slot: SlotId, v: Sym) {
335        let old = std::mem::replace(&mut self.slots[slot as usize], v);
336        self.log.push((slot, old));
337    }
338
339    /// `if c`: each branch in its worlds, and then each variable either
340    /// branch assigned is one or the other, as `c` says.
341    fn branch(&mut self, c: Bdd, then: &Block, otherwise: &Block, guard: Bdd) -> Result<(), Fallback> {
342        let yes = self.dd.and(guard, c);
343        let no = self.dd.and(guard, c.not());
344        // Enumeration runs a branch only if a world gets there.
345        let reaches = |run: &mut Run, path: Bdd| run.dd.and(path, run.evidence) != Bdd::FALSE;
346        let (go_then, go_else) = (reaches(self, yes), reaches(self, no));
347        if !go_then || !go_else {
348            // The variables of the other branch's worlds don't matter: it
349            // has none.
350            if go_then {
351                self.block(then, yes)?;
352            } else if go_else {
353                self.block(otherwise, no)?;
354            }
355            return Ok(());
356        }
357        let mark = self.log.len();
358        self.block(then, yes)?;
359        // What the first branch left, and the values before it, back.
360        let mut after_then: FxHashMap<SlotId, Sym> = FxHashMap::default();
361        for (slot, _) in &self.log[mark..] {
362            after_then
363                .entry(*slot)
364                .or_insert_with(|| self.slots[*slot as usize].clone());
365        }
366        for (slot, old) in self.log.drain(mark..).rev() {
367            self.slots[slot as usize] = old;
368        }
369        self.block(otherwise, no)?;
370        let mut touched: Vec<SlotId> = self.log[mark..].iter().map(|(s, _)| *s).collect();
371        touched.extend(after_then.keys());
372        touched.sort_unstable();
373        touched.dedup();
374        for slot in touched {
375            // Before the branches: what the second one replaced first, or
376            // what's there if it didn't assign it.
377            let before = self.log[mark..]
378                .iter()
379                .find(|(s, _)| *s == slot)
380                .map(|(_, old)| old.clone());
381            let then_value = after_then
382                .remove(&slot)
383                .or_else(|| before.clone())
384                .unwrap_or_else(|| self.slots[slot as usize].clone());
385            let else_value = self.slots[slot as usize].clone();
386            let merged = self.merge(c, then_value, else_value);
387            if before.is_none() {
388                self.log.push((slot, self.slots[slot as usize].clone()));
389            }
390            self.slots[slot as usize] = merged;
391        }
392        Ok(())
393    }
394
395    /// `c ? a : b`.
396    fn merge(&mut self, c: Bdd, a: Sym, b: Sym) -> Sym {
397        match (a, b) {
398            (a, b) if a == b => a,
399            (Sym::Unset, x) | (x, Sym::Unset) => x,
400            (Sym::Bool(a), Sym::Bool(b)) => Sym::Bool(self.dd.ite(c, a, b)),
401            (Sym::Values(a), Sym::Values(b)) => {
402                let mut parts = Vec::with_capacity(a.len() + b.len());
403                for (g, v) in a {
404                    parts.push((self.dd.and(c, g), v));
405                }
406                for (g, v) in b {
407                    parts.push((self.dd.and(c.not(), g), v));
408                }
409                Sym::Values(self.gather(parts))
410            }
411            _ => Sym::Mixed,
412        }
413    }
414
415    /// Values by set of worlds, each value once, without empty sets.
416    fn gather(&mut self, parts: Vec<(Bdd, Value)>) -> Vec<(Bdd, Value)> {
417        let mut out: Vec<(Bdd, Value)> = Vec::with_capacity(parts.len());
418        for (g, v) in parts {
419            if g == Bdd::FALSE {
420                continue;
421            }
422            match out.iter_mut().find(|(_, x)| *x == v) {
423                Some((h, _)) => *h = self.dd.or(*h, g),
424                None => out.push((g, v)),
425            }
426        }
427        out
428    }
429
430    /// The values of `f` applied to each value, in the same worlds.
431    fn map(
432        &mut self,
433        vs: Vec<(Bdd, Value)>,
434        span: Span,
435        f: impl Fn(&Value, &mut Budget) -> OpResult<Value>,
436    ) -> Result<Sym, Fallback> {
437        let mut parts = Vec::with_capacity(vs.len());
438        for (g, v) in vs {
439            match f(&v, &mut self.budget) {
440                Ok(x) => parts.push((g, x)),
441                Err(_) => return Err(unsupported("an operation that fails", span)),
442            }
443        }
444        self.values(parts, span)
445    }
446
447    /// Values as a variable holds them: Booleans as the worlds where
448    /// they're true.
449    fn values(&mut self, parts: Vec<(Bdd, Value)>, span: Span) -> Result<Sym, Fallback> {
450        let booleans = parts.iter().filter(|(_, v)| matches!(v, Value::Bool(_))).count();
451        if booleans == 0 {
452            if parts.iter().any(|(_, v)| !plain(v)) {
453                return Err(unsupported("this value", span));
454            }
455            return Ok(Sym::Values(self.gather(parts)));
456        }
457        if booleans < parts.len() {
458            return Err(unsupported(
459                "a value that's a boolean in some worlds and not in others",
460                span,
461            ));
462        }
463        let mut b = Bdd::FALSE;
464        for (g, v) in parts {
465            if v == Value::Bool(true) {
466                b = self.dd.or(b, g);
467            }
468        }
469        Ok(Sym::Bool(b))
470    }
471
472    /// A variable for a fresh trial with these weights, or a constant if
473    /// it's certain.
474    fn trial(&mut self, no: f64, yes: f64) -> Bdd {
475        if yes <= 0.0 {
476            return Bdd::FALSE;
477        }
478        if no <= 0.0 {
479            return Bdd::TRUE;
480        }
481        self.weights.push((Weight::new(no), Weight::new(yes)));
482        self.dd.var()
483    }
484
485    /// A fresh trial from a law of booleans (or a probability, drawn as
486    /// `bernoulli(p)`).
487    fn draw_law(&mut self, law: &Value, span: Span) -> Result<Bdd, Fallback> {
488        let d = match law {
489            Value::Prob(p) => Arc::new(Dist::bernoulli(*p)),
490            Value::Dist(d) => d.clone(),
491            _ => return Err(unsupported("drawing from this", span)),
492        };
493        if d.missing > 0.0 {
494            return Err(unsupported("a distribution with unresolved probability", span));
495        }
496        let (mut no, mut yes) = (0.0, 0.0);
497        for (v, p) in &d.outcomes {
498            match v {
499                Value::Bool(false) => no = *p,
500                Value::Bool(true) => yes = *p,
501                _ => return Err(unsupported("drawing values other than booleans", span)),
502            }
503        }
504        Ok(self.trial(no, yes))
505    }
506
507    /// `x ~ d`: in each set of worlds, a fresh trial of its law.
508    fn draw(&mut self, d: Sym, span: Span) -> Result<Sym, Fallback> {
509        match d {
510            Sym::Values(laws) => {
511                let mut b = Bdd::FALSE;
512                for (g, law) in laws {
513                    let t = self.draw_law(&law, span)?;
514                    let here = self.dd.and(g, t);
515                    b = self.dd.or(b, here);
516                }
517                Ok(Sym::Bool(b))
518            }
519            // A value that isn't a distribution is its only outcome.
520            Sym::Bool(_) => Ok(d),
521            _ => Err(unsupported(
522                "drawing from a variable whose value differs between paths",
523                span,
524            )),
525        }
526    }
527
528    /// The worlds where a condition holds. A probability, or a law of
529    /// booleans, is a fresh trial each time (docs/semantics.md, section 3).
530    fn condition(&mut self, c: Sym, span: Span) -> Result<Bdd, Fallback> {
531        match c {
532            Sym::Bool(b) => Ok(b),
533            Sym::Values(vs) => {
534                let mut b = Bdd::FALSE;
535                for (g, v) in vs {
536                    let c = ops::condition(&v).map_err(|_| unsupported("this condition", span))?;
537                    if c.missing > 0.0 {
538                        return Err(unsupported("a condition with unresolved probability", span));
539                    }
540                    let t = self.trial(c.no, c.yes);
541                    let here = self.dd.and(g, t);
542                    b = self.dd.or(b, here);
543                }
544                Ok(b)
545            }
546            _ => Err(unsupported("a variable whose value differs between paths", span)),
547        }
548    }
549
550    /// `observe b from d`: the worlds a trial of `d` agrees with `b` in,
551    /// which keep that part of their weight, and those it never could,
552    /// which are ruled out.
553    fn likelihood(&mut self, b: Bdd, d: Sym, span: Span) -> Result<(Bdd, Bdd), Fallback> {
554        let Sym::Values(laws) = d else {
555            return Err(unsupported("observing a value from this", span));
556        };
557        let (mut kept, mut ruled_out) = (Bdd::FALSE, Bdd::FALSE);
558        for (g, law) in laws {
559            if matches!(law, Value::Prob(_)) {
560                // An error, as enumeration says.
561                return Err(unsupported("observing a value from a probability", span));
562            }
563            let t = self.draw_law(&law, span)?;
564            let agrees = self.dd.xor(t, b).not();
565            let here = self.dd.and(g, agrees);
566            kept = self.dd.or(kept, here);
567            // A certain law rules out the worlds that disagree; an
568            // uncertain one only weighs them.
569            if t == Bdd::TRUE || t == Bdd::FALSE {
570                let here = self.dd.and(g, agrees.not());
571                ruled_out = self.dd.or(ruled_out, here);
572            }
573        }
574        Ok((kept, ruled_out))
575    }
576
577    /// The worlds on the path keep only `kept`.
578    fn observe(&mut self, guard: Bdd, kept: Bdd, ruled_out: Bdd, span: Span) {
579        let reached = self.dd.and(guard, self.evidence);
580        if reached == Bdd::FALSE {
581            return;
582        }
583        self.observed = true;
584        if self.dd.and(reached, ruled_out) != Bdd::FALSE {
585            self.last_ruling_out = Some(span);
586        }
587        let others = self.dd.or(guard.not(), kept);
588        self.evidence = self.dd.and(self.evidence, others);
589    }
590
591    /// Add what the worlds on this path report.
592    fn report(&mut self, site: usize, v: Sym, guard: Bdd, span: Span) -> Result<(), Fallback> {
593        let reached = self.dd.and(guard, self.evidence);
594        if reached == Bdd::FALSE {
595            return Ok(());
596        }
597        // The worlds that reach it with each value, counted.
598        let parts = match v {
599            Sym::Bool(b) => vec![(b, Value::Bool(true)), (b.not(), Value::Bool(false))],
600            Sym::Values(vs) => vs,
601            _ => {
602                return Err(unsupported(
603                    "reporting a variable whose value differs between paths",
604                    span,
605                ));
606            }
607        };
608        for (worlds, value) in parts {
609            let mut pairs = FxHashMap::default();
610            let weight = self
611                .dd
612                .count_and(reached, worlds, &self.weights, &mut self.counts, &mut pairs);
613            if weight.is_zero() && !matches!(value, Value::Bool(_)) {
614                continue;
615            }
616            let sink = &self.sinks[site];
617            let valid = sink
618                .validate_analytic(&Value::Unit, &value)
619                .and_then(|()| sink.validate_structure(&Value::Unit, &value));
620            if valid.is_err() {
621                return Err(unsupported("this report", span));
622            }
623            self.sinks[site].add(Value::Unit, &value, weight, None);
624        }
625        Ok(())
626    }
627
628    fn eval(&mut self, e: &Expr) -> Result<Sym, Fallback> {
629        let span = e.span;
630        let varies = || unsupported("a variable whose value differs between paths", span);
631        Ok(match &e.kind {
632            ExprKind::Lit(l) => match literal(l, &mut self.budget) {
633                Ok(Value::Bool(b)) => Sym::fact(b),
634                Ok(v) => Sym::constant(v),
635                Err(_) => return Err(unsupported("this literal", span)),
636            },
637            ExprKind::Slot(s) => match &self.slots[*s as usize] {
638                Sym::Unset | Sym::Mixed => return Err(varies()),
639                v => v.clone(),
640            },
641            ExprKind::Unary(op, x) => match (op, self.eval(x)?) {
642                (UnOp::Not, Sym::Bool(b)) => Sym::Bool(b.not()),
643                (op, Sym::Values(vs)) => self.map(vs, span, |v, budget| ops::unary(*op, v, budget))?,
644                _ => return Err(unsupported("this operation", span)),
645            },
646            ExprKind::Binary(op, a, b) => {
647                let a = self.eval(a)?;
648                let b = self.eval(b)?;
649                match (op, a, b) {
650                    (BinOp::And, Sym::Bool(x), Sym::Bool(y)) => Sym::Bool(self.dd.and(x, y)),
651                    (BinOp::Or, Sym::Bool(x), Sym::Bool(y)) => Sym::Bool(self.dd.or(x, y)),
652                    (BinOp::Eq, Sym::Bool(x), Sym::Bool(y)) => Sym::Bool(self.dd.xor(x, y).not()),
653                    (BinOp::Ne, Sym::Bool(x), Sym::Bool(y)) => Sym::Bool(self.dd.xor(x, y)),
654                    (BinOp::And | BinOp::Or, _, _) => return Err(unsupported("this operation", span)),
655                    (op, Sym::Values(xs), Sym::Values(ys)) => {
656                        let mut parts = Vec::with_capacity(xs.len() * ys.len());
657                        for (g, x) in &xs {
658                            for (h, y) in &ys {
659                                let both = self.dd.and(*g, *h);
660                                if both == Bdd::FALSE {
661                                    continue;
662                                }
663                                match ops::binary(*op, x, y, &mut self.budget) {
664                                    Ok(v) => parts.push((both, v)),
665                                    Err(_) => return Err(unsupported("an operation that fails", span)),
666                                }
667                            }
668                        }
669                        self.values(parts, span)?
670                    }
671                    _ => return Err(unsupported("this operation", span)),
672                }
673            }
674            ExprKind::Builtin { func, args, .. } => {
675                let x = self.eval(&args[0])?;
676                match (func, x) {
677                    (Builtin::IsTrue, Sym::Bool(b)) => Sym::Bool(b),
678                    (Builtin::IsFalse, Sym::Bool(b)) => Sym::Bool(b.not()),
679                    (Builtin::IsTrue | Builtin::IsFalse, Sym::Values(vs)) => {
680                        let truth = *func == Builtin::IsTrue;
681                        self.map(vs, span, |v, _| Ok(Value::Bool(ops::is_certain(v, truth))))?
682                    }
683                    (Builtin::Bernoulli | Builtin::ScoreLaw, Sym::Values(vs)) => {
684                        self.map(vs, span, |p, _| Ok(Dist::bernoulli(ops::to_prob(p)?).into_value()))?
685                    }
686                    (Builtin::BooleanLaw, Sym::Values(vs)) => self.map(vs, span, |v, _| ops::boolean_law(v))?,
687                    (Builtin::BooleanLaw, Sym::Bool(b)) => {
688                        // A fact's law is certain: a trial of it is the fact.
689                        let certain = |b| Value::Dist(Arc::new(Dist::bernoulli(if b { 1.0 } else { 0.0 })));
690                        let parts = vec![(b, certain(true)), (b.not(), certain(false))];
691                        Sym::Values(self.gather(parts))
692                    }
693                    (_, Sym::Unset | Sym::Mixed) => return Err(varies()),
694                    _ => return Err(unsupported("this operation", span)),
695                }
696            }
697            _ => unreachable!("checked before running"),
698        })
699    }
700}
701
702/// A literal's value, as the engine makes it.
703fn literal(l: &Lit, budget: &mut Budget) -> OpResult<Value> {
704    Ok(match l {
705        Lit::Builtin(b) => Value::Builtin(*b),
706        Lit::Unit => Value::Unit,
707        Lit::Bool(b) => Value::Bool(*b),
708        Lit::Int(i) => {
709            budget.integer_bits(i.bits())?;
710            Value::Int(i.clone())
711        }
712        Lit::Float(x) | Lit::FloatConstant(x) => Value::Float(*x),
713        Lit::Prob(p) => Value::Prob(*p),
714        Lit::Str(s) => crate::text::value(s, budget)?,
715        Lit::Dice { .. } | Lit::Enum { .. } => unreachable!("checked before running"),
716    })
717}
718
719/// Whether diagrams can carry a value: not a continuous value, a function
720/// or a law too broad to list.
721fn plain(v: &Value) -> bool {
722    match v {
723        Value::Unit | Value::Bool(_) | Value::Int(_) | Value::Float(_) | Value::Prob(_) | Value::Str(_) => true,
724        Value::Builtin(_) => true,
725        Value::Dist(d) => d.missing == 0.0 && d.outcomes.iter().all(|(v, _)| plain(v)),
726        _ => false,
727    }
728}
probl_engine/symbolic.rs

probl_engine/
symbolic.rs
