nonzero.cpp File Reference

SQL function provsql.true_nonzero() – structural universal-zero test backing the default mode of provsql.nonzero(). More...

#include "postgres.h"
#include "fmgr.h"
#include "utils/uuid.h"
#include "provsql_utils.h"
#include <exception>
#include <unordered_map>
#include "BooleanCircuit.h"
#include "CircuitFromMMap.h"
#include "GenericCircuit.h"
#include "provsql_utils_cpp.h"

Include dependency graph for nonzero.cpp:

Go to the source code of this file.

Functions
static bool	provably_zero (const GenericCircuit &gc, gate_t g, const BooleanCircuit *bc, const std::unordered_map< gate_t, gate_t > *gc_to_bc, std::unordered_map< gate_t, bool > &memo)
	Structural proof of universal zero-ness of g, memoized over the DAG.
Datum	true_nonzero (PG_FUNCTION_ARGS)
	PostgreSQL-callable wrapper: the default mode of provsql.nonzero().

Detailed Description

SQL function provsql.true_nonzero() – structural universal-zero test backing the default mode of provsql.nonzero().

Decides whether a circuit is provably the semiring zero – zero in every m-semiring under every leaf valuation – by the sound structural rules: gate_zero; a ⊗ with a zero factor; a ⊕ (or δ, or a transparent single-child wrapper) all of whose children are zero; a ⊖ whose left operand is zero; a semimod whose provenance side is zero. Comparison gates are resolved through the Boolean-abstraction pipeline (the same provsql_having world enumeration every evaluator applies): a cmp whose satisfying-world set is empty is the empty disjunction, i.e. zero in every semiring, and surfaces in the Boolean circuit as a childless OR (the BoolExpr semiring's zero()). Everything else – input gates, undecided probabilistic comparisons, mixtures, conditioning – blocks the proof: the verdict is then true (not provably zero), never a dropped row.

Exact zero-ness in the free m-semiring is the word problem for the m-semiring axioms, whose decidability is open; drop-only-on-proof is the specified contract, so a sound under-approximation is exactly right.

Definition in file nonzero.cpp.

Function Documentation

provably_zero()

bool provably_zero ( const GenericCircuit & gc, gate_t g, const BooleanCircuit * bc, const std::unordered_map< gate_t, gate_t > * gc_to_bc, std::unordered_map< gate_t, bool > & memo )

static

Structural proof of universal zero-ness of g, memoized over the DAG.

Parameters

gc	The loaded circuit (post the load-time simplification passes, so RangeCheck-decided RV comparisons are already constants).
g	Gate to test.
bc	Boolean abstraction of gc, when it could be built; used only to read comparison gates' world-set emptiness.
gc_to_bc	Gate map into bc.
memo	Verdict cache (the circuit is a DAG).

Definition at line 58 of file nonzero.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

true_nonzero()

Datum true_nonzero

(

PG_FUNCTION_ARGS

)

PostgreSQL-callable wrapper: the default mode of provsql.nonzero().

Definition at line 140 of file nonzero.cpp.

Here is the call graph for this function: