ProvSQL C/C++ API
Adding support for provenance and uncertainty management to PostgreSQL databases
Loading...
Searching...
No Matches
TreeDecompositionKnowledgeCompiler.cpp
Go to the documentation of this file.
1/**
2 * @file TreeDecompositionKnowledgeCompiler.cpp
3 * @brief Standalone @c tdkc tool: tree-decomposition-based knowledge compiler.
4 *
5 * This file contains the @c main() entry point for the standalone
6 * @c tdkc (Tree-Decomposition Knowledge Compiler) binary. It is built
7 * separately from the PostgreSQL extension (see @c Makefile target @c tdkc).
8 *
9 * Usage:
10 * @code
11 * tdkc <circuit_file>
12 * @endcode
13 *
14 * The circuit file is a text file produced by @c BooleanCircuit::exportCircuit()
15 * listing the number of gates followed by one line per gate describing its
16 * type, probability, and children.
17 *
18 * The tool:
19 * 1. Reads the circuit from the file.
20 * 2. Rewrites multivalued gates.
21 * 3. Computes a tree decomposition.
22 * 4. Builds a d-DNNF via @c dDNNFTreeDecompositionBuilder.
23 * 5. Evaluates the probability and prints it to @c stdout.
24 *
25 * Timing information is printed to @c stderr.
26 */
27#include <iostream>
28#include <fstream>
29#include <iomanip>
30
31extern "C" {
32#include <sys/time.h>
33}
34
36#include "Circuit.hpp"
37
38/**
39 * @brief Return the current time as a floating-point number of seconds.
40 * @return Current time (seconds since the epoch, with microsecond precision).
41 */
42static double get_timestamp ()
43{
44 struct timeval now;
45 gettimeofday (&now, NULL);
46 return now.tv_usec * 1e-6 + now.tv_sec;
47}
48
49/**
50 * @brief Entry point for the standalone tree-decomposition knowledge compiler.
51 * @param argc Argument count; must be 2.
52 * @param argv Argument vector; @c argv[1] is the path to the circuit file.
53 * @return 0 on success, non-zero on error.
54 */
55int main(int argc, char **argv) {
56 if(argc != 2) {
57 std::cerr << "Usage: " << argv[0] << " circuit" << std::endl;
58 exit(1);
59 }
60
61 std::ifstream g(argv[1]);
63 unsigned nbGates;
64
65 g >> nbGates;
66 std::string line;
67 std::getline(g,line);
68
69 for(unsigned i=0; i<nbGates; ++i) {
70 std::getline(g, line);
71 if(line=="IN")
72 c.setGate(std::to_string(i), BooleanGate::IN, 0.001);
73 else if(line=="OR")
74 c.setGate(std::to_string(i), BooleanGate::OR);
75 else if(line=="AND")
76 c.setGate(std::to_string(i), BooleanGate::AND);
77 else if(line=="NOT")
78 c.setGate(std::to_string(i), BooleanGate::NOT);
79 else {
80 std::cerr << "Wrong line type: " << line << std::endl;
81 exit(1);
82 }
83 }
84
85 gate_t u,v;
86 while(g >> u >> v)
87 c.addWire(u,v);
88 g.close();
89
90 try {
91 double t0, t1;
92 t0 = get_timestamp();
93
95 std::cerr << "Treewidth: " << td.getTreewidth() << std::endl;
96 t1 = get_timestamp();
97 std::cerr << "Computing tree decomposition took " << (t1-t0) << "s" << std::endl;
98 t0 = t1;
99
100 auto dnnf{dDNNFTreeDecompositionBuilder{c, c.getGate("0"), td}.build()};
101 t1 = get_timestamp();
102 std::cerr << "Computing dDNNF took " << (t1-t0) << "s" << std::endl;
103 t0 = t1;
104
105 std::cerr << "Probability: " << std::setprecision (15) << dnnf.probabilityEvaluation() << std::endl;
106 t1 = get_timestamp();
107 std::cerr << "Evaluating dDNNF took " << (t1-t0) << "s" << std::endl;
109 std::cerr << "Could not build tree decomposition of width <= " << TreeDecomposition::MAX_TREEWIDTH;
110 exit(1);
111 }
112
113 return 0;
114}
@ NOT
Logical negation of a single child gate.
@ OR
Logical disjunction of child gates.
@ AND
Logical conjunction of child gates.
@ IN
Input (variable) gate representing a base tuple.
gate_t
Strongly-typed gate identifier.
Definition Circuit.h:48
Out-of-line template method implementations for Circuit<gateType>.
int main(int argc, char **argv)
Entry point for the standalone tree-decomposition knowledge compiler.
static double get_timestamp()
Return the current time as a floating-point number of seconds.
Boolean circuit for provenance formula evaluation.
gate_t setGate(BooleanGate type) override
Allocate a new gate with type type and no UUID.
void addWire(gate_t f, gate_t t)
Add a directed wire from gate f (parent) to gate t (child).
Definition Circuit.hpp:81
gate_t getGate(const uuid &u)
Return (or create) the gate associated with UUID u.
Definition Circuit.hpp:33
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.
static constexpr int MAX_TREEWIDTH
Maximum supported treewidth.
Builds a d-DNNF from a Boolean circuit using a tree decomposition.
Constructs a d-DNNF from a Boolean circuit and its tree decomposition.