Binaries

[SHoltzen]

Add a /bin/ directory that organizes the following main binaries for interacting with the library.

• [x] bottomup_cnf_to_bdd: takes as input a CNF and outputs a BDD.
  • [x] Input argument: CNF file
    • [x] DIMACS format
    • [ ] JSON format
  • [x] Input argument: order, specifies a variable order:
    • [x] default: auto_minfill: use a min-fill heuristic to find the variable ordering
    • [x] auto_force: use the FORCE heuristic to find a variable ordering
    • [ ] manual: provide a manual variable order as a JSON file
  • [x] Input argument: strategy, specifies a compilation order (i.e., a tree describing the sequence in which clauses are conjoined together)
  • [x] default: dtree, uses the dtree decomposition of the CNF according to the variable order
  • [x] Input argument: verbose, show verbose output (timing information, hash table information, etc.)
  • [ ] Input argument: progress, show a progress bar that gives an estimate of compilation progress (fraction of compiled clauses)
• [x] bottomup_formula_to_bdd: takes as input an arbitrary logical formula and outputs a BDD.
  • [x] Input argument: formula file (in SEXPR JSON format)
  • [x] Input argument: ordering
    • [x] Default: manual, must provide a manual variable order.
    • [ ] interaction_minfill: user provides an interaction graph between variables and minfill is run to extract a good variable order
• [ ] bottomup_cnf_to_sdd: same as for BDD
• [ ] bottomup_formula_to_sdd: same as for BDD
• [ ] cnf_to_ddnnf: compiles a d-DNNF from a CNF
  • [ ] Input: a CNF file
  • [ ] Input: order, specifies a variable ordering strategy
    • [ ] Default: static_minfill, follows a static variable ordering based on the minfill heuristic on the graph
    • [ ] static_manual, user provides a manual static variable ordering
• [x] weighted_model_count: takes as input a compiled circuit and weight file and outputs the resulting weighted model count
  • [ ] Input: circuit, either a dDNNF, SDD, or BDD
  • [ ] Input: semiring, choice of semiring under which to perform the computation
    • [ ] Either f64 or rational for now; more to come later
  • [x] Input: weights A JSON file describing the weights (a dictionary mapping literals to weights)

[mattxwang]

For the progress bar feature, perhaps indicatif is the one to look at!