Provenance-as-Boolean-circuit semiring. More...

#include "BoolExpr.h"

Inheritance diagram for semiring::BoolExpr:

Collaboration diagram for semiring::BoolExpr:

[legend]

Public Member Functions
	BoolExpr (BooleanCircuit &bc)
	Construct a BoolExpr semiring over the given circuit.
value_type	zero () const override
	Return the additive identity \(\mathbb{0}\).
value_type	one () const override
	Return the multiplicative identity \(\mathbb{1}\).
value_type	plus (const std::vector< value_type > &vec) const override
	Apply the additive operation to a list of values.
value_type	times (const std::vector< value_type > &vec) const override
	Apply the multiplicative operation to a list of values.
virtual value_type	monus (value_type x, value_type y) const override
	Apply the monus (m-semiring difference) operation.
value_type	delta (value_type x) const override
	Apply the \(\delta\) operator.
virtual bool	absorptive () const override
	Return `true` if this semiring is absorptive ( \(\mathbb{1} \oplus a = \mathbb{1}\) for all \(a\)).
virtual bool	compatibleWithBooleanRewrite () const override
	`BoolExpr` is the free Boolean-circuit construction; the evaluation map to `Bool` at any valuation is an m-semiring homomorphism, so the safe-query Boolean rewrite preserves semantics.
virtual bool	certifying () const override
	`BoolExpr` persists the d-DNNF certificate on the HAVING possible-worlds enumerations it builds (deterministic ORs over decomposable world terms), so the certificate-aware evaluators (`independentEvaluation`, `interpretAsDD`) handle the resulting circuits linearly.
virtual bool	independent_literal (const value_type &g) const override
	A gate qualifies as an independent literal when it is a base Bernoulli input, or a constant (the empty AND / OR): distinct such gates have disjoint supports, so ANDs over them are decomposable.
virtual value_type	certified_world_term (const std::vector< value_type > &present, const std::vector< value_type > &missing) const override
	One complete world: AND of the `present` literals and of NOT-gates over the `missing` ones, marked decomposable (pairwise-distinct independent literals have disjoint supports).
virtual value_type	certified_exclusive_plus (const std::vector< value_type > &vec) const override
	Deterministic OR over pairwise-exclusive world terms, marked with the d-DNNF certificate.
Public Member Functions inherited from semiring::Semiring< gate_t >
virtual value_type	cmp (value_type s1, ComparisonOperator op, value_type s2) const
	Evaluate a comparison gate.
virtual value_type	semimod (value_type x, value_type s) const
	Apply a semimodule scalar multiplication.
virtual value_type	agg (AggregationOperator op, const std::vector< value_type > &s)
	Evaluate an aggregation gate.
virtual value_type	value (const std::string &s) const
	Interpret a literal string as a semiring value.
virtual	~Semiring ()=default

Private Types
using	value_t = gate_t
	Carrier type: a gate ID in the target BooleanCircuit.

Private Attributes
BooleanCircuit &	c
	The Boolean circuit being constructed.
const gate_t	ZERO
	Pre-allocated zero gate (OR with no children).
const gate_t	ONE
	Pre-allocated one gate (AND with no children).
std::map< gate_t, gate_t >	not_cache
	Per-literal NOT gates of `certified_world_term` (shared across world terms).

Additional Inherited Members
Public Types inherited from semiring::Semiring< gate_t >
typedef gate_t	value_type
	The carrier type of this semiring.

Detailed Description

Provenance-as-Boolean-circuit semiring.

The carrier type is gate_t (a gate identifier in BooleanCircuit). Evaluating the provenance circuit over this semiring constructs a new Boolean circuit expressing the provenance formula.

Definition at line 48 of file BoolExpr.h.

Member Typedef Documentation

◆ value_t

using semiring::BoolExpr::value_t = gate_t

private

Carrier type: a gate ID in the target BooleanCircuit.

Definition at line 49 of file BoolExpr.h.

Constructor & Destructor Documentation

◆ BoolExpr()

semiring::BoolExpr::BoolExpr ( BooleanCircuit & bc )

inline

Construct a BoolExpr semiring over the given circuit.

Parameters

bc	The Boolean circuit in which semiring operations create new gates.

Definition at line 60 of file BoolExpr.h.

Member Function Documentation

◆ absorptive()

virtual bool semiring::BoolExpr::absorptive ( ) const

inlineoverridevirtual

Return true if this semiring is absorptive ( \(\mathbb{1} \oplus a = \mathbb{1}\) for all \(a\)).

When true, the circuit evaluator and HAVING-semantics machinery may exploit the resulting idempotency ( \(a \oplus a = a\), implied by absorptivity) to deduplicate children of plus gates and to short-circuit over the multiplicative identity.

Returns: false by default; override to return true.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 121 of file BoolExpr.h.

◆ certified_exclusive_plus()

virtual value_type semiring::BoolExpr::certified_exclusive_plus ( const std::vector< value_type > & vec ) const

inlineoverridevirtual

Deterministic OR over pairwise-exclusive world terms, marked with the d-DNNF certificate.

No child deduplication: distinct complete worlds yield structurally distinct terms.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 202 of file BoolExpr.h.

◆ certified_world_term()

virtual value_type semiring::BoolExpr::certified_world_term	(	const std::vector< value_type > &	present,
		const std::vector< value_type > &	missing ) const

inlineoverridevirtual

One complete world: AND of the present literals and of NOT-gates over the missing ones, marked decomposable (pairwise-distinct independent literals have disjoint supports).

The negations are De Morgan-expanded per literal – rather than the monus(one, plus(missing)) form the uncertified construction uses – so the whole term lies inside one certified island and the sharing of contributors across the (mutually exclusive) world terms is licensed by the certificate. NOT-gates are cached per literal: the same contributor is negated in up to half the worlds.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 176 of file BoolExpr.h.

◆ certifying()

virtual bool semiring::BoolExpr::certifying ( ) const

inlineoverridevirtual

BoolExpr persists the d-DNNF certificate on the HAVING possible-worlds enumerations it builds (deterministic ORs over decomposable world terms), so the certificate-aware evaluators (independentEvaluation, interpretAsDD) handle the resulting circuits linearly.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 144 of file BoolExpr.h.

◆ compatibleWithBooleanRewrite()

virtual bool semiring::BoolExpr::compatibleWithBooleanRewrite ( ) const

inlineoverridevirtual

BoolExpr is the free Boolean-circuit construction; the evaluation map to Bool at any valuation is an m-semiring homomorphism, so the safe-query Boolean rewrite preserves semantics.

Lean: BoolFunc is the algebraic counterpart; the relevant theorems live in Provenance.Semirings.BoolFunc and Provenance.Semirings.Bool.homomorphism_to_BoolFunc.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 133 of file BoolExpr.h.

◆ delta()

value_type semiring::BoolExpr::delta ( value_type x ) const

inlineoverridevirtual

Apply the \(\delta\) operator.

Parameters

x	Input value.

Returns: \(\delta(x)\).

Implements semiring::Semiring< gate_t >.

Definition at line 117 of file BoolExpr.h.

◆ independent_literal()

virtual bool semiring::BoolExpr::independent_literal ( const value_type & g ) const

inlineoverridevirtual

A gate qualifies as an independent literal when it is a base Bernoulli input, or a constant (the empty AND / OR): distinct such gates have disjoint supports, so ANDs over them are decomposable.

Derived contributors (internal sub-circuits, mulinput literals whose block siblings are correlated) do not qualify.

Reimplemented from semiring::Semiring< gate_t >.

Definition at line 156 of file BoolExpr.h.

◆ monus()

virtual value_type semiring::BoolExpr::monus	(	value_type	x,
		value_type	y ) const

inlineoverridevirtual

Apply the monus (m-semiring difference) operation.

Parameters

x	Minuend.
y	Subtrahend.

Returns: \(x \ominus y\).

Implements semiring::Semiring< gate_t >.

Definition at line 103 of file BoolExpr.h.

◆ one()

value_type semiring::BoolExpr::one ( ) const

inlineoverridevirtual

Return the multiplicative identity \(\mathbb{1}\).

Returns: The one element of the semiring.

Implements semiring::Semiring< gate_t >.

Definition at line 67 of file BoolExpr.h.

◆ plus()

value_type semiring::BoolExpr::plus ( const std::vector< value_type > & v ) const

inlineoverridevirtual

Apply the additive operation to a list of values.

Parameters

v	Ordered list of operands (empty list should return `zero()`).

Returns: \(v_0 \oplus v_1 \oplus \cdots\).

Implements semiring::Semiring< gate_t >.

Definition at line 71 of file BoolExpr.h.

◆ times()

value_type semiring::BoolExpr::times ( const std::vector< value_type > & v ) const

inlineoverridevirtual

Apply the multiplicative operation to a list of values.

Parameters

v	Ordered list of operands (empty list should return `one()`).

Returns: \(v_0 \otimes v_1 \otimes \cdots\).

Implements semiring::Semiring< gate_t >.

Definition at line 87 of file BoolExpr.h.

◆ zero()

value_type semiring::BoolExpr::zero ( ) const

inlineoverridevirtual

Return the additive identity \(\mathbb{0}\).

Returns: The zero element of the semiring.

Implements semiring::Semiring< gate_t >.

Definition at line 63 of file BoolExpr.h.

Member Data Documentation

◆ c

BooleanCircuit& semiring::BoolExpr::c

private

The Boolean circuit being constructed.

Definition at line 51 of file BoolExpr.h.

◆ not_cache

std::map<gate_t, gate_t> semiring::BoolExpr::not_cache

mutableprivate

Per-literal NOT gates of certified_world_term (shared across world terms).

Definition at line 215 of file BoolExpr.h.

◆ ONE

const gate_t semiring::BoolExpr::ONE

private

Pre-allocated one gate (AND with no children).

Definition at line 53 of file BoolExpr.h.

◆ ZERO

const gate_t semiring::BoolExpr::ZERO

private

Pre-allocated zero gate (OR with no children).

Definition at line 52 of file BoolExpr.h.

The documentation for this class was generated from the following file:

/home/senellar/git/software/provsql/src/semiring/BoolExpr.h

Public Member Functions

Private Types

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ value_t

Constructor & Destructor Documentation

◆ BoolExpr()

Member Function Documentation

◆ absorptive()

◆ certified_exclusive_plus()

◆ certified_world_term()

◆ certifying()

◆ compatibleWithBooleanRewrite()

◆ delta()

◆ independent_literal()

◆ monus()

◆ one()

◆ plus()

◆ times()

◆ zero()

Member Data Documentation

◆ c

◆ not_cache

◆ ONE

◆ ZERO