SQL function provsql.compile_to_ddnnf() – return the compiled d-DNNF of a provenance circuit as c2d / d4 ".nnf" text. More...

#include "postgres.h"
#include "fmgr.h"
#include "catalog/pg_type.h"
#include "utils/uuid.h"
#include "provsql_shmem.h"
#include "provsql_utils.h"
#include "c_cpp_compatibility.h"
#include "BooleanCircuit.h"
#include "CircuitFromMMap.h"
#include "dDNNF.h"
#include "provsql_utils_cpp.h"
#include "tool_registry_sync.h"
#include <string>
#include <unordered_map>

Include dependency graph for compile_to_ddnnf.cpp:

Go to the source code of this file.

Functions
Datum	compile_to_ddnnf (PG_FUNCTION_ARGS)
	PostgreSQL-callable entry point.

Detailed Description

SQL function provsql.compile_to_ddnnf() – return the compiled d-DNNF of a provenance circuit as c2d / d4 ".nnf" text.

Companion to compile_to_ddnnf_dot (which returns GraphViz DOT for a human): this returns the standard NNF interchange format, so the compiled circuit can be fed to an external d-DNNF reasoner / verifier or saved alongside the tseytin_cnf output (the two share the same variable numbering). Dispatch is the shared makeDDByName, so it accepts the same compiler / meta-route names as the DOT version.

Definition in file compile_to_ddnnf.cpp.

Function Documentation

◆ compile_to_ddnnf()

Datum compile_to_ddnnf ( PG_FUNCTION_ARGS )

PostgreSQL-callable entry point.

Arguments: token (uuid), compiler (text, default "d4"). Returns: the compiled d-DNNF in NNF text format.

Definition at line 45 of file compile_to_ddnnf.cpp.

Here is the call graph for this function:

Functions

Detailed Description

Function Documentation

◆ compile_to_ddnnf()