Compiles a Boolean UCQ over a joint encoding into a certified d-D, along a tree decomposition of the joint graph. More...

#include "UCQJointCompiler.h"

Classes
struct	Stats
	Structural statistics of a compilation, for diagnostics and tests. More...
struct	Result
	A compiled UCQ: the d-D and its statistics. More...
struct	AnswerRoot
	Per-answer evaluation by a single top-down DP (data-graph regime). More...
struct	AnswerCircuit

Static Public Member Functions
static Result	compile (const JointEncoding &enc, const UCQ &ucq, unsigned max_treewidth=TreeDecomposition::MAX_TREEWIDTH, std::size_t max_states=DEFAULT_MAX_STATES)
	Compile a Boolean UCQ over `enc` into a certified d-D.
static AnswerCircuit	compileAnswersOneDP (const JointEncoding &enc, const UCQ &ucq, const std::vector< unsigned > &head_vars, unsigned max_treewidth=TreeDecomposition::MAX_TREEWIDTH, std::size_t max_states=DEFAULT_MAX_STATES)

Static Public Attributes
static constexpr std::size_t	DEFAULT_MAX_STATES = 1u << 16
	Default bound on the number of DP states at a single node.

Detailed Description

Compiles a Boolean UCQ over a joint encoding into a certified d-D, along a tree decomposition of the joint graph.

Definition at line 89 of file UCQJointCompiler.h.

Member Function Documentation

◆ compile()

UCQJointCompiler::Result UCQJointCompiler::compile	(	const JointEncoding &	enc,
		const UCQ &	ucq,
		unsigned	max_treewidth = TreeDecomposition::MAX_TREEWIDTH,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Compile a Boolean UCQ over enc into a certified d-D.

Parameters

enc	The joint encoding (facts, events, joint graph).
ucq	The Boolean UCQ.
max_treewidth	Reject (fall through to the ladder) when the joint width exceeds this.
max_states	Bound on the DP state count per node.

Returns: The compiled d-D and statistics.

Exceptions

TreeDecompositionException	if the joint width exceeds `max_treewidth` (the degeneracy screen or the min-fill build).
JointCompilerException	on unsupported input shapes or when `max_states` is exceeded.

Definition at line 2142 of file UCQJointCompiler.cpp.

Here is the call graph for this function:

◆ compileAnswersOneDP()

UCQJointCompiler::AnswerCircuit UCQJointCompiler::compileAnswersOneDP	(	const JointEncoding &	enc,
		const UCQ &	ucq,
		const std::vector< unsigned > &	head_vars,
		unsigned	max_treewidth = TreeDecomposition::MAX_TREEWIDTH,
		std::size_t	max_states = DEFAULT_MAX_STATES )

static

Definition at line 2152 of file UCQJointCompiler.cpp.

Member Data Documentation

◆ DEFAULT_MAX_STATES

std::size_t UCQJointCompiler::DEFAULT_MAX_STATES = 1u << 16

staticconstexpr

Default bound on the number of DP states at a single node.

The cap (not the static enumerating-variable count) is the true safety net: the realised-state count is governed by data sparsity and the absorbing sat collapse, typically far below the a-priori bound.

Definition at line 116 of file UCQJointCompiler.h.

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

/home/senellar/git/software/provsql/src/UCQJointCompiler.h
/home/senellar/git/software/provsql/src/UCQJointCompiler.cpp

Classes