ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
GenericCircuit.h
Go to the documentation of this file.
1/**
2 * @file GenericCircuit.h
3 * @brief Semiring-agnostic in-memory provenance circuit.
4 *
5 * @c GenericCircuit is an in-memory directed acyclic graph whose gate
6 * types use the PostgreSQL @c gate_type enumeration. It is built from
7 * the persistent mmap representation (via @c createGenericCircuit() /
8 * @c getGenericCircuit()) and then evaluated over an arbitrary semiring
9 * using the @c evaluate() template method.
10 *
11 * Beyond the gate/wire data inherited from @c Circuit<gate_type>,
12 * @c GenericCircuit tracks:
13 * - Per-gate integer annotation pairs (@c info1, @c info2) used by
14 * aggregation and semimodule gates.
15 * - Per-gate variable-length string extras (e.g. label strings for
16 * @c gate_value gates).
17 * - A probability vector for probabilistic evaluation.
18 * - The set of input gate IDs (for semiring evaluation traversal).
19 *
20 * The circuit is Boost-serialisable, which is used when sending it as
21 * a blob to an external knowledge-compiler process.
22 */
23#ifndef GENERIC_CIRCUIT_H
24#define GENERIC_CIRCUIT_H
25
26#include <map>
27#include <type_traits>
28
29#include <boost/archive/binary_oarchive.hpp>
30#include <boost/serialization/unordered_map.hpp>
31#include <boost/serialization/map.hpp>
32#include <boost/serialization/set.hpp>
33#include <boost/serialization/vector.hpp>
34
35#include "Circuit.h"
36#include "semiring/Semiring.h"
37
38extern "C" {
39#include "provsql_utils.h"
40}
41
42/**
43 * @brief In-memory provenance circuit with semiring-generic evaluation.
44 *
45 * Gate types are the PostgreSQL @c gate_type values. The circuit is
46 * constructed from the persistent mmap store and then evaluated in-memory.
47 */
48class GenericCircuit : public Circuit<gate_type>
49{
50private:
51std::map<gate_t, std::pair<unsigned,unsigned> > infos; ///< Per-gate (info1, info2) annotations
52std::map<gate_t, std::string> extra; ///< Per-gate string extras
53std::set<gate_t> inputs; ///< Set of input (leaf) gate IDs
54std::vector<double> prob; ///< Per-gate probability values
55std::set<gate_t> boolean_assumed_gates; ///< Side-band Boolean-assumption marker set by the Boolean-only fold rules ; an evaluator visiting a gate in this set refuses to proceed under a semiring that does not admit a homomorphism from Boolean functions. In-memory only ; never persisted to mmap. Distinct from the @c gate_assumed enum (used by the safe-query rewriter to encode the same restriction at the persistent layer).
56std::set<gate_t> absorptive_assumed_gates; ///< Side-band absorptive-assumption marker set by the absorptive fold rules (plus-idempotence, plus-with-one absorber, plus-absorbs-times -- sound in every absorptive semiring) ; an evaluator visiting a gate in this set refuses unless the semiring is absorptive or tolerates the (stronger) Boolean rewrite. In-memory only.
57
58public:
59/**
60 * @brief Return a placeholder debug string (not intended for display).
61 * @param g Gate identifier (unused).
62 * @return Fixed placeholder string @c "<GenericCircuit>".
63 */
64virtual std::string toString(gate_t g) const override {
65 return "<GenericCircuit>";
66}
67
68/**
69 * @brief Set the integer annotation pair for gate @p g.
70 * @param g Gate identifier.
71 * @param info1 First annotation integer.
72 * @param info2 Second annotation integer.
73 */
74void setInfos(gate_t g, unsigned info1, unsigned info2)
75{
76 infos[g]=std::make_pair(info1, info2);
77}
78
79/**
80 * @brief Return the integer annotation pair for gate @p g.
81 * @param g Gate identifier.
82 * @return @c {info1, info2}, or @c {-1,-1} if not set.
83 */
84std::pair<unsigned,unsigned> getInfos(gate_t g) const
85{
86 auto it = infos.find(g);
87 if(it==infos.end())
88 return std::make_pair(-1, -1);
89 return it->second;
90}
91
92/**
93 * @brief Attach a string extra to gate @p g.
94 * @param g Gate identifier.
95 * @param ex String to store.
96 */
97void setExtra(gate_t g, const std::string &ex)
98{
99 extra[g]=ex;
100}
101
102/**
103 * @brief Return the string extra for gate @p g.
104 * @param g Gate identifier.
105 * @return The stored string, or empty if not set.
106 */
107std::string getExtra(gate_t g) const
108{
109 auto it = extra.find(g);
110 if(it==extra.end())
111 return "";
112 else
113 return it->second;
114}
115
116/** @copydoc Circuit::addGate() */
117gate_t addGate() override;
118/** @copydoc Circuit::setGate(gateType) */
119gate_t setGate(gate_type type) override;
120/** @copydoc Circuit::setGate(const uuid&, gateType) */
121gate_t setGate(const uuid &u, gate_type type) override;
122
123/**
124 * @brief Return the set of input (leaf) gates.
125 * @return Const reference to the set of input gate identifiers.
126 */
127const std::set<gate_t> &getInputs() const {
128 return inputs;
129}
130
131/**
132 * @brief Set the probability for gate @p g.
133 * @param g Gate identifier.
134 * @param p Probability in [0, 1].
135 */
136void setProb(gate_t g, double p) {
137 prob[static_cast<std::underlying_type<gate_t>::type>(g)]=p;
138}
139
140/**
141 * @brief Return the probability for gate @p g.
142 * @param g Gate identifier.
143 * @return The stored probability.
144 */
145double getProb(gate_t g) const {
146 return prob[static_cast<std::underlying_type<gate_t>::type>(g)];
147}
148
149/**
150 * @brief Replace a @c gate_cmp by a constant Boolean leaf
151 * (@c gate_one for @p p == 1, @c gate_zero for @p p == 0)
152 * or by a Bernoulli @c gate_input for any other @p p.
153 *
154 * Used by peephole pruning passes when a comparator's probability is
155 * provably 0, 1, or a closed-form value. Distinguishing the
156 * 0 / 1 case from the fractional case matters because non-probabilistic
157 * semirings (e.g. @c sr_formula, @c sr_counting) have well-defined
158 * @c zero() / @c one() values but no notion of "Bernoulli with
159 * probability @c p" &ndash; an unknown @c gate_input would default
160 * to @c semiring.one() in every semiring (per
161 * @c GenericCircuit::evaluate), which is wrong for an
162 * always-false comparator. Using @c gate_zero / @c gate_one
163 * directly is universally correct: every semiring knows its
164 * identities.
165 *
166 * Fractional probabilities are still encoded as @c gate_input + a
167 * probability so probability evaluators (MC, independent, treedec,
168 * d-DNNF, d4) can consume them, but only those evaluators handle
169 * non-trivial probabilities meaningfully. Such resolutions should
170 * therefore be confined to passes invoked from a probability
171 * context (not the universal @c getGenericCircuit-time pass).
172 *
173 * Operates on the in-memory circuit only; the persistent mmap store
174 * is never mutated. Children that become orphaned are not reaped
175 * here.
176 */
177void resolveCmpToBernoulli(gate_t g, double p) {
178 if (p == 0.0) {
180 } else if (p == 1.0) {
182 } else {
184 setProb(g, p);
185 inputs.insert(g);
186 }
187 getWires(g).clear();
188 infos.erase(g);
189 extra.erase(g);
190}
191
192/**
193 * @brief Replace a @c gate_cmp by a @c gate_plus over the given
194 * per-row K-gates (the OR of the agg's row-presence
195 * indicators).
196 *
197 * Used by the probability-side always-true HAVING rewriter
198 * (@c runHavingAlwaysTrueRewriter): when a HAVING predicate is
199 * provably true on the agg's value-interval, the cmp value equals
200 * "the group is non-empty" -- the OR over the agg's K-gates -- not
201 * @c gate_one, which would over-credit the empty world (see
202 * @c decideAggVsConstCmp's doc comment).
203 *
204 * Sound for absorptive semirings where @c gate_plus is idempotent
205 * OR (probability, Boolean, formula, why, which, max-min, max-max);
206 * the call site lives in the probability-evaluate pre-pass for
207 * that reason, mirroring @c resolveCmpToBernoulli with a fractional
208 * probability.
209 *
210 * Same wire/info/extra clearing as @c resolveCmpToBernoulli. No
211 * special-casing for @c ks of size 1: a single-child @c gate_plus is
212 * structurally redundant but semantically equivalent to that child
213 * in every semiring.
214 */
215void resolveCmpToPlusOfKGates(gate_t g, const std::vector<gate_t> &ks) {
217 auto &w = getWires(g);
218 w.clear();
219 w.reserve(ks.size());
220 for (gate_t k : ks) w.push_back(k);
221 infos.erase(g);
222 extra.erase(g);
223}
224
225/**
226 * @brief Replace an arbitrary gate (typically @c gate_times) by
227 * @c gate_zero.
228 *
229 * Used by RangeCheck's joint-conjunction pass when an AND of cmps
230 * over a shared RV constrains its support to an empty interval:
231 * since @c gate_zero is the multiplicative absorber in every
232 * semiring, replacing a @c gate_times with it is universally sound,
233 * and orphans the conjuncts (their effects are now unreachable
234 * from the root, regardless of what each individual cmp would
235 * resolve to).
236 *
237 * The wires, infos and extra fields are cleared so the gate is a
238 * proper leaf. Operates on the in-memory circuit only.
239 */
242 getWires(g).clear();
243 infos.erase(g);
244 extra.erase(g);
245}
246
247/**
248 * @brief Rewrite an arbitrary gate as a @c gate_value carrying the
249 * textual extra @p s.
250 *
251 * Used by the @c HybridEvaluator simplifier when a @c gate_arith
252 * subtree constant-folds to a scalar. Same wire/info/extra clearing
253 * as @c resolveCmpToBernoulli &ndash; the old children become
254 * orphans relative to @p g. @p s is interpreted by the consumer
255 * via @c parseDoubleStrict (or analogous routines), so it must be
256 * a canonical textual representation that round-trips through
257 * @c std::stod. Operates on the in-memory circuit only.
258 */
259void resolveToValue(gate_t g, const std::string &s) {
261 getWires(g).clear();
262 infos.erase(g);
263 extra[g] = s;
264}
265
266/**
267 * @brief Rewrite an arbitrary gate as a @c gate_rv carrying the
268 * distribution-spec extra @p s.
269 *
270 * Used by the @c HybridEvaluator simplifier when a linear
271 * combination of independent normals (or i.i.d. exponentials with
272 * the same rate) collapses to a single closed-form distribution.
273 * @p s must be a textual encoding parseable by
274 * @c parse_distribution_spec. Same wire/info clearing as
275 * @c resolveCmpToBernoulli. Operates on the in-memory circuit only.
276 */
277void resolveToRv(gate_t g, const std::string &s) {
279 getWires(g).clear();
280 infos.erase(g);
281 extra[g] = s;
282}
283
284/**
285 * @brief Replace a @c gate_conditioned @p g by a transparent passthrough to
286 * its @p target child (a single-child @c gate_arith @c PLUS, i.e. the
287 * sum of one operand = the operand itself).
288 *
289 * Used by the conditional-moment evaluator to lift conditioning out of a
290 * scalar arithmetic expression: @c "f(X|A, Y|B)" becomes @c "f(X, Y)" with the
291 * evidence @c A, @c B collected separately and conjoined into the root
292 * conditioning event. The passthrough REFERENCES @p target (it does not copy
293 * it), so a shared @c gate_rv keeps a single sampled draw. Operates on the
294 * in-memory circuit only.
295 */
298 auto &w = getWires(g);
299 w.clear();
300 w.push_back(target);
302 extra.erase(g);
303}
304
305/**
306 * @brief Drop semiring identity wires and collapse single-wire
307 * @c gate_times / @c gate_plus to their lone non-identity
308 * child; collapse a @c gate_times containing a @c gate_zero
309 * wire to that absorber.
310 *
311 * Universal rewrite: the multiplicative identity (@c gate_one), the
312 * additive identity (@c gate_zero), and the multiplicative absorber
313 * (@c gate_zero) hold across every provsql semiring, so a single
314 * pass after @c RangeCheck is sound for every downstream consumer
315 * (probability_evaluate, to_provxml, view_circuit, Studio's
316 * simplified subgraph). Does NOT apply the additive absorber
317 * rewrite (@c plus-with-one): @c gate_one only absorbs in
318 * idempotent semirings (Boolean, MinMax), so applying it
319 * unconditionally would silently change the semantics for
320 * @c Counting / @c Formula / etc.
321 *
322 * A collapsed gate is not mutated to carry its target's content;
323 * instead every parent wire is rewired straight to the target and the
324 * UUID-to-@c gate_t map is re-pointed so a gate resolved by UUID
325 * (notably the caller-supplied root) follows the collapse. This keeps
326 * a shared leaf a single gate: copying a shared @c gate_input's
327 * content into the collapsed gate under a fresh UUID would mint an
328 * independent duplicate of that Bernoulli variable and over-count the
329 * probability of any non-read-once circuit.
330 *
331 * Operates on the in-memory circuit only; the persistent mmap store
332 * is never touched. Gated alongside @c RangeCheck by
333 * @c provsql.simplify_on_load.
334 *
335 * @return @c true if any phase mutated the circuit (so callers, notably
336 * @c foldBooleanIdentities, can drive a joint fixpoint).
337 */
339
340/**
341 * @brief Apply the Boolean-only AND the absorptive simplification rules
342 * to @c gate_plus and @c gate_times, to a joint fixpoint with
343 * @c foldSemiringIdentities.
344 *
345 * The rule set splits by the semiring class that justifies each rule:
346 *
347 * - @b Absorptive @b rules (sound in every absorptive semiring,
348 * i.e. whenever @f$1 \oplus a = 1@f$; gates marked
349 * absorptive-assumed):
350 * plus-idempotence @c gate_plus(a, a, b) → @c gate_plus(a, b)
351 * (@f$a \oplus a = a \oplus a \cdot 1 = a@f$);
352 * plus-with-one absorber @c gate_plus(…, @c gate_one, …) →
353 * @c gate_one; plus-absorbs-times
354 * @c gate_plus(x, gate_times(x, y, …), …) → @c gate_plus(x, …)
355 * (@f$a \oplus a b = a@f$, the defining identity).
356 * - @b Boolean-only @b rules (gates marked Boolean-assumed):
357 * times-idempotence @c gate_times(a, a, b) → @c gate_times(a, b)
358 * (fails in tropical: @f$a + a = 2a@f$); times-absorbs-plus
359 * @c gate_times(x, gate_plus(x, y, …), …) → @c gate_times(x, …)
360 * (the lattice dual, also unsound in tropical).
361 *
362 * Operates on the in-memory @c GenericCircuit only ; the persistent
363 * mmap store is never mutated, and the gate's UUID-to-@c gate_t
364 * mapping survives so callers indexing by the original UUID still
365 * find it. Interleaves the rule sweep (@c applyFoldRuleSweep) with
366 * @c foldSemiringIdentities to a JOINT fixpoint, so an absorption
367 * whose dominating literal is only exposed by a single-wire collapse
368 * still fires; the result is a circuit on which no enabled rule
369 * applies.
370 */
372
373/**
374 * @brief Absorptive-rules-only variant of @c foldBooleanIdentities():
375 * the joint fixpoint of the absorptive fold rules with
376 * @c foldSemiringIdentities, leaving the Boolean-only rules
377 * (times-idempotence, times-absorbs-plus) unapplied. Used at
378 * circuit-load time under the @c 'absorptive' provenance class.
379 */
381
382/**
383 * @brief One pass of the fold rules over every @c gate_plus /
384 * @c gate_times.
385 *
386 * Helper for the joint-fixpoint loops : applies each enabled rule in
387 * place, marking touched gates absorptive- or Boolean-assumed
388 * according to which rule fired, and reports whether any rule fired so
389 * the caller knows whether to iterate. Not a fixpoint on its own (it
390 * does a single sweep).
391 *
392 * @param boolean_level Also apply the Boolean-only rules.
393 * @return @c true if any rule fired during the sweep.
394 */
395bool applyFoldRuleSweep(bool boolean_level);
396
397/**
398 * @brief Mark gate @p g as Boolean-assumed (in-memory side band).
399 * Visited by every @c evaluate<S> traversal : if @p g is in
400 * the set, the visit checks @c S::compatibleWithBooleanRewrite
401 * and throws a @c CircuitException otherwise.
402 */
404
405/** @brief Report whether @p g carries the Boolean-assumption flag. */
407 return boolean_assumed_gates.count(g) > 0;
408}
409
410/**
411 * @brief Mark gate @p g as absorptive-assumed (in-memory side band).
412 * Visited by every @c evaluate<S> traversal : if @p g is in
413 * the set, the visit requires @c S::absorptive() or
414 * @c S::compatibleWithBooleanRewrite() (a semiring tolerating
415 * the stronger Boolean rewrite tolerates the weaker absorptive
416 * one) and throws a @c CircuitException otherwise.
417 */
419
420/** @brief Report whether @p g carries the absorptive-assumption flag. */
422 return absorptive_assumed_gates.count(g) > 0;
423}
424
425/**
426 * @brief Replace the wires of @p g with @p w.
427 *
428 * Used by the @c HybridEvaluator simplifier's identity-element drop
429 * to remove constant-zero wires from a @c PLUS gate (or constant-one
430 * wires from a @c TIMES gate) without changing the gate's type.
431 * Dropped children become orphans relative to @p g.
432 */
433void setWires(gate_t g, std::vector<gate_t> w) {
434 getWires(g) = std::move(w);
435}
436
437/**
438 * @brief Rewrite an arbitrary gate as a @c gate_plus over @p w.
439 *
440 * Used by the @c HybridEvaluator multi-cmp island decomposer when
441 * a comparator from a shared-island group is rewritten as the OR
442 * of the joint-table @c gate_mulinput leaves where the comparator's
443 * bit is set. Clears infos and extra and installs the new wires.
444 */
445void resolveToPlus(gate_t g, std::vector<gate_t> w) {
447 getWires(g) = std::move(w);
448 infos.erase(g);
449 extra.erase(g);
450}
451
452/**
453 * @brief Allocate a fresh @c gate_input gate carrying probability
454 * @p p, with a unique synthetic UUID so subsequent
455 * @c BooleanCircuit conversion does not collide multiple
456 * no-UUID inputs onto the same gate.
457 *
458 * The synthetic UUID is derived from the freshly-assigned gate id;
459 * it is not a real v4 UUID (does not match the @c xxxxxxxx-...
460 * format) and exists only for in-memory uniqueness during the
461 * probability_evaluate pipeline. The gate is added to @c inputs
462 * so the conversion's first loop maps it into @c BooleanCircuit's
463 * @c gc_to_bc.
464 *
465 * @param p Probability for the new input.
466 * @return The id of the new gate.
467 */
469 gate_t id = addGate();
471 setProb(id, p);
472 std::string u = "dec-in-" + std::to_string(static_cast<size_t>(id));
473 uuid2id[u] = id;
474 id2uuid[id] = u;
475 inputs.insert(id);
476 return id;
477}
478
479/**
480 * @brief Allocate a fresh @c gate_mulinput gate with key @p key,
481 * probability @p p, and value index @p value_index.
482 *
483 * Used by the joint-table decomposer to materialise one Bernoulli
484 * outcome of a 2^k-way categorical distribution over a shared
485 * continuous island. All mulinputs in one joint table share the
486 * same @p key (the block anchor returned by @c addAnonymousInputGate);
487 * @p value_index is stored in @c info1 so
488 * @c BooleanCircuit::independentEvaluation can group / dedup
489 * MULIN references at OR sites. A unique synthetic UUID is
490 * minted for the same reason as @c addAnonymousInputGate.
491 */
493 unsigned value_index) {
494 gate_t id = addGate();
496 setProb(id, p);
497 setInfos(id, value_index, 0);
498 getWires(id).push_back(key);
499 std::string u = "dec-mul-" + std::to_string(static_cast<size_t>(id));
500 uuid2id[u] = id;
501 id2uuid[id] = u;
502 return id;
503}
504
505/**
506 * @brief Allocate a fresh @c gate_arith gate with operator tag @p op
507 * and the given @p wires.
508 *
509 * Used by the @c HybridEvaluator simplifier's mixture-lift rule when
510 * pushing a @c PLUS / @c TIMES inside a mixture's two scalar branches:
511 * each branch needs a fresh @c gate_arith child carrying the lifted
512 * operation, and those children must round-trip through downstream
513 * @c id2uuid / @c uuid2id lookups (Studio's simplified subgraph,
514 * @c to_provxml). A unique synthetic UUID is minted for the same
515 * reason as @c addAnonymousInputGate.
516 */
518 std::vector<gate_t> wires_) {
519 gate_t id = addGate();
521 setInfos(id, static_cast<int>(op), 0);
522 getWires(id) = std::move(wires_);
523 std::string u = "dec-arith-" + std::to_string(static_cast<size_t>(id));
524 uuid2id[u] = id;
525 id2uuid[id] = u;
526 return id;
527}
528
529/**
530 * @brief Allocate a fresh @c gate_value gate carrying the textual
531 * scalar @p text.
532 *
533 * Used by the @c HybridEvaluator simplifier's PLUS coefficient
534 * aggregation rule: when same-RV terms in a @c PLUS gate are merged
535 * into <tt>arith(TIMES, value:a_total, Z)</tt> per RV, each
536 * coefficient @c a_total needs a fresh @c gate_value to feed the
537 * synthetic @c TIMES. @p text must be a canonical text form that
538 * round-trips through @c parseDoubleStrict (the simplifier already
539 * formats with precision 17). A unique synthetic UUID is minted for
540 * the same reason as @c addAnonymousInputGate.
541 */
542gate_t addAnonymousValueGate(const std::string &text) {
543 gate_t id = addGate();
545 setExtra(id, text);
546 std::string u = "dec-value-" + std::to_string(static_cast<size_t>(id));
547 uuid2id[u] = id;
548 id2uuid[id] = u;
549 return id;
550}
551
552/**
553 * @brief Rewrite @p g in place as a @c gate_mixture over the wires
554 * @c [p_token, x_token, y_token].
555 *
556 * Used by the @c HybridEvaluator simplifier's mixture-lift rule when
557 * a @c gate_arith containing a single @c gate_mixture child is pushed
558 * inside the mixture's branches: the outer arith gate is rewritten in
559 * place as the lifted mixture, preserving its UUID and the
560 * non-mixture-aware code paths that already hold references to it.
561 * The @p p_token is reused verbatim so Bernoulli identity is
562 * preserved across the rewrite; the @p x_token and @p y_token are
563 * the freshly-minted arith children built via
564 * @c addAnonymousArithGate.
565 */
567 gate_t x_token, gate_t y_token) {
569 std::vector<gate_t> w;
570 w.reserve(3);
571 w.push_back(p_token);
572 w.push_back(x_token);
573 w.push_back(y_token);
574 getWires(g) = std::move(w);
575 infos.erase(g);
576 extra.erase(g);
577}
578
579/**
580 * @brief Allocate a fresh @c gate_mulinput labelled with a numeric
581 * outcome value carried in @c extra.
582 *
583 * Variant of @c addAnonymousMulinputGate used by the categorical
584 * mixture lowering: the mulinput's @c info1 still holds the ordinal
585 * @p value_index for @c independentEvaluation's dedup, and the
586 * outcome's numeric label is stored in @c extra so the evaluator-side
587 * categorical-mixture handlers can read it as a @c float8.
588 */
590 unsigned value_index,
591 const std::string &value_text) {
592 gate_t id = addAnonymousMulinputGate(key, p, value_index);
593 setExtra(id, value_text);
594 return id;
595}
596
597/**
598 * @brief Rewrite @p g in place as a categorical-form @c gate_mixture
599 * over @p wires (@c [key, mul_1, ..., mul_n]).
600 *
601 * Used by the explicit @c provsql.categorical constructor (built at
602 * SQL-call time, not by the simplifier): the @c gate_mixture type is
603 * reused with @c N > 3 wires, where @c wires[0] is a fresh
604 * @c gate_input "key" anchor (its own probability is irrelevant: the
605 * categorical mass is on the mulinputs) and @c wires[1..n] are
606 * @c gate_mulinput leaves sharing that key. Every @c gate_mixture
607 * handler downstream branches on <tt>wires.size() == 3</tt> for the
608 * classic <tt>[p_token, x_token, y_token]</tt> shape vs the
609 * categorical shape; the latter is what unlocks closed-form CDF /
610 * cmp evaluation via @c AnalyticEvaluator.
611 */
612void resolveToCategoricalMixture(gate_t g, std::vector<gate_t> wires_) {
614 getWires(g) = std::move(wires_);
615 infos.erase(g);
616 extra.erase(g);
617}
618
619/**
620 * @brief Test whether @p g is a categorical-form @c gate_mixture
621 * (the explicit @c provsql.categorical output).
622 *
623 * Returns true iff @p g is a @c gate_mixture whose wires are
624 * @c [key, mul_1, ..., mul_n] with @p n &ge; 1: @c wires[0] a
625 * @c gate_input key anchor, and every subsequent wire a
626 * @c gate_mulinput. The classic mixture shape
627 * @c [p_token, x_token, y_token] returns false (one or both of
628 * @c wires[1..2] are not @c gate_mulinput).
629 */
631{
632 if (getGateType(g) != gate_mixture) return false;
633 const auto &w = getWires(g);
634 if (w.size() < 2) return false;
635 if (getGateType(w[0]) != gate_input) return false;
636 for (std::size_t i = 1; i < w.size(); ++i) {
637 if (getGateType(w[i]) != gate_mulinput) return false;
638 }
639 return true;
640}
641
642/**
643 * @brief Boost serialisation support.
644 * @param ar Boost archive (input or output).
645 * @param version Archive version (unused).
646 */
647template<class Archive>
648void serialize (Archive & ar, const unsigned int version)
649{
650 ar & uuid2id;
651 ar & id2uuid;
652 ar & gates;
653 ar & wires;
654 ar & infos;
655 ar & extra;
656 ar & inputs;
657 ar & prob;
658}
659
662
663/**
664 * @brief Evaluate the sub-circuit rooted at gate @p g over semiring @p semiring.
665 *
666 * Performs a post-order traversal from @p g, mapping each input gate to
667 * its semiring value via @p provenance_mapping, and combining the results
668 * using the semiring operations.
669 *
670 * Every computed gate is memoised into @p provenance_mapping (a gate's
671 * semiring value is a pure function of the gate, so reuse is always
672 * sound): shared sub-DAGs are evaluated once, and gate-creating
673 * semirings (BoolExpr, formula) preserve the sharing structurally.
674 * After the call the mapping therefore covers every visited gate, not
675 * only the pre-seeded inputs.
676 *
677 * @tparam S A concrete @c semiring::Semiring subclass.
678 * @param g Root gate of the sub-circuit to evaluate.
679 * @param provenance_mapping Map from input gate IDs to semiring values;
680 * also serves as the memoisation table.
681 * @param semiring Semiring instance providing @c zero(), @c one(),
682 * @c plus(), @c times(), etc.
683 * @return The semiring value of the circuit at gate @p g.
684 */
685template<typename S, std::enable_if_t<std::is_base_of_v<semiring::Semiring<typename S::value_type>, S>, int> = 0>
686typename S::value_type evaluate(gate_t g, std::unordered_map<gate_t, typename S::value_type> &provenance_mapping, S semiring) const;
687
688};
689
690#endif /* GENERIC_CIRCUIT_H */
Generic directed-acyclic-graph circuit template and gate identifier.
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:49
Abstract semiring interface for provenance evaluation.
Generic template base class for provenance circuits.
Definition Circuit.h:62
std::string uuid
Definition Circuit.h:65
std::vector< gate_t > & getWires(gate_t g)
Definition Circuit.h:140
gate_type getGateType(gate_t g) const
Definition Circuit.h:130
std::unordered_map< gate_t, uuid > id2uuid
Definition Circuit.h:69
std::unordered_map< uuid, gate_t > uuid2id
Definition Circuit.h:68
void setGateType(gate_t g, gate_type t)
Definition Circuit.h:79
std::vector< gate_type > gates
Definition Circuit.h:71
std::vector< std::vector< gate_t > > wires
Definition Circuit.h:72
In-memory provenance circuit with semiring-generic evaluation.
void resolveToPlus(gate_t g, std::vector< gate_t > w)
Rewrite an arbitrary gate as a gate_plus over w.
void resolveToCategoricalMixture(gate_t g, std::vector< gate_t > wires_)
Rewrite g in place as a categorical-form gate_mixture over wires ([key, mul_1, ......
void resolveGateToZero(gate_t g)
Replace an arbitrary gate (typically gate_times) by gate_zero.
void setWires(gate_t g, std::vector< gate_t > w)
Replace the wires of g with w.
std::map< gate_t, std::pair< unsigned, unsigned > > infos
Per-gate (info1, info2) annotations.
void markAbsorptiveAssumed(gate_t g)
Mark gate g as absorptive-assumed (in-memory side band).
void resolveCmpToPlusOfKGates(gate_t g, const std::vector< gate_t > &ks)
Replace a gate_cmp by a gate_plus over the given per-row K-gates (the OR of the agg's row-presence in...
S::value_type evaluate(gate_t g, std::unordered_map< gate_t, typename S::value_type > &provenance_mapping, S semiring) const
Evaluate the sub-circuit rooted at gate g over semiring semiring.
gate_t addAnonymousMulinputGateWithValue(gate_t key, double p, unsigned value_index, const std::string &value_text)
Allocate a fresh gate_mulinput labelled with a numeric outcome value carried in extra.
void resolveToRv(gate_t g, const std::string &s)
Rewrite an arbitrary gate as a gate_rv carrying the distribution-spec extra s.
bool foldSemiringIdentities()
Drop semiring identity wires and collapse single-wire gate_times / gate_plus to their lone non-identi...
void foldAbsorptiveIdentities()
Absorptive-rules-only variant of foldBooleanIdentities(): the joint fixpoint of the absorptive fold r...
void resolveToMixture(gate_t g, gate_t p_token, gate_t x_token, gate_t y_token)
Rewrite g in place as a gate_mixture over the wires [p_token, x_token, y_token].
std::map< gate_t, std::string > extra
Per-gate string extras.
gate_t addGate() override
Allocate a new gate with a default-initialised type.
std::set< gate_t > inputs
Set of input (leaf) gate IDs.
gate_t addAnonymousArithGate(provsql_arith_op op, std::vector< gate_t > wires_)
Allocate a fresh gate_arith gate with operator tag op and the given wires.
gate_t addAnonymousValueGate(const std::string &text)
Allocate a fresh gate_value gate carrying the textual scalar text.
void serialize(Archive &ar, const unsigned int version)
Boost serialisation support.
friend class dDNNFTreeDecompositionBuilder
std::set< gate_t > absorptive_assumed_gates
Side-band absorptive-assumption marker set by the absorptive fold rules (plus-idempotence,...
bool isCategoricalMixture(gate_t g) const
Test whether g is a categorical-form gate_mixture (the explicit provsql.categorical output).
std::vector< double > prob
Per-gate probability values.
void setInfos(gate_t g, unsigned info1, unsigned info2)
Set the integer annotation pair for gate g.
std::string getExtra(gate_t g) const
Return the string extra for gate g.
gate_t setGate(gate_type type) override
Allocate a new gate with type type and no UUID.
void markBooleanAssumed(gate_t g)
Mark gate g as Boolean-assumed (in-memory side band).
std::set< gate_t > boolean_assumed_gates
Side-band Boolean-assumption marker set by the Boolean-only fold rules ; an evaluator visiting a gate...
double getProb(gate_t g) const
Return the probability for gate g.
bool isAbsorptiveAssumed(gate_t g) const
Report whether g carries the absorptive-assumption flag.
void resolveCmpToBernoulli(gate_t g, double p)
Replace a gate_cmp by a constant Boolean leaf (gate_one for p == 1, gate_zero for p == 0) or by a Ber...
gate_t addAnonymousInputGate(double p)
Allocate a fresh gate_input gate carrying probability p, with a unique synthetic UUID so subsequent B...
friend class boost::serialization::access
const std::set< gate_t > & getInputs() const
Return the set of input (leaf) gates.
bool isBooleanAssumed(gate_t g) const
Report whether g carries the Boolean-assumption flag.
std::pair< unsigned, unsigned > getInfos(gate_t g) const
Return the integer annotation pair for gate g.
void liftConditionedToTarget(gate_t g, gate_t target)
Replace a gate_conditioned g by a transparent passthrough to its target child (a single-child gate_ar...
void setExtra(gate_t g, const std::string &ex)
Attach a string extra to gate g.
virtual std::string toString(gate_t g) const override
Return a placeholder debug string (not intended for display).
gate_t addAnonymousMulinputGate(gate_t key, double p, unsigned value_index)
Allocate a fresh gate_mulinput gate with key key, probability p, and value index value_index.
bool applyFoldRuleSweep(bool boolean_level)
One pass of the fold rules over every gate_plus / gate_times.
void resolveToValue(gate_t g, const std::string &s)
Rewrite an arbitrary gate as a gate_value carrying the textual extra s.
void foldBooleanIdentities()
Apply the Boolean-only AND the absorptive simplification rules to gate_plus and gate_times,...
void setProb(gate_t g, double p)
Set the probability for gate g.
Core types, constants, and utilities shared across ProvSQL.
provsql_arith_op
Arithmetic operator tags used by gate_arith.
@ PROVSQL_ARITH_PLUS
n-ary, sum of children
@ gate_rv
Continuous random-variable leaf (extra encodes distribution).
@ gate_mixture
Probabilistic mixture: three wires [p_token (gate_input Bernoulli), x_token, y_token]; samples x when...
@ gate_arith
n-ary arithmetic gate over scalar-valued children (info1 holds operator tag)