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

probl_engine/
symbolic.rs
