45 gettimeofday (&now, NULL);
46 return now.tv_usec * 1e-6 + now.tv_sec;
55int main(
int argc,
char **argv) {
57 std::cerr <<
"Usage: " << argv[0] <<
" circuit" << std::endl;
61 std::ifstream g(argv[1]);
69 for(
unsigned i=0; i<nbGates; ++i) {
70 std::getline(g, line);
80 std::cerr <<
"Wrong line type: " << line << std::endl;
95 std::cerr <<
"Treewidth: " << td.
getTreewidth() << std::endl;
97 std::cerr <<
"Computing tree decomposition took " << (t1-t0) <<
"s" << std::endl;
102 std::cerr <<
"Computing dDNNF took " << (t1-t0) <<
"s" << std::endl;
105 std::cerr <<
"Probability: " << std::setprecision (15) << dnnf.probabilityEvaluation() << std::endl;
107 std::cerr <<
"Evaluating dDNNF took " << (t1-t0) <<
"s" << std::endl;
@ 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.
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).
gate_t getGate(const uuid &u)
Return (or create) the gate associated with UUID u.
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.