Boolean circuit for provenance formula evaluation. More...

#include "BooleanCircuit.h"

Inheritance diagram for BooleanCircuit:

[legend]

Collaboration diagram for BooleanCircuit:

Classes
struct	CNFInputMapping
	One row of the Tseytin variable mapping. More...

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.
bool	hasMultivaluedGates () const
	Return `true` if the circuit contains any MULIN gates.
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.
dDNNF	parseDDNNF (std::istream &in, const std::vector< gate_t > &inputOrder) const
	Parse a c2d/d4 NNF stream into a `dDNNF` over this circuit's input gates.
double	monteCarlo (gate_t g, unsigned samples) const
	Estimate the probability via Monte Carlo sampling.
double	wmcCount (gate_t g, const std::string &tool, const std::string &opt) const
	Weighted model counting through a registered external 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.
dDNNF	makeDDByName (gate_t g, const std::string &name) const
	Build a `dDNNF` from a single compiler/route name.
virtual std::string	toString (gate_t g) const override
	Return a textual description of gate `g` for debugging.
std::string	toString (gate_t g, const std::unordered_map< gate_t, std::string > &labels) const
	Render the sub-circuit at `g`, labelling input gates from a map.
std::string	exportCircuit (gate_t g) const
	Export the circuit in the textual format expected by external compilers.
std::string	TseytinCNF (gate_t g, bool display_prob, bool mapping=false) const
	Return the Tseytin transformation of the sub-circuit at `g` as a DIMACS string.
std::vector< CNFInputMapping >	tseytinVariableMapping () const
	Map each input gate to its DIMACS variable, UUID, probability.
std::string	BCS12 (gate_t g, std::vector< gate_t > &inputOrder) const
	Serialise the sub-circuit at `g` in d4's BC-S1.2 circuit format.
dDNNF	parsePaniniDD (const std::string &outfilename) const
	Parse a Panini (KCBox) DD output file into a ProvSQL d-DNNF.
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`.
virtual gate_t	setGate (const uuid &u, BooleanGate type)
	Create or update the gate associated with UUID `u`.
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.
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()`.
std::string	toStringHelper (gate_t g, BooleanGate parent, const std::unordered_map< gate_t, std::string > *labels) const
	Internal recursive helper for the two `toString()` variants.

Friends
class	dDNNFTreeDecompositionBuilder
class	boost::serialization::access

Additional Inherited Members
Public Types inherited from Circuit< BooleanGate >
using	uuid
	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 74 of file BooleanCircuit.h.

Constructor & Destructor Documentation

◆ BooleanCircuit()

BooleanCircuit::BooleanCircuit ( )

inline

Construct an empty Boolean circuit.

Definition at line 127 of file BooleanCircuit.h.

◆ ~BooleanCircuit()

virtual BooleanCircuit::~BooleanCircuit ( )

inlinevirtual

Definition at line 129 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 172 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ BCS12()

std::string BooleanCircuit::BCS12	(	gate_t	g,
		std::vector< gate_t > &	inputOrder ) const

Serialise the sub-circuit at g in d4's BC-S1.2 circuit format.

Emits the Boolean circuit directly (inputs as "I" declarations, AND/OR gates as "G name := A|O …" definitions, the root as "T"), inlining NOT gates as literal sign flips. This is the input consumed by d4v2's --input-type circuit mode, letting us skip the Tseytin transform.

Inputs are emitted first, so d4 (which numbers literals from 1 in first-seen order) assigns them variables 1..k in declaration order; every variable above k is an internal-gate variable. inputOrder is filled so that d4 variable v (1-based) corresponds to input gate inputOrder[v-1], which the d-DNNF parse-back uses to map decision literals to the right IN gate.

Throws CircuitException on a gate shape BC-S1.2 cannot express (a nullary AND/OR, or a non-AND/OR/NOT/IN gate); the caller falls back to the Tseytin CNF path.

Parameters

g	Root gate of the sub-circuit.
inputOrder	Output: input gate for each d4 variable (1-based).

Returns: BC-S1.2 circuit description as a string.

Definition at line 516 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller 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 783 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 319 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 260 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 1343 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 160 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 194 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ hasMultivaluedGates()

bool BooleanCircuit::hasMultivaluedGates ( ) const

inline

Return true if the circuit contains any MULIN gates.

Multivalued inputs are normally rewritten into AND/OR/NOT/IN gates by rewriteMultivaluedGates() before the circuit is consumed by an evaluation method. Algorithms that cannot handle multivalued inputs directly can use this as a precondition check.

