SQL function provsql.tseytin_cnf() – return the DIMACS CNF produced by the Tseytin transformation of a provenance circuit. More...

#include "postgres.h"
#include "fmgr.h"
#include "catalog/pg_type.h"
#include "utils/jsonb.h"
#include "utils/fmgrprotos.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 "provsql_utils_cpp.h"
#include <sstream>
#include <string>

Include dependency graph for tseytin_cnf.cpp:

Go to the source code of this file.

Functions
Datum	tseytin_cnf (PG_FUNCTION_ARGS)
	PostgreSQL-callable entry point.
static void	json_escape (std::ostringstream &out, const std::string &s)
Datum	tseytin_cnf_mapping_json (PG_FUNCTION_ARGS)
	PostgreSQL-callable entry point: variable mapping as jsonb.

Detailed Description

SQL function provsql.tseytin_cnf() – return the DIMACS CNF produced by the Tseytin transformation of a provenance circuit.

This is the same encoding that BooleanCircuit::compilation() writes to a temp file before invoking d4 / c2d / minic2d / dsharp, but returned as a string so the user can inspect it or feed it to a standalone knowledge-compilation tool.

Definition in file tseytin_cnf.cpp.

Function Documentation

◆ json_escape()

void json_escape	(	std::ostringstream &	out,
		const std::string &	s )

static

Definition at line 79 of file tseytin_cnf.cpp.

Here is the caller graph for this function:

◆ tseytin_cnf()

Datum tseytin_cnf ( PG_FUNCTION_ARGS )

PostgreSQL-callable entry point.

Arguments: token (uuid), weighted (bool, default true), mapping (bool, default true). Returns: DIMACS CNF as text; when weighted, includes w lines; when mapping, prepends "c input <var> <uuid> <prob>" comments.

Definition at line 46 of file tseytin_cnf.cpp.

Here is the call graph for this function:

◆ tseytin_cnf_mapping_json()

Datum tseytin_cnf_mapping_json ( PG_FUNCTION_ARGS )

PostgreSQL-callable entry point: variable mapping as jsonb.

Argument: token (uuid). Returns a jsonb array of objects {"variable":int,"gate":uuid-string,"probability":float8}, one per input gate, with the same variable numbering as tseytin_cnf. The SQL wrapper tseytin_cnf_mapping unnests this into a table.

Definition at line 98 of file tseytin_cnf.cpp.