28#include "catalog/pg_type.h"
30#include "storage/latch.h"
31#include "utils/uuid.h"
32#include "executor/spi.h"
89 if (!proc_exit_inprogress) {
90 InterruptPending =
true;
91 QueryCancelPending =
true;
111 const std::unordered_map<gate_t, gate_t> &gc_to_bc,
113 std::map<gate_t, StructuredDNNFBuilder::InputKey> &out)
115 std::set<gate_t> seen;
116 std::stack<gate_t> st;
118 while (!st.empty()) {
119 gate_t g = st.top(); st.pop();
120 if (!seen.insert(g).second)
continue;
127 auto it = gc_to_bc.find(w[0]);
128 if (it != gc_to_bc.end())
139 std::set<gate_t> bseen;
140 std::stack<gate_t> bst;
142 while (!bst.empty()) {
143 gate_t g = bst.top(); bst.pop();
144 if (!bseen.insert(g).second)
continue;
146 if (out.find(g) == out.end())
170 const std::map<gate_t, StructuredDNNFBuilder::InputKey> &keys)
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;
184 std::map<gate_t, int> rank;
186 for (
const auto &p : v) rank[p.first] = r++;
200 std::string ex = gc.
getExtra(gc_root);
203 "carries no inversion-free certificate");
205 std::unordered_map<gate_t, gate_t> gc_to_bc;
207 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
209 throw CircuitException(
"compile 'inversion-free': the certificate's inputs "
210 "lack per-input order markers");
222 (
pg_uuid_t token,
const string &method,
const string &args)
242 bool inv_free_cert =
false;
244 std::string ex = gc.
getExtra(gc_root);
248 inv_free_cert =
true;
254 provsql_notice(
"inversion-free certificate read back from circuit "
255 "root: %d atoms, %d classes, root_class=%d",
321 auto count_reachable = [&](
gate_t r) {
322 std::set<gate_t> seen;
323 std::stack<gate_t> stk;
325 while (!stk.empty()) {
326 gate_t g = stk.top(); stk.pop();
327 if (!seen.insert(g).second)
continue;
332 size_t gates_before = count_reachable(gc_root);
347 unsigned count_cmp_resolved = 0;
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";
369 breakdown = std::to_string(count_cmp_resolved) +
" Poisson-binomial";
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);
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', "
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");
410 void (*prev_sigint_handler)(int);
422 samples = stoi(args);
423 }
catch(
const std::invalid_argument &) {
426 provsql_error(
"Invalid number of samples: '%s'", args.c_str());
434 std::unordered_map<gate_t, gate_t> gc_to_bc;
437 bool processed =
false;
439 if(method==
"independent") {
442 }
else if(method==
"inversion-free") {
448 provsql_error(
"method 'inversion-free' requires an inversion-free "
449 "certificate on the provenance root");
450 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
452 provsql_error(
"method 'inversion-free': the provenance root carries "
453 "a certificate but its inputs lack per-input order "
458 }
else if(method==
"") {
469 std::map<gate_t, StructuredDNNFBuilder::InputKey> keys;
484 if(method==
"monte-carlo") {
488 samples = stoi(args);
489 }
catch(
const std::invalid_argument &e) {
493 provsql_error(
"Invalid number of samples: '%s'", args.c_str());
496 }
else if(method==
"possible-worlds") {
498 provsql_warning(
"Argument '%s' ignored for method possible-worlds", args.c_str());
501 }
else if(method==
"weightmc") {
503 result = c.
wmcCount(gate,
"weightmc", args);
504 }
else if(method==
"wmc") {
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"
517 method==
"default" ? std::string() : method,
521 provsql_error(
"Wrong method '%s' for probability evaluation", method.c_str());
532 CHECK_FOR_INTERRUPTS();
537 signal (SIGINT, prev_sigint_handler);
545 PG_RETURN_FLOAT8(result);
553 Datum token = PG_GETARG_DATUM(0);
560 if(!PG_ARGISNULL(1)) {
561 text *t = PG_GETARG_TEXT_P(1);
562 method = string(VARDATA(t),VARSIZE(t)-VARHDRSZ);
565 if(!PG_ARGISNULL(2)) {
566 text *t = PG_GETARG_TEXT_P(2);
567 args = string(VARDATA(t),VARSIZE(t)-VARHDRSZ);
571 }
catch(
const std::exception &e) {
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.
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.
virtual char const * what() const noexcept
Return the error message as a C-string.
std::vector< gate_t > & getWires(gate_t g)
Return a mutable reference to the child-wire list of gate g.
gateType getGateType(gate_t g) const
Return the type of gate g.
gate_t getGate(const uuid &u)
Return (or create) the gate associated with UUID u.
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.
double probabilityEvaluation() const
Compute the exact probability of the d-DNNF being true.
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.
bool provsql_inversion_free
Insert the inversion-free structured-d-DNNF path into the default probability chain (after independen...
int provsql_rv_mc_samples
Default sample count for analytical-evaluator MC fallbacks; 0 disables fallback (callers raise instea...
bool provsql_cmp_probability_evaluation
Run closed-form / analytic probability evaluators for gate_cmps inside probability_evaluate (currentl...
bool provsql_interrupted
Global variable that becomes true if this particular backend received an interrupt signal.
bool provsql_hybrid_evaluation
Run the hybrid-evaluator simplifier inside probability_evaluate; controlled by the provsql....
#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.
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).