Returns: true iff at least one MULIN gate is present.

Definition at line 174 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 1332 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 1241 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 1486 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 1431 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 202 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 1505 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ makeDDByName()

dDNNF BooleanCircuit::makeDDByName	(	gate_t	g,
		const std::string &	name ) const

Build a dDNNF from a single compiler/route name.

Resolves the name the way a user (or Studio) thinks of it, with no separate method / args split:

the in-process meta-routes "tree-decomposition", "interpret-as-dd", "default" (and the empty string) go through makeDD;
any other name is an external compiler ("d4", "d4v2", "c2d", "minic2d", "dsharp", "panini-*") and is passed straight to compilation.

This is the single dispatch point shared by compile_to_ddnnf_dot, compile_to_ddnnf (NNF) and ddnnf_stats, so they cannot drift on which names they accept.

Parameters

g	Root gate.
name	Compiler or meta-route name.

Returns: The constructed dDNNF.

Definition at line 1548 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 355 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ parseDDNNF()

dDNNF BooleanCircuit::parseDDNNF	(	std::istream &	in,
		const std::vector< gate_t > &	inputOrder ) const

Parse a c2d/d4 NNF stream into a dDNNF over this circuit's input gates.

Shared by the CLI compilation() path and the KCMCP client: both obtain the same NNF text (from a temp file or a socket RESULT) and parse it identically. inputOrder maps d4 circuit-mode variables (1..k) to IN gates; an empty vector means CNF mode, where d-DNNF variable v stands for gate id v-1 (real only for IN gates, every other being a Tseytin auxiliary that is projected out).

Parameters

in	NNF text stream.
inputOrder	Circuit-mode input-variable to IN-gate map (empty = CNF).

Returns: The compiled dDNNF (empty if the formula is unsat).

Definition at line 944 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ parsePaniniDD()

dDNNF BooleanCircuit::parsePaniniDD ( const std::string & outfilename ) const

Parse a Panini (KCBox) DD output file into a ProvSQL d-DNNF.

The panini-dd output parser, selected by compilation() for the panini-* records. Those records run the generic compile path (a Tseytin CNF written to the input, the record's argtpl run, the --lang carried in the template); they differ from the nnf compilers only in this parse-back. Panini's DD output is over the variables of our Tseytin CNF: decisions on input variables are translated to the corresponding IN gates; decisions on Tseytin auxiliaries are dropped (their branches are mutually exclusive over input assignments by Tseytin determinism, so the input-projection is still a sound d-DNNF). "R2-D2" / "CCDD" emit K (kernelize) nodes that break decomposability, so those variants are not registered and a K node here is an error.

Parameters

outfilename Path to Panini's DD output file.

Returns: The compiled d-DNNF.

Definition at line 608 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 390 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 1401 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 1353 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 506 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 163 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 130 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 154 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 142 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 1338 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 183 of file BooleanCircuit.h.

Here is the caller graph for this function:

◆ toString() [1/2]

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 179 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ toString() [2/2]

std::string BooleanCircuit::toString	(	gate_t	g,
		const std::unordered_map< gate_t, std::string > &	labels ) const

Render the sub-circuit at g, labelling input gates from a map.

Same as toString(gate_t), but IN and MULIN gates whose gate identifier is present in labels are rendered using the mapped string instead of the default x<id> placeholder. Gates not found in labels fall back to the default rendering.

Parameters

g	Gate to render.
labels	Optional mapping from input/mulinput gate IDs to user-supplied labels.

Returns: Human-readable string.

Definition at line 184 of file BooleanCircuit.cpp.

Here is the call graph for this function:

◆ toStringHelper()

std::string BooleanCircuit::toStringHelper	(	gate_t	g,
		BooleanGate	parent,
		const std::unordered_map< gate_t, std::string > *	labels ) const

private

Internal recursive helper for the two toString() variants.

The parent parameter carries the gate type of the immediate caller. It drives parenthesis elision in two cases: at the root (parent set to UNDETERMINED) the outer wrap is omitted, and when parent matches the current gate type (associative AND/OR) the wrap is omitted to flatten same-op nesting. A 1-wire AND/OR also bypasses the wrap and delegates to its child since such single-element joins carry no information.

Parameters

g	Gate to render.
parent	Gate type of the caller, or `UNDETERMINED` at the root.
labels	Pointer to a label map, or `nullptr` for the unlabelled rendering.

Definition at line 191 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ TseytinCNF()

std::string BooleanCircuit::TseytinCNF	(	gate_t	g,
		bool	display_prob,
		bool	mapping = false ) const

Return the Tseytin transformation of the sub-circuit at g as a DIMACS string.

Same encoding as the private Tseytin file-emitting overload, but returned in memory without any file I/O. Useful for surfacing the CNF to a user or to a knowledge-compilation tool over stdin.

Parameters

g	Root gate.
display_prob	Include `w` lines listing each input's probability (and its complement).
mapping	Prepend `"c input <var> <uuid> <prob>"` comment lines, one per input gate, so the emitted DIMACS is self-documenting (the comments are ignored by every model counter / compiler).

Returns: DIMACS CNF as a string.

Definition at line 423 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ tseytinVariableMapping()

std::vector< BooleanCircuit::CNFInputMapping > BooleanCircuit::tseytinVariableMapping ( ) const

Map each input gate to its DIMACS variable, UUID, probability.

The variable numbering matches TseytinCNF (and dDNNF::toNNF): variable = gate id + 1. Inputs are listed in gate-id order so the mapping is deterministic.

Returns: One CNFInputMapping per input gate.

Definition at line 501 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ wmcCount()

double BooleanCircuit::wmcCount	(	gate_t	g,
		const std::string &	tool,
		const std::string &	opt ) const

Weighted model counting through a registered external counter.

Generic over the counter: tool names a registry record with the "wmc" operation (today weightmc, ganak, sharpsat-td, dpmc, or any tool an administrator registers). The record's binary, dependencies, argtpl and parser drive the whole call – which weighted-CNF dialect to write, the command to run, and how to read the count back – so there is no per-counter code path. Two output/input conventions are understood, by parser: "wmc-line" (MCC-2024 weighted DIMACS in, a "c s exact" / "s wmc" count line out) and "weightmc" (weightmc's own dialect in, a "mantissa x 2^exp" line out).

