17#include <boost/property_tree/ptree.hpp>
18#include <boost/property_tree/json_parser.hpp>
29#include <sys/socket.h>
40using steady = std::chrono::steady_clock;
48constexpr uint32_t SERVER_MAX_PAYLOAD = 256u * 1024 * 1024;
49constexpr uint32_t CLIENT_FLOOR = 1u * 1024 * 1024;
50constexpr long KCMCP_MAJOR = 1;
56 uint32_t request_id = 0;
58 steady::time_point start;
59 steady::time_point last_progress;
60 steady::time_point deadline;
61 bool has_deadline =
false;
62 std::chrono::milliseconds progress_interval{2000};
64ActiveJob *g_job =
nullptr;
68long client_major(
const std::string &hello_json)
71 boost::property_tree::ptree pt;
72 std::istringstream is(hello_json);
73 boost::property_tree::read_json(is, pt);
74 auto kc = pt.get_child_optional(
"kcmcp");
77 for (
const auto &elem : *kc)
78 return elem.second.get_value<
long>();
85std::string server_hello()
88 o <<
"{\"kcmcp\":1,\"engine\":\"tdkc\",\"max_payload\":" << SERVER_MAX_PAYLOAD
89 <<
",\"operations\":[\"compile\",\"wmc\"]"
90 <<
",\"input_formats\":[\"dimacs-cnf\"]"
91 <<
",\"output_formats\":{\"compile\":[\"ddnnf-nnf\"],\"wmc\":[\"decimal\"]}"
92 <<
",\"features\":[\"cancel\",\"progress\"]}";
98long option_long(
const std::string &options,
const char *key,
long def)
103 boost::property_tree::ptree pt;
104 std::istringstream is(options);
105 boost::property_tree::read_json(is, pt);
106 return pt.get<
long>(key, def);
113 const std::string &msg)
119int var_of_input_uuid(
const std::string &u)
121 if (u.size() > 1 && u[0] ==
'v') {
122 try {
return std::stoi(u.substr(1)); }
catch (...) {}
137 +
"'; this engine offers compile and wmc");
143 +
"'; this engine reads dimacs-cnf");
159 }
catch (
const std::exception &e) {
167 job.start = job.last_progress = steady::now();
168 long timeout_ms = option_long(req.
options,
"timeout_ms", 0);
169 if (timeout_ms > 0) {
170 job.deadline = job.start + std::chrono::milliseconds(timeout_ms);
171 job.has_deadline =
true;
174 job.progress_interval =
175 std::chrono::milliseconds(std::max(0L, option_long(req.
options,
176 "progress_every_ms", 2000)));
184 std::ostringstream meta;
186 std::string nnf = dnnf.toNNF(var_of_input_uuid);
188 <<
",\"nodes\":" << dnnf.getNbGates() <<
",\"exact\":true}";
192 double p = dnnf.probabilityEvaluation();
193 meta <<
"{\"treewidth\":" << td.
getTreewidth() <<
",\"exact\":true}";
194 std::ostringstream val;
195 val << std::setprecision(15) << p;
199 }
catch (
const Cancelled &) {
202 }
catch (
const TimedOut &) {
205 "time budget exceeded (timeout_ms)");
209 "treewidth exceeds the supported bound");
210 }
catch (
const std::exception &e) {
216void run_session(
int fd)
218 Connection conn(fd, SERVER_MAX_PAYLOAD, CLIENT_FLOOR);
231 "expected HELLO as the first frame");
238 long major = client_major(m.
payload);
239 if (major > KCMCP_MAJOR) {
242 "this server speaks KCMCP major " + std::to_string(KCMCP_MAJOR)
243 +
"; client requires major " + std::to_string(major));
264 catch (...) {
return; }
273 handle_request(conn, m);
284 "unexpected frame type");
289int listen_unix(
const std::string &path)
291 int fd = ::socket(AF_UNIX, SOCK_STREAM, 0);
292 if (fd < 0) { perror(
"socket");
return -1; }
293 struct sockaddr_un addr;
294 memset(&addr, 0,
sizeof(addr));
295 addr.sun_family = AF_UNIX;
296 if (path.size() >=
sizeof(addr.sun_path)) {
297 fprintf(stderr,
"tdkc: socket path too long\n");
300 strncpy(addr.sun_path, path.c_str(),
sizeof(addr.sun_path) - 1);
301 ::unlink(path.c_str());
302 if (::bind(fd,
reinterpret_cast<sockaddr *
>(&addr),
sizeof(addr)) < 0) {
303 perror(
"bind");
return -1;
308int listen_tcp(
const std::string &host,
const std::string &port)
310 struct addrinfo hints, *res =
nullptr;
311 memset(&hints, 0,
sizeof(hints));
312 hints.ai_family = AF_UNSPEC;
313 hints.ai_socktype = SOCK_STREAM;
314 if (::getaddrinfo(host.c_str(), port.c_str(), &hints, &res) != 0 || !res) {
315 fprintf(stderr,
"tdkc: cannot resolve %s:%s\n", host.c_str(), port.c_str());
318 int fd = ::socket(res->ai_family, res->ai_socktype, res->ai_protocol);
319 if (fd < 0) { perror(
"socket"); freeaddrinfo(res);
return -1; }
321 ::setsockopt(fd, SOL_SOCKET, SO_REUSEADDR, &one,
sizeof(one));
322 if (::bind(fd, res->ai_addr, res->ai_addrlen) < 0) {
323 perror(
"bind"); freeaddrinfo(res); ::close(fd);
return -1;
327 struct sockaddr_storage ss;
328 socklen_t sl =
sizeof(ss);
329 if (::getsockname(fd,
reinterpret_cast<sockaddr *
>(&ss), &sl) == 0) {
330 char hbuf[NI_MAXHOST], pbuf[NI_MAXSERV];
331 if (::getnameinfo(
reinterpret_cast<sockaddr *
>(&ss), sl, hbuf,
sizeof(hbuf),
332 pbuf,
sizeof(pbuf), NI_NUMERICHOST | NI_NUMERICSERV) == 0)
333 fprintf(stderr,
"tdkc: bound %s:%s\n", hbuf, pbuf);
344 ActiveJob *job = g_job;
349 pfd.fd = job->conn->
fd();
352 if (::poll(&pfd, 1, 0) > 0 && (pfd.revents & POLLIN)) {
355 if (job->conn->
recv(m)) {
369 auto now = steady::now();
372 if (job->has_deadline && now >= job->deadline)
374 if (now - job->last_progress >= job->progress_interval) {
375 long ms = std::chrono::duration_cast<std::chrono::milliseconds>(
376 now - job->start).count();
379 "{\"phase\":\"compile\",\"elapsed_ms\":" + std::to_string(ms) +
"}");
384 job->last_progress = now;
390 ::signal(SIGPIPE, SIG_IGN);
393 if (endpoint.rfind(
"unix:", 0) == 0) {
394 lfd = listen_unix(endpoint.substr(5));
396 auto colon = endpoint.rfind(
':');
397 if (colon == std::string::npos) {
398 fprintf(stderr,
"tdkc: endpoint must be unix:/path or host:port\n");
401 lfd = listen_tcp(endpoint.substr(0, colon), endpoint.substr(colon + 1));
405 if (::listen(lfd, 16) < 0) {
406 perror(
"listen"); ::close(lfd);
return 1;
408 fprintf(stderr,
"tdkc: KCMCP server listening on %s\n", endpoint.c_str());
412 int cfd = ::accept(lfd,
nullptr,
nullptr);
414 if (errno == EINTR)
continue;
Boolean provenance circuit with support for knowledge compilation.
gate_t
Strongly-typed gate identifier.
Out-of-line template method implementations for Circuit<gateType>.
Tree decomposition of a Boolean circuit for knowledge compilation.
Boolean circuit for provenance formula evaluation.
Exception thrown when a tree decomposition cannot be constructed.
Tree decomposition of a Boolean circuit's primal graph.
unsigned getTreewidth() const
Return the treewidth of this decomposition.
Builds a d-DNNF from a Boolean circuit using a tree decomposition.
dDNNF && build() &&
Execute the compilation and return the resulting d-DNNF.
Framed message transport over one connected socket fd.
bool recv(Message &out)
Read one logical message (concatenating MORE frames).
void send(Type type, uint32_t request_id, const std::string &payload)
Send a message, splitting payload across MORE-flagged frames no larger than the peer's limit.
Constructs a d-DNNF from a Boolean circuit and its tree decomposition.
Decomposable Deterministic Negation Normal Form circuit.
gate_t parse_dimacs_cnf(const std::string &text, BooleanCircuit &c, bool weighted)
Parse text (a DIMACS CNF) into c and return the root gate.
Parse a DIMACS CNF into a ProvSQL BooleanCircuit.
Wire codec for KCMCP, the Knowledge Compiler / Model Counter Protocol (see doc/source/dev/kc-server-p...
int kcmcp_serve(const std::string &endpoint)
Serve KCMCP on endpoint until terminated.
std::chrono::steady_clock steady
The tdkc KCMCP reference server.
std::string build_result(OutputFormat fmt, const std::string &meta_json, const std::string &result)
Build a RESULT payload (result_format byte + meta JSON + result bytes).
const char * input_format_name(InputFormat fmt)
const char * output_format_name(OutputFormat fmt)
@ UNSUPPORTED_VERSION
client requires a KCMCP major this server lacks
@ UNSUPPORTED_OPERATION
unsupported operation or unknown frame type
const char * operation_name(Operation op)
OutputFormat
Output-format registry (REQUEST byte 2 / RESULT byte 0; one shared space).
std::string build_error(ErrorCode code, const std::string &message)
Build an ERROR payload (u16 code + UTF-8 message).
bool parse_request(const std::string &payload, Request &out)
Decode a REQUEST payload; returns false if structurally malformed.
A fully reassembled inbound message (MORE frames concatenated).
Thrown by Connection on a protocol violation that warrants an ERROR frame (e.g.
std::string problem
the formula bytes
std::string options
UTF-8 JSON (may be empty == {}).
OutputFormat output_format
Build-loop interrupt hook for the standalone tdkc binary.