Boolean circuit for provenance formula evaluation. More...

#include "BooleanCircuit.h"

Inheritance diagram for BooleanCircuit:

[legend]

Collaboration diagram for BooleanCircuit:

Public Member Functions
	BooleanCircuit ()
	Construct an empty Boolean circuit.

virtual	~BooleanCircuit ()

gate_t	addGate () override
	Allocate a new gate with a default-initialised type.

gate_t	setGate (BooleanGate type) override
	Allocate a new gate with type `type` and no UUID.

gate_t	setGate (const uuid &u, BooleanGate type) override
	Create or update the gate associated with UUID `u`.

gate_t	setGate (BooleanGate t, double p)
	Create a new gate with a probability annotation.

gate_t	setGate (const uuid &u, BooleanGate t, double p)
	Create (or update) a gate with a UUID and probability.

const std::set< gate_t > &	getInputs () const
	Return the set of input (IN) gate IDs.

void	setProb (gate_t g, double p)
	Set the probability for gate `g` and mark the circuit as probabilistic.

double	getProb (gate_t g) const
	Return the probability stored for gate `g`.

bool	isProbabilistic () const
	Return `true` if any gate has a non-trivial (< 1) probability.

void	setInfo (gate_t g, unsigned info)
	Store an integer annotation on gate `g`.

unsigned	getInfo (gate_t g) const
	Return the integer annotation for gate `g`.

double	possibleWorlds (gate_t g) const
	Compute the probability by exact enumeration of all possible worlds.

dDNNF	compilation (gate_t g, std::string compiler) const
	Compile the sub-circuit rooted at `g` to a `dDNNF` via an external tool.

double	monteCarlo (gate_t g, unsigned samples) const
	Estimate the probability via Monte Carlo sampling.

double	WeightMC (gate_t g, std::string opt) const
	Compute the probability using the `weightmc` model counter.

double	independentEvaluation (gate_t g) const
	Compute the probability exactly when inputs are independent.

void	rewriteMultivaluedGates ()
	Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.

dDNNF	interpretAsDD (gate_t g) const
	Build a `dDNNF` directly from the Boolean circuit's structure.

dDNNF	makeDD (gate_t g, const std::string &method, const std::string &args) const
	Dispatch to the appropriate d-DNNF construction method.

virtual std::string	toString (gate_t g) const override
	Return a textual description of gate `g` for debugging.

std::string	exportCircuit (gate_t g) const
	Export the circuit in the textual format expected by external compilers.

template<class Archive >
void	serialize (Archive &ar, const unsigned int version)
	Boost serialisation support.

Public Member Functions inherited from Circuit< BooleanGate >
virtual	~Circuit ()

std::vector< gate_t >::size_type	getNbGates () const
	Return the total number of gates in the circuit.

gate_t	getGate (const uuid &u)
	Return (or create) the gate associated with UUID `u`.

uuid	getUUID (gate_t g) const
	Return the UUID string associated with gate `g`.

BooleanGate	getGateType (gate_t g) const
	Return the type of gate `g`.

std::vector< gate_t > &	getWires (gate_t g)
	Return a mutable reference to the child-wire list of gate `g`.

const std::vector< gate_t > &	getWires (gate_t g) const
	Return a const reference to the child-wire list of gate `g`.

virtual gate_t	setGate (const uuid &u, BooleanGate type)
	Create or update the gate associated with UUID `u`.

virtual gate_t	setGate (BooleanGate type)
	Allocate a new gate with type `type` and no UUID.

bool	hasGate (const uuid &u) const
	Test whether a gate with UUID `u` exists.

void	addWire (gate_t f, gate_t t)
	Add a directed wire from gate `f` (parent) to gate `t` (child).

Protected Attributes
std::set< gate_t >	inputs
	Set of IN (input) gate IDs.

std::set< gate_t >	mulinputs
	Set of MULVAR gate IDs.

std::vector< double >	prob
	Per-gate probability (for IN gates)

std::map< gate_t, unsigned >	info
	Per-gate integer info (for MULIN gates)

bool	probabilistic =false
	`true` if any gate has a non-unit probability

Protected Attributes inherited from Circuit< BooleanGate >
std::unordered_map< uuid, gate_t >	uuid2id
	UUID string → gate index.

std::unordered_map< gate_t, uuid >	id2uuid
	Gate index → UUID string.

std::vector< BooleanGate >	gates
	Gate type for each gate.

std::vector< std::vector< gate_t > >	wires
	Child wire lists for each gate.

Private Member Functions
bool	evaluate (gate_t g, const std::unordered_set< gate_t > &sampled) const
	Evaluate the sub-circuit at `g` on one sampled world.

std::string	Tseytin (gate_t g, bool display_prob) const
	Generate a Tseytin transformation of the sub-circuit at `g`.

gate_t	interpretAsDDInternal (gate_t g, std::set< gate_t > &seen, dDNNF &dd) const
	Recursive helper for `interpretAsDD()`.

double	independentEvaluationInternal (gate_t g, std::set< gate_t > &seen) const
	Recursive helper for `independentEvaluation()`.

void	rewriteMultivaluedGatesRec (const std::vector< gate_t > &muls, const std::vector< double > &cumulated_probs, unsigned start, unsigned end, std::vector< gate_t > &prefix)
	Recursive helper for `rewriteMultivaluedGates()`.

Friends
class	dDNNFTreeDecompositionBuilder

class	boost::serialization::access

Additional Inherited Members
Public Types inherited from Circuit< BooleanGate >
using	uuid = std::string
	UUID type used in this circuit (always `std::string`).

Protected Member Functions inherited from Circuit< BooleanGate >
void	setGateType (gate_t g, BooleanGate t)
	Update the type of an existing gate.

Detailed Description

Boolean circuit for provenance formula evaluation.

Inherits the gate/wire infrastructure from Circuit<BooleanGate> and adds probability annotation, info integers (for multivalued inputs), and a rich set of evaluation algorithms.

Definition at line 73 of file BooleanCircuit.h.

Constructor & Destructor Documentation

◆ BooleanCircuit()

BooleanCircuit::BooleanCircuit ( )

inline

Construct an empty Boolean circuit.

Definition at line 138 of file BooleanCircuit.h.

◆ ~BooleanCircuit()

virtual BooleanCircuit::~BooleanCircuit ( )

inlinevirtual

Definition at line 140 of file BooleanCircuit.h.

Member Function Documentation

◆ addGate()

gate_t BooleanCircuit::addGate ( )

overridevirtual

Allocate a new gate with a default-initialised type.

Derived classes override this to perform additional initialisation (e.g. resizing auxiliary vectors).

Returns: The gate_t identifier of the newly created gate.

Reimplemented from Circuit< BooleanGate >.

Definition at line 100 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ compilation()

dDNNF BooleanCircuit::compilation	(	gate_t	g,
		std::string	compiler
	)		const

Compile the sub-circuit rooted at g to a dDNNF via an external tool.

Writes the circuit in DIMACS/DNNF format, invokes compiler as a subprocess, and parses the resulting d-DNNF.

Parameters

g	Root gate.
compiler	Command to invoke (e.g. "d4", "c2d", "minic2d").

Returns: The compiled dDNNF.

Definition at line 379 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluate()

bool BooleanCircuit::evaluate	(	gate_t	g,
		const std::unordered_set< gate_t > &	sampled
	)		const

private

Evaluate the sub-circuit at g on one sampled world.

Each gate in sampled is treated as true; all other IN gates are false.

Parameters

g	Root gate to evaluate.
sampled	Set of input gates that are `true` in this world.

Returns: Boolean value of the circuit at gate g.

Definition at line 211 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ exportCircuit()

std::string BooleanCircuit::exportCircuit ( gate_t g ) const

Export the circuit in the textual format expected by external compilers.

Produces a multi-line string encoding all gates reachable from the circuit in the format used by the standalone tdkc tool and external model counters.

Parameters

g	Root gate.

Returns: Circuit description string.

Definition at line 152 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ getInfo()

unsigned BooleanCircuit::getInfo ( gate_t g ) const

Return the integer annotation for gate g.

Parameters

g	Gate identifier.

Returns: Stored integer, or 0 if not set.

Definition at line 708 of file BooleanCircuit.cpp.

Here is the caller graph for this function:

◆ getInputs()

const std::set< gate_t > & BooleanCircuit::getInputs ( ) const

inline

Return the set of input (IN) gate IDs.

Returns: Const reference to the set of IN gate identifiers.

Definition at line 171 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ getProb()

double BooleanCircuit::getProb ( gate_t g ) const

inline

Return the probability stored for gate g.

Parameters

g	Gate identifier.

Returns: Probability value.

Definition at line 191 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ independentEvaluation()

double BooleanCircuit::independentEvaluation ( gate_t g ) const

Compute the probability exactly when inputs are independent.

Applicable when the circuit has no shared input gate (i.e., each input appears at most once).

Parameters

g	Root gate.

Returns: Exact probability.

Definition at line 697 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ independentEvaluationInternal()

double BooleanCircuit::independentEvaluationInternal	(	gate_t	g,
		std::set< gate_t > &	seen
	)		const

private

Recursive helper for independentEvaluation().

Parameters

g	Current gate to evaluate.
seen	Set of gates already evaluated (for memoisation).

Returns: Probability at gate g.

Definition at line 622 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interpretAsDD()

dDNNF BooleanCircuit::interpretAsDD ( gate_t g ) const

Build a dDNNF directly from the Boolean circuit's structure.

Used as a fallback when no external compiler is available and the circuit is already in a form that can be interpreted as a d-DNNF.

Parameters

g	Root gate.

Returns: A dDNNF wrapping the same structure.

Definition at line 842 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interpretAsDDInternal()

gate_t BooleanCircuit::interpretAsDDInternal	(	gate_t	g,
		std::set< gate_t > &	seen,
		dDNNF &	dd
	)		const

private

Recursive helper for interpretAsDD().

Parameters

g	Current gate to process.
seen	Set of gates already visited (prevents re-processing).
dd	The d-DNNF being constructed.

Returns: Gate ID in dd corresponding to g.

Definition at line 790 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isProbabilistic()

bool BooleanCircuit::isProbabilistic ( ) const

inline

Return true if any gate has a non-trivial (< 1) probability.

Returns: true iff at least one gate has a probability strictly less than 1.

Definition at line 199 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ makeDD()

dDNNF BooleanCircuit::makeDD	(	gate_t	g,
		const std::string &	method,
		const std::string &	args
	)		const

Dispatch to the appropriate d-DNNF construction method.

Parameters

g	Root gate.
method	Compilation method name (e.g. "tree-decomposition", "d4", "c2d", …).
args	Additional arguments forwarded to the chosen method.

Returns: The constructed dDNNF.

Definition at line 852 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ monteCarlo()

double BooleanCircuit::monteCarlo	(	gate_t	g,
		unsigned	samples
	)		const

Estimate the probability via Monte Carlo sampling.

Parameters

g	Root gate.
samples	Number of independent worlds to sample.

Returns: Estimated probability.

Definition at line 247 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ possibleWorlds()

double BooleanCircuit::possibleWorlds ( gate_t g ) const

Compute the probability by exact enumeration of all possible worlds.

Only tractable for circuits with a small number of input gates.

Parameters

g	Root gate.

Returns: Exact probability.

Definition at line 269 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rewriteMultivaluedGates()

void BooleanCircuit::rewriteMultivaluedGates ( )

Rewrite all MULVAR/MULIN gate clusters into standard AND/OR/NOT circuits.

Must be called before any evaluation method when the circuit contains multivalued input gates.

Definition at line 760 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rewriteMultivaluedGatesRec()

void BooleanCircuit::rewriteMultivaluedGatesRec	(	const std::vector< gate_t > &	muls,
		const std::vector< double > &	cumulated_probs,
		unsigned	start,
		unsigned	end,
		std::vector< gate_t > &	prefix
	)

private

Recursive helper for rewriteMultivaluedGates().

Parameters

muls	Gates in the MULVAR group being rewritten.
cumulated_probs	Cumulative probability thresholds for each MULIN.
start	First index in `muls` to process.
end	One past the last index in `muls` to process.
prefix	Current AND-chain prefix being built.

Definition at line 718 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ serialize()

template<class Archive >

void BooleanCircuit::serialize	(	Archive &	ar,
		const unsigned int	version
	)

inline

Boost serialisation support.

Parameters

ar	Boost archive (input or output).
version	Archive version (unused).

Definition at line 322 of file BooleanCircuit.h.

◆ setGate() [1/4]

gate_t BooleanCircuit::setGate	(	BooleanGate	t,
		double	p
	)

Create a new gate with a probability annotation.

Parameters

t	Gate type (typically `BooleanGate::IN`).
p	Probability of this gate being `true`.

Returns: Gate identifier.

Definition at line 91 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setGate() [2/4]

gate_t BooleanCircuit::setGate ( BooleanGate type )

override

Allocate a new gate with type type and no UUID.

Parameters

type	Gate type.

Returns: Gate identifier.

Definition at line 58 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setGate() [3/4]

gate_t BooleanCircuit::setGate	(	const uuid &	u,
		BooleanGate	t,
		double	p
	)

Create (or update) a gate with a UUID and probability.

Parameters

u	UUID string.
t	Gate type.
p	Probability of this gate being `true`.

Returns: Gate identifier.

Definition at line 82 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setGate() [4/4]

gate_t BooleanCircuit::setGate	(	const uuid &	u,
		BooleanGate	type
	)

override

Create or update the gate associated with UUID u.

If the UUID is already mapped the existing gate's type is updated. Otherwise a new gate is allocated.

Parameters

u	UUID string to associate with the gate.
type	Gate type.

Returns: Gate identifier.

Definition at line 70 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ setInfo()

void BooleanCircuit::setInfo	(	gate_t	g,
		unsigned	info
	)

Store an integer annotation on gate g.

Used to record the index of a MULIN gate within its MULVAR group.

Parameters

g	Gate identifier.
info	Integer to store.

Definition at line 703 of file BooleanCircuit.cpp.

Here is the caller graph for this function:

◆ setProb()

void BooleanCircuit::setProb	(	gate_t	g,
		double	p
	)

inline

Set the probability for gate g and mark the circuit as probabilistic.

Parameters

g	Gate identifier.
p	Probability value in [0, 1].

Definition at line 180 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ toString()

std::string BooleanCircuit::toString ( gate_t g ) const

overridevirtual

Return a textual description of gate g for debugging.

Pure virtual; each concrete circuit class provides its own formatting.

Parameters

g	Gate to describe.

Returns: Human-readable string.

Implements Circuit< BooleanGate >.

Definition at line 107 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Tseytin()

std::string BooleanCircuit::Tseytin	(	gate_t	g,
		bool	display_prob = `false`
	)		const

private

Generate a Tseytin transformation of the sub-circuit at g.

Produces a CNF/DIMACS-style encoding suitable for input to model counters such as weightmc or d4.

Parameters

g	Root gate.
display_prob	Include probability weights in the output.

Returns: DIMACS string.

Definition at line 302 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ WeightMC()

double BooleanCircuit::WeightMC	(	gate_t	g,
		std::string	opt
	)		const

Compute the probability using the weightmc model counter.

Parameters

g	Root gate.
opt	Additional command-line options forwarded to `weightmc`.

Returns: Probability estimate returned by weightmc.

Definition at line 556 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Symbol Documentation

◆ boost::serialization::access

friend class boost::serialization::access

friend

Definition at line 336 of file BooleanCircuit.h.

◆ dDNNFTreeDecompositionBuilder

friend class dDNNFTreeDecompositionBuilder

friend

Definition at line 335 of file BooleanCircuit.h.

Member Data Documentation

◆ info

std::map<gate_t, unsigned> BooleanCircuit::info

protected

Per-gate integer info (for MULIN gates)

Definition at line 133 of file BooleanCircuit.h.

◆ inputs

std::set<gate_t> BooleanCircuit::inputs

protected

Set of IN (input) gate IDs.

Definition at line 130 of file BooleanCircuit.h.

◆ mulinputs

std::set<gate_t> BooleanCircuit::mulinputs

protected

Set of MULVAR gate IDs.

Definition at line 131 of file BooleanCircuit.h.

◆ prob

std::vector<double> BooleanCircuit::prob

protected

Per-gate probability (for IN gates)

Definition at line 132 of file BooleanCircuit.h.

◆ probabilistic

bool BooleanCircuit::probabilistic =false

protected

true if any gate has a non-unit probability

Definition at line 134 of file BooleanCircuit.h.

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

/home/pierre/git/software/provsql/src/BooleanCircuit.h
/home/pierre/git/software/provsql/src/BooleanCircuit.cpp

Public Member Functions

Protected Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BooleanCircuit()

◆ ~BooleanCircuit()

Member Function Documentation

◆ addGate()

◆ compilation()

◆ evaluate()

◆ exportCircuit()

◆ getInfo()

◆ getInputs()

◆ getProb()

◆ independentEvaluation()

◆ independentEvaluationInternal()

◆ interpretAsDD()

◆ interpretAsDDInternal()

◆ isProbabilistic()

◆ makeDD()

◆ monteCarlo()

◆ possibleWorlds()

◆ rewriteMultivaluedGates()

◆ rewriteMultivaluedGatesRec()

◆ serialize()

◆ setGate() [1/4]

◆ setGate() [2/4]

◆ setGate() [3/4]

◆ setGate() [4/4]

◆ setInfo()

◆ setProb()

◆ toString()

◆ Tseytin()

◆ WeightMC()

Friends And Related Symbol Documentation

◆ boost::serialization::access

◆ dDNNFTreeDecompositionBuilder

Member Data Documentation

◆ info

◆ inputs

◆ mulinputs

◆ prob

◆ probabilistic