Parameters

g	Root gate of the sub-circuit.
tool	Logical name of the wmc tool to use.
opt	Tool options; for the approximate counters of the form `"delta;epsilon"` (drives the `{pivotAC}` placeholder).

Returns: The weighted model count = P(formula).

Definition at line 1124 of file BooleanCircuit.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ boost::serialization::access

friend class boost::serialization::access

friend

Definition at line 520 of file BooleanCircuit.h.

◆ dDNNFTreeDecompositionBuilder

friend class dDNNFTreeDecompositionBuilder

friend

Definition at line 519 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 122 of file BooleanCircuit.h.

◆ inputs

std::set<gate_t> BooleanCircuit::inputs

protected

Set of IN (input) gate IDs.

Definition at line 119 of file BooleanCircuit.h.

◆ mulinputs

std::set<gate_t> BooleanCircuit::mulinputs

protected

Set of MULVAR gate IDs.

Definition at line 120 of file BooleanCircuit.h.

◆ prob

std::vector<double> BooleanCircuit::prob

protected

Per-gate probability (for IN gates).

Definition at line 121 of file BooleanCircuit.h.

◆ probabilistic

bool BooleanCircuit::probabilistic =false

protected

true if any gate has a non-unit probability

Definition at line 123 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

Classes

Public Member Functions

Protected Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ BooleanCircuit()

◆ ~BooleanCircuit()

Member Function Documentation

◆ addGate()

◆ BCS12()

◆ compilation()

◆ evaluate()

◆ exportCircuit()

◆ getInfo()

◆ getInputs()

◆ getProb()

◆ hasMultivaluedGates()

◆ independentEvaluation()

◆ independentEvaluationInternal()

◆ interpretAsDD()

◆ interpretAsDDInternal()

◆ isProbabilistic()

◆ makeDD()

◆ makeDDByName()

◆ monteCarlo()

◆ parseDDNNF()

◆ parsePaniniDD()

◆ possibleWorlds()

◆ rewriteMultivaluedGates()

◆ rewriteMultivaluedGatesRec()

◆ serialize()

◆ setGate() [1/4]

◆ setGate() [2/4]

◆ setGate() [3/4]

◆ setGate() [4/4]

◆ setInfo()

◆ setProb()

◆ toString() [1/2]

◆ toString() [2/2]

◆ toStringHelper()

◆ TseytinCNF()

◆ tseytinVariableMapping()

◆ wmcCount()

Friends And Related Symbol Documentation

◆ boost::serialization::access

◆ dDNNFTreeDecompositionBuilder

Member Data Documentation

◆ info

◆ inputs

◆ mulinputs

◆ prob

◆ probabilistic