ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
probability_evaluate.cpp
Go to the documentation of this file.
1/**
2 * @file probability_evaluate.cpp
3 * @brief SQL function @c provsql.probability_evaluate() – probabilistic circuit evaluation.
4 *
5 * Implements @c provsql.probability_evaluate(), which computes the
6 * probability that a provenance circuit evaluates to @c true under the
7 * tuple-independent probabilistic-database model.
8 *
9 * The @p method argument selects the computation algorithm:
10 * - @c "possible-worlds": exact enumeration of all 2^n worlds.
11 * - @c "monte-carlo": approximate via random sampling (fast, inexact).
12 * - @c "weightmc": approximate using the @c weightmc model counter.
13 * - @c "tree-decomposition": exact via tree-decomposition-based d-DNNF.
14 * - @c "independent": exact evaluation for disconnected circuits.
15 * - @c "inversion-free": exact via the structured-d-DNNF builder over the
16 * query-derived order; errors unless the root carries an inversion-free
17 * certificate. The default method also tries it (after @c "independent")
18 * when a certificate is present.
19 * - Any external compiler name (@c "d4", @c "c2d", @c "minic2d", @c "dsharp").
20 *
21 * A SIGINT signal sets a process-local flag that causes the evaluation
22 * to abort and return @c NULL (used when the user cancels a long-running
23 * probability computation).
24 */
25extern "C" {
26#include "postgres.h"
27#include "fmgr.h"
28#include "catalog/pg_type.h"
29#include "miscadmin.h"
30#include "storage/latch.h"
31#include "utils/uuid.h"
32#include "executor/spi.h"
33#include "provsql_shmem.h"
34#include "provsql_utils.h"
35
36PG_FUNCTION_INFO_V1(probability_evaluate);
37}
38
39#include "c_cpp_compatibility.h"
40#include <set>
41#include <stack>
42#include <map>
43#include <vector>
44#include <algorithm>
45#include <cmath>
46#include <csignal>
47
48#include "BooleanCircuit.h"
49#include "CircuitFromMMap.h"
50#include "GenericCircuit.h"
51#include "AnalyticEvaluator.h"
52#include "CountCmpEvaluator.h"
53#include "HybridEvaluator.h"
54#include "RangeCheck.h"
55#include "MonteCarloSampler.h"
57#include "StructuredDNNF.h"
58#include "having_semantics.hpp"
59#include "provsql_mmap.h"
60#include "safe_query_cert.h"
61#include "provsql_utils_cpp.h"
62#include "tool_registry_sync.h"
63#include "semiring/BoolExpr.h"
64
65using namespace std;
66
67/**
68 * @brief SIGINT handler that sets the global interrupted flag.
69 *
70 * The signal number argument is required by the @c signal() API but is
71 * not used.
72 *
73 * In addition to the @c provsql_interrupted flag polled by the long
74 * Monte-Carlo / possible-worlds evaluation loops, we drive PG's
75 * standard cancel pipeline (@c InterruptPending / @c QueryCancelPending
76 * + @c SetLatch) the same way PG's own @c StatementCancelHandler does.
77 * That makes a SIGINT delivered to the backend (e.g. via
78 * @c pg_cancel_backend) outside of a @c system() wait turn into a
79 * proper 57014 cancel at the next @c CHECK_FOR_INTERRUPTS instead of
80 * being silently absorbed. (The matching case where an external
81 * compiler is running is handled in @c run_external_tool, which runs the
82 * tool in its own process group and @c SIGKILLs that group on a pending
83 * cancel, then lets @c CHECK_FOR_INTERRUPTS raise it.)
84 */
85static void provsql_sigint_handler (int)
86{
88
89 if (!proc_exit_inprogress) {
90 InterruptPending = true;
91 QueryCancelPending = true;
92 }
93 SetLatch(MyLatch);
94}
95
96/**
97 * @brief Collect the inversion-free per-input order keys for the structured
98 * builder.
99 *
100 * Walks the @c GenericCircuit @p gc for @c K-prefixed annotation gates whose
101 * child is a @c gate_input (the per-input order markers attached by the planner
102 * on the certified path), parses each key, and maps the wrapped input to its
103 * @c BooleanCircuit variable via @p gc_to_bc. Returns @c true only if every
104 * @c BooleanCircuit input reachable from @p bc_root carries a key (the
105 * structured builder needs a total order over all variables); a missing marker
106 * means the certified markers are absent / incomplete and the caller must not
107 * use the structured path.
108 */
110 const GenericCircuit &gc, gate_t gc_root,
111 const std::unordered_map<gate_t, gate_t> &gc_to_bc,
112 const BooleanCircuit &c, gate_t bc_root,
113 std::map<gate_t, StructuredDNNFBuilder::InputKey> &out)
114{
115 std::set<gate_t> seen;
116 std::stack<gate_t> st;
117 st.push(gc_root);
118 while (!st.empty()) {
119 gate_t g = st.top(); st.pop();
120 if (!seen.insert(g).second) continue;
121 if (gc.getGateType(g) == gate_annotation) {
122 std::string ex = gc.getExtra(g); // must outlive the parse (k points into it)
123 SafeCertKey k;
124 if (safe_cert_key_parse(ex.c_str(), &k)) {
125 const auto &w = gc.getWires(g);
126 if (!w.empty() && gc.getGateType(w[0]) == gate_input) {
127 auto it = gc_to_bc.find(w[0]);
128 if (it != gc_to_bc.end())
129 out[it->second] = StructuredDNNFBuilder::InputKey{
130 std::string(k.root, k.root_len),
131 std::string(k.sec, k.sec_len), k.factor };
132 }
133 }
134 }
135 for (gate_t ch : gc.getWires(g)) st.push(ch);
136 }
137
138 /* every Boolean input must be ordered */
139 std::set<gate_t> bseen;
140 std::stack<gate_t> bst;
141 bst.push(bc_root);
142 while (!bst.empty()) {
143 gate_t g = bst.top(); bst.pop();
144 if (!bseen.insert(g).second) continue;
145 if (c.getGateType(g) == BooleanGate::IN) {
146 if (out.find(g) == out.end())
147 return false;
148 } else {
149 for (gate_t ch : c.getWires(g)) bst.push(ch);
150 }
151 }
152 return true;
153}
154
155/**
156 * @brief Flatten the per-input order keys into a total rank for the structured
157 * builder's order-only constructor.
158 *
159 * Sorts the certified inputs into a Prop. 4.5-consistent order -- root-class
160 * value first (one independent block per value), then secondary-class value
161 * (one tile per value within a block), then the shared self-join guard before
162 * the payloads of its tile, then by factor -- and assigns consecutive ranks.
163 * Ties (two inputs with identical keys) keep a deterministic order via the
164 * input gate id, so distinct variables always get distinct ranks. Unlike the
165 * keyed (factored-sweep) constructor this makes no single-secondary-axis /
166 * one-payload-per-tile assumption, so it certifies every hierarchical
167 * inversion-free lineage, including the self-join-free case.
168 */
169static std::map<gate_t, int> inversion_free_rank(
170 const std::map<gate_t, StructuredDNNFBuilder::InputKey> &keys)
171{
172 std::vector<std::pair<gate_t, StructuredDNNFBuilder::InputKey>> v(
173 keys.begin(), keys.end());
174 std::sort(v.begin(), v.end(), [](const auto &a, const auto &b) {
175 const auto &ka = a.second, &kb = b.second;
176 if (ka.root != kb.root) return ka.root < kb.root;
177 if (ka.sec != kb.sec) return ka.sec < kb.sec;
178 int ga = (ka.factor == StructuredDNNFBuilder::GUARD_FACTOR) ? 0 : 1;
179 int gb = (kb.factor == StructuredDNNFBuilder::GUARD_FACTOR) ? 0 : 1;
180 if (ga != gb) return ga < gb;
181 if (ka.factor != kb.factor) return ka.factor < kb.factor;
182 return a.first < b.first;
183 });
184 std::map<gate_t, int> rank;
185 int r = 0;
186 for (const auto &p : v) rank[p.first] = r++;
187 return rank;
188}
189
191{
192 // Compile a query certified inversion-free to its structured d-DNNF (the
193 // same artefact the 'inversion-free' probability method builds), so the KC
194 // surface can render / measure it. Mirrors the dispatch in
195 // probability_evaluate_internal: the per-input order keys live on the
196 // GenericCircuit's annotation markers, so we go through the generic circuit
197 // rather than getBooleanCircuit(token, ...) directly.
199 gate_t gc_root = gc.getGate(uuid2string(token));
200 std::string ex = gc.getExtra(gc_root);
201 if (ex.empty() || ex[0] != SAFE_CERT_EXTRA_PREFIX_RECIPE)
202 throw CircuitException("compile 'inversion-free': the provenance root "
203 "carries no inversion-free certificate");
204 gate_t root;
205 std::unordered_map<gate_t, gate_t> gc_to_bc;
206 BooleanCircuit c = getBooleanCircuit(gc, token, root, gc_to_bc);
207 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
208 if (!collect_inversion_free_keys(gc, gc_root, gc_to_bc, c, root, keys))
209 throw CircuitException("compile 'inversion-free': the certificate's inputs "
210 "lack per-input order markers");
211 return StructuredDNNFBuilder(c, root, inversion_free_rank(keys)).dnnf();
212}
213
214/**
215 * @brief Core implementation of probability evaluation for a circuit token.
216 * @param token UUID of the root provenance gate.
217 * @param method Evaluation method name (e.g. "independent", "monte-carlo").
218 * @param args Additional arguments for the chosen method.
219 * @return Float8 Datum containing the computed probability.
220 */
222 (pg_uuid_t token, const string &method, const string &args)
223{
224 // Load the GenericCircuit once: we need it for the RV-detection
225 // dispatch below, and getBooleanCircuit() reuses it internally so we
226 // pay no extra cost compared to the previous flow. Universal
227 // cmp-resolution passes (RangeCheck) have already been applied
228 // inside getGenericCircuit when the provsql.simplify_on_load GUC is
229 // on (the default), so the circuit we receive here is already
230 // peephole-pruned for any "always true / always false" comparator.
232 gate_t gc_root = gc.getGate(uuid2string(token));
233
234 // Inversion-free tractability certificate: the planner wraps the per-row
235 // provenance root in a transparent annotation gate carrying the serialised
236 // SafeCert recipe. Its presence routes the default probability chain through
237 // the structured-d-DNNF builder (after independentEvaluation, before
238 // tree-decomposition) and is required by the explicit 'inversion-free'
239 // method. The recipe is read here (early, before the simplifier passes); the
240 // per-input order keys are collected at the dispatch point, where the
241 // GenericCircuit->BooleanCircuit mapping is available.
242 bool inv_free_cert = false;
243 {
244 std::string ex = gc.getExtra(gc_root);
245 if (!ex.empty() && ex[0] == SAFE_CERT_EXTRA_PREFIX_RECIPE) {
246 SafeCert *cert = safe_cert_parse(ex.c_str());
247 if (cert != nullptr && cert->kind == CERT_INVERSION_FREE) {
248 inv_free_cert = true;
249 // Internal per-evaluation diagnostic (the certificate round-trips from
250 // the planner), not a result-comprehension message: keep it at the
251 // detector's debug-trace level (>= 30) so it stays out of the level-5
252 // floor the Studio eval strip applies.
253 if (provsql_verbose >= 30)
254 provsql_notice("inversion-free certificate read back from circuit "
255 "root: %d atoms, %d classes, root_class=%d",
256 cert->natoms, cert->nclasses, cert->root_class);
257 }
258 }
259 }
260
261 // Hybrid-evaluator simplifier: constant-fold gate_arith subtrees,
262 // drop identity wires (0 from PLUS, 1 from TIMES), and collapse
263 // PLUS over independent normals or i.i.d. exponentials into a
264 // single gate_rv with the closed-form distribution. Gated by
265 // provsql.hybrid_evaluation (default on) so the unfolded DAG can
266 // still be exercised end-to-end through the MC fallback during
267 // A/B-testing. Runs before AnalyticEvaluator so newly-bare normal
268 // / Erlang leaves unlock the closed-form CDF on the surrounding
269 // cmp gate. Runs before a re-pass of RangeCheck so that the
270 // joint-conjunction pass also benefits from constant folding
271 // (e.g. a cmp's `arith(NEG, value:100)` operand becomes a bare
272 // `value:-100` that the asRvVsConstCmp shape match accepts).
276 }
277
278 // Hybrid-evaluator island decomposer: handles continuous-island
279 // comparators by grouping them via base-RV footprint overlap.
280 // Multi-cmp shared-island groups get a joint-distribution table
281 // inlined as a mulinput block - via the monotone-shared-scalar
282 // fast path (k+1 mulinputs; interval probabilities exact via
283 // cdfAt when the shared scalar is a bare gate_rv, MC binning over
284 // k+1 intervals when it is a gate_arith composite) when all cmps
285 // share an lhs gate_t and have gate_value rhs, falling through to
286 // the generic 2^k MC joint table otherwise. Singleton bare-RV
287 // cmps are left for AnalyticEvaluator (closed-form CDF on its own
288 // is cheaper than per-cmp MC); singleton gate_arith cmps get a
289 // per-cmp MC marginalisation here. Either way the rewritten
290 // cmps become gate_plus over mulinputs (or gate_input
291 // Bernoullis), so the surrounding circuit is purely Boolean for
292 // the downstream pass.
293 //
294 // Runs BEFORE AnalyticEvaluator so shared bare-RV cmps reach the
295 // grouping logic - AnalyticEvaluator would otherwise resolve each
296 // independently into a Bernoulli, silently using the independence
297 // approximation on shared base RVs. The trade-off: the fast
298 // path's mulinput block is a dependent circuit that
299 // BooleanCircuit::independentEvaluation rejects when the cmps
300 // combine via AND ('Not an independent circuit'). Callers that
301 // need shared-island dependence handling must use
302 // 'tree-decomposition' / 'monte-carlo' / external compilation;
303 // 'independent' remains correct only for circuits that ARE
304 // independent.
307 gc, static_cast<unsigned>(provsql_rv_mc_samples));
308 }
309
310 // Probability-specific peephole: AnalyticEvaluator decides any
311 // residual continuous-RV comparators the decomposer left alone
312 // (singleton bare gate_rv vs gate_value, or two bare normals) by
313 // replacing them with Bernoulli gate_input gates carrying the
314 // analytical probability. Always sound for probability
315 // evaluation; produces fractional probabilities so it is
316 // meaningful only on this path (not in getGenericCircuit, which
317 // is shared with semiring evaluators).
318 // Count gates reachable from the root before / after the
319 // probability-side pre-pass, so the user can see how much the
320 // shortcut shrank the circuit the downstream method actually sees.
321 auto count_reachable = [&](gate_t r) {
322 std::set<gate_t> seen;
323 std::stack<gate_t> stk;
324 stk.push(r);
325 while (!stk.empty()) {
326 gate_t g = stk.top(); stk.pop();
327 if (!seen.insert(g).second) continue;
328 for (gate_t c : gc.getWires(g)) stk.push(c);
329 }
330 return seen.size();
331 };
332 size_t gates_before = count_reachable(gc_root);
333 unsigned analytic_resolved = provsql::runAnalyticEvaluator(gc);
334
335 /* Closed-form cmp-probability evaluators. First implementation
336 * is the Poisson-binomial pre-pass for HAVING COUNT(*) op C over
337 * distinct gate_input leaves ; future MIN / MAX / SUM resolvers
338 * will run from the same hook. Each replaces a matched gate_cmp
339 * with a Bernoulli gate_input carrying the closed-form probability,
340 * so the surrounding circuit can skip the DNF that
341 * provsql_having's enumerate_valid_worlds would otherwise build.
342 * Same probability-side sound-only caveat as runAnalyticEvaluator :
343 * the gate_input carries a fractional probability so the rewrite
344 * lives here, not in getGenericCircuit. Hidden behind
345 * provsql.cmp_probability_evaluation for developer A/B testing ;
346 * on by default. */
347 unsigned count_cmp_resolved = 0;
349 count_cmp_resolved = provsql::runCountCmpEvaluator(gc);
350 }
351
352 /* If either probability-side pre-pass replaced any cmp with a
353 * closed-form Bernoulli, the formula the downstream tool sees is
354 * not the formula the user wrote: it has had part (or all) of its
355 * comparison structure folded into Bernoulli leaves before any
356 * d-DNNF compiler / weighted model counter is invoked. Emit a
357 * NOTICE (gated on provsql.verbose_level >= 5) so the user knows
358 * the requested method's reported timing and structure may not
359 * reflect work on the original formula. */
360 if (analytic_resolved + count_cmp_resolved > 0 && provsql_verbose >= 5) {
361 size_t gates_after = count_reachable(gc_root);
362 std::string breakdown;
363 if (analytic_resolved > 0 && count_cmp_resolved > 0) {
364 breakdown = std::to_string(analytic_resolved) + " analytic + "
365 + std::to_string(count_cmp_resolved) + " Poisson-binomial";
366 } else if (analytic_resolved > 0) {
367 breakdown = std::to_string(analytic_resolved) + " analytic";
368 } else {
369 breakdown = std::to_string(count_cmp_resolved) + " Poisson-binomial";
370 }
372 "gate_cmp expression was shortcut by probability-side pre-pass "
373 "(%s): provenance circuit reduced from %zu to %zu gates",
374 breakdown.c_str(), gates_before, gates_after);
375 }
376
377 /* After every resolution pass has run, any gate_rv left in the
378 * circuit reaches the BoolExpr translation in getBooleanCircuit
379 * unchanged; that walk recurses into the surrounding gate_cmp and
380 * calls semiring.value() on the gate_value side, producing the
381 * generic "This semiring does not support value gates." error.
382 * Detect that here and raise a message that names the actual
383 * root cause: the analytical evaluators couldn't fold the RV
384 * leaves away, and the MC fallback that would have decided the
385 * surrounding cmp is either disabled (rv_mc_samples = 0) or
386 * wasn't able to close the gap. HAVING-style cmps over gate_agg
387 * don't contain gate_rv, so this check leaves them for
388 * provsql_having. */
389 if (method != "monte-carlo" && provsql::circuitHasRV(gc, gc_root)) {
390 if (provsql_rv_mc_samples <= 0) {
392 "probability_evaluate: a comparison over random variables "
393 "could not be resolved analytically; raise "
394 "provsql.rv_mc_samples above 0 to enable the Monte Carlo "
395 "fallback, or call probability_evaluate(..., 'monte-carlo', "
396 "<n>) directly");
397 } else {
399 "probability_evaluate: a comparison over random variables "
400 "could not be resolved analytically and the hybrid evaluator "
401 "left it unresolved; call probability_evaluate(..., "
402 "'monte-carlo', <n>) directly for an MC estimate");
403 }
404 }
405
406 double result;
407
408 provsql_interrupted = false;
409
410 void (*prev_sigint_handler)(int);
411 prev_sigint_handler = signal(SIGINT, provsql_sigint_handler);
412
413 try {
414 // RV-aware Monte Carlo: when the circuit contains continuous
415 // random-variable leaves, the BoolExpr translation in
416 // getBooleanCircuit drops them, so we sample directly on the
417 // GenericCircuit instead. Other probability methods are not
418 // (yet) defined over RV circuits.
419 if(method == "monte-carlo" && provsql::circuitHasRV(gc, gc_root)) {
420 int samples = 0;
421 try {
422 samples = stoi(args);
423 } catch(const std::invalid_argument &) {
424 }
425 if(samples <= 0)
426 provsql_error("Invalid number of samples: '%s'", args.c_str());
427
428 result = provsql::monteCarloRV(gc, gc_root, samples);
429 } else {
430 // Existing Boolean-circuit path: applies HAVING semantics and
431 // BoolExpr translation, then dispatches across the legacy
432 // probability methods.
433 gate_t gate;
434 std::unordered_map<gate_t, gate_t> gc_to_bc;
435 BooleanCircuit c = getBooleanCircuit(gc, token, gate, gc_to_bc);
436
437 bool processed = false;
438
439 if(method=="independent") {
440 result = c.independentEvaluation(gate);
441 processed = true;
442 } else if(method=="inversion-free") {
443 // Explicit inversion-free method: requires the certificate, errors
444 // otherwise (and ignores the provsql.inversion_free kill-switch). The
445 // structured builder throws on multivalued inputs (BID) and on a
446 // variable left unordered by collect_inversion_free_keys.
447 if(!inv_free_cert)
448 provsql_error("method 'inversion-free' requires an inversion-free "
449 "certificate on the provenance root");
450 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
451 if(!collect_inversion_free_keys(gc, gc_root, gc_to_bc, c, gate, keys))
452 provsql_error("method 'inversion-free': the provenance root carries "
453 "a certificate but its inputs lack per-input order "
454 "markers");
455 result = StructuredDNNFBuilder(c, gate, inversion_free_rank(keys))
456 .probability();
457 processed = true;
458 } else if(method=="") {
459 // Default evaluation: independent, then (when an inversion-free
460 // certificate is present) the structured-d-DNNF builder, then
461 // tree-decomposition / compilation, in order until one works.
462 try {
463 result = c.independentEvaluation(gate);
464 processed = true;
465 } catch(CircuitException &) {}
466
467 if(!processed && inv_free_cert && provsql_inversion_free) {
468 try {
469 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
470 if(collect_inversion_free_keys(gc, gc_root, gc_to_bc, c, gate, keys)) {
471 result = StructuredDNNFBuilder(c, gate, inversion_free_rank(keys))
472 .probability();
473 processed = true;
474 }
475 } catch(CircuitException &) {} // fall through to tree-decomposition
476 }
477 }
478
479 if(!processed) {
480 // Other methods do not deal with multivalued input gates, they
481 // need to be rewritten
483
484 if(method=="monte-carlo") {
485 int samples=0;
486
487 try {
488 samples = stoi(args);
489 } catch(const std::invalid_argument &e) {
490 }
491
492 if(samples<=0)
493 provsql_error("Invalid number of samples: '%s'", args.c_str());
494
495 result = c.monteCarlo(gate, samples);
496 } else if(method=="possible-worlds") {
497 if(!args.empty())
498 provsql_warning("Argument '%s' ignored for method possible-worlds", args.c_str());
499
500 result = c.possibleWorlds(gate);
501 } else if(method=="weightmc") {
502 // Backward-compatible alias for the wmc/weightmc path.
503 result = c.wmcCount(gate, "weightmc", args);
504 } else if(method=="wmc") {
505 // 'args' = "tool[;tool_args]". 'tool' selects which weighted model
506 // counter to invoke (any registered wmc tool); 'tool_args'
507 // (optional, ';'-prefixed) is forwarded. wmcCount validates the
508 // tool against the registry, so there is no per-tool branch here.
509 auto sep = args.find(';');
510 std::string tool = (sep == std::string::npos) ? args : args.substr(0, sep);
511 std::string tool_args = (sep == std::string::npos) ? std::string() : args.substr(sep + 1);
512 result = c.wmcCount(gate, tool, tool_args);
513 } else if(method=="compilation" || method=="tree-decomposition"
514 || method=="interpret-as-dd" || method=="default"
515 || method=="") {
516 auto dd = c.makeDD(gate,
517 method=="default" ? std::string() : method,
518 args);
519 result = dd.probabilityEvaluation();
520 } else {
521 provsql_error("Wrong method '%s' for probability evaluation", method.c_str());
522 }
523 }
524 }
525 } catch(CircuitException &e) {
526 // If the exception was raised because a query cancel or statement
527 // timeout is pending (the in-process loops throw "Interrupted" off the
528 // provsql_interrupted flag rather than longjmp through their C++ stack),
529 // let PG report its native 57014 with the specific reason instead of the
530 // generic "Interrupted". For any other CircuitException no cancel is
531 // pending, so CHECK_FOR_INTERRUPTS is a no-op and we report it as-is.
532 CHECK_FOR_INTERRUPTS();
533 provsql_error("%s", e.what());
534 }
535
536 provsql_interrupted = false;
537 signal (SIGINT, prev_sigint_handler);
538
539 // Avoid rounding errors that make probability outside of [0,1]
540 if(result>1.)
541 result=1.;
542 else if(result<0.)
543 result=0.;
544
545 PG_RETURN_FLOAT8(result);
546}
547
548/** @brief PostgreSQL-callable wrapper for probability_evaluate(). */
549Datum probability_evaluate(PG_FUNCTION_ARGS)
550{
551 provsql_sync_tool_registry(); // honour persisted tool-registry overrides
552 try {
553 Datum token = PG_GETARG_DATUM(0);
554 string method;
555 string args;
556
557 if(PG_ARGISNULL(0))
558 PG_RETURN_NULL();
559
560 if(!PG_ARGISNULL(1)) {
561 text *t = PG_GETARG_TEXT_P(1);
562 method = string(VARDATA(t),VARSIZE(t)-VARHDRSZ);
563 }
564
565 if(!PG_ARGISNULL(2)) {
566 text *t = PG_GETARG_TEXT_P(2);
567 args = string(VARDATA(t),VARSIZE(t)-VARHDRSZ);
568 }
569
570 return probability_evaluate_internal(*DatumGetUUIDP(token), method, args);
571 } catch(const std::exception &e) {
572 provsql_error("probability_evaluate: %s", e.what());
573 } catch(...) {
574 provsql_error("probability_evaluate: Unknown exception");
575 }
576
577 PG_RETURN_NULL();
578}
Closed-form CDF resolution for trivial gate_cmp shapes.
Boolean-expression (lineage formula) semiring.
Boolean provenance circuit with support for knowledge compilation.
@ IN
Input (variable) gate representing a base tuple.
BooleanCircuit getBooleanCircuit(GenericCircuit &gc, pg_uuid_t token, gate_t &gate, std::unordered_map< gate_t, gate_t > &gc_to_bc)
Build a BooleanCircuit from an already-loaded GenericCircuit.
GenericCircuit getGenericCircuit(pg_uuid_t token)
Build a GenericCircuit from the mmap store rooted at token.
Build in-memory circuits from the mmap-backed persistent store.
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:49
Closed-form Poisson-binomial CDF resolution for HAVING COUNT(*) op C gate_cmps.
Semiring-agnostic in-memory provenance circuit.
Peephole simplifier for continuous gate_arith sub-circuits.
Monte Carlo sampling over a GenericCircuit, RV-aware.
Support-based bound check for continuous-RV comparators.
In-process structured-d-DNNF construction over a query-derived variable order, for the inversion-free...
Fix gettext macro conflicts between PostgreSQL and the C++ STL.
Boolean circuit for provenance formula evaluation.
double possibleWorlds(gate_t g) const
Compute the probability by exact enumeration of all possible worlds.
dDNNF makeDD(gate_t g, const std::string &method, const std::string &args) const
Dispatch to the appropriate d-DNNF construction method.
double wmcCount(gate_t g, const std::string &tool, const std::string &opt) const
Weighted model counting through a registered external counter.
double monteCarlo(gate_t g, unsigned samples) const
Estimate the probability via Monte Carlo sampling.
void rewriteMultivaluedGates()
Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.
double independentEvaluation(gate_t g) const
Compute the probability exactly when inputs are independent.
Exception type thrown by circuit operations on invalid input.
Definition Circuit.h:206
virtual char const * what() const noexcept
Return the error message as a C-string.
Definition Circuit.h:220
std::vector< gate_t > & getWires(gate_t g)
Return a mutable reference to the child-wire list of gate g.
Definition Circuit.h:140
gateType getGateType(gate_t g) const
Return the type of gate g.
Definition Circuit.h:130
gate_t getGate(const uuid &u)
Return (or create) the gate associated with UUID u.
Definition Circuit.hpp:33
In-memory provenance circuit with semiring-generic evaluation.
std::string getExtra(gate_t g) const
Return the string extra for gate g.
Top-down structured-d-DNNF builder over a query-derived variable order.
double probability() const
Probability that the function is true (independent inputs).
const dDNNF & dnnf() const
The constructed d-DNNF (root set, simplified).
A d-DNNF circuit supporting exact probabilistic and game-theoretic evaluation.
Definition dDNNF.h:71
double probabilityEvaluation() const
Compute the exact probability of the d-DNNF being true.
Definition dDNNF.cpp:141
Constructs a d-DNNF from a Boolean circuit and its tree decomposition.
Provenance evaluation helper for HAVING-clause circuits.
unsigned runCountCmpEvaluator(GenericCircuit &gc)
Run the Poisson-binomial pre-pass over gc.
unsigned runRangeCheck(GenericCircuit &gc)
Run the support-based pruning pass over gc.
unsigned runHybridSimplifier(GenericCircuit &gc)
Run the peephole simplifier over gc.
double monteCarloRV(const GenericCircuit &gc, gate_t root, unsigned samples)
Run Monte Carlo on a circuit that may contain gate_rv leaves.
bool circuitHasRV(const GenericCircuit &gc, gate_t root)
Walk the circuit reachable from root looking for any gate_rv.
unsigned runHybridDecomposer(GenericCircuit &gc, unsigned samples)
Marginalise unresolved continuous-island gate_cmp gates into Bernoulli gate_input leaves.
unsigned runAnalyticEvaluator(GenericCircuit &gc)
Run the closed-form CDF resolution pass over gc.
Datum probability_evaluate(PG_FUNCTION_ARGS)
PostgreSQL-callable wrapper for probability_evaluate().
static std::map< gate_t, int > inversion_free_rank(const std::map< gate_t, StructuredDNNFBuilder::InputKey > &keys)
Flatten the per-input order keys into a total rank for the structured builder's order-only constructo...
dDNNF buildInversionFreeDDNNF(pg_uuid_t token)
Compile a query certified inversion-free to its structured d-DNNF.
static bool collect_inversion_free_keys(const GenericCircuit &gc, gate_t gc_root, const std::unordered_map< gate_t, gate_t > &gc_to_bc, const BooleanCircuit &c, gate_t bc_root, std::map< gate_t, StructuredDNNFBuilder::InputKey > &out)
Collect the inversion-free per-input order keys for the structured builder.
static void provsql_sigint_handler(int)
SIGINT handler that sets the global interrupted flag.
static Datum probability_evaluate_internal(pg_uuid_t token, const string &method, const string &args)
Core implementation of probability evaluation for a circuit token.
int provsql_verbose
Verbosity level; controlled by the provsql.verbose_level GUC.
Definition provsql.c:79
bool provsql_inversion_free
Insert the inversion-free structured-d-DNNF path into the default probability chain (after independen...
Definition provsql.c:89
int provsql_rv_mc_samples
Default sample count for analytical-evaluator MC fallbacks; 0 disables fallback (callers raise instea...
Definition provsql.c:85
bool provsql_cmp_probability_evaluation
Run closed-form / analytic probability evaluators for gate_cmps inside probability_evaluate (currentl...
Definition provsql.c:88
bool provsql_interrupted
Global variable that becomes true if this particular backend received an interrupt signal.
Definition provsql.c:75
bool provsql_hybrid_evaluation
Run the hybrid-evaluator simplifier inside probability_evaluate; controlled by the provsql....
Definition provsql.c:87
#define provsql_error(fmt,...)
Report a fatal ProvSQL error and abort the current transaction.
#define provsql_warning(fmt,...)
Emit a ProvSQL warning message (execution continues).
#define provsql_notice(fmt,...)
Emit a ProvSQL informational notice (execution continues).
Background worker and IPC primitives for mmap-backed circuit storage.
Shared-memory segment and inter-process pipe management.
Core types, constants, and utilities shared across ProvSQL.
@ gate_annotation
Transparent single-child wrapper carrying a query-level annotation in extra (inversion-free certifica...
string uuid2string(pg_uuid_t uuid)
Format a pg_uuid_t as a std::string.
C++ utility functions for UUID manipulation.
SafeCert * safe_cert_parse(const char *str)
Parse a C-prefixed recipe string (as produced by safe_cert_serialise and read back from an annotation...
bool safe_cert_key_parse(const char *str, SafeCertKey *out)
Parse a K-prefixed order-key string into out.
Tractability certificate for the inversion-free UCQ(OBDD) path.
@ CERT_INVERSION_FREE
Inversion-free UCQ(OBDD) over TID inputs.
#define SAFE_CERT_EXTRA_PREFIX_RECIPE
Discriminator prefixes for the annotation gate's extra payload.
const char * sec
const char * root
Query-derived order recipe for the structured-d-DNNF builder.
int nclasses
Number of (compacted) equivalence classes.
int root_class
Compacted id of the root class (touches every atom).
int natoms
Number of atoms (range-table entries).
SafeCertKind kind
Structured per-input order key carried by the planner's markers.
UUID structure.
void provsql_sync_tool_registry()
Rebuild the in-memory registry as "compiled seed overlaid with the provsql.tool_overrides rows"...
Reload the in-memory external-tool registry from its persistent overrides.