TODO.txt

Extensions Input:
- allow gates xor, ite  (easy)
- allow non-prefix qcir during parsing (semantics?)
- allow free variables  (doable)

Preprocessing:
- eliminate pure positive/negative literals
- early quantification: more heuristics
- early quantification: should use caching in implementation?
- transform back to prenex (partially or completely)
- could transform to positive normal form. (useful?)
- further simplifications:
    - remove duplicate arguments, as in and(2,5,7,2,19)
    - remove duplicate gates, 5=and(2,3), 6=and(2,3)
    - remove empty gates (T/F), as in 5 = or(3,4), 3 = and(), 6 = and(5,3) => 6=T!

Solving:
- use parallel disjunction/conjunction

Improvements:
- statistics: intermediate timing
- take care of removed variables in returned example
- rethink defaults (in particular with prefix)

Refactor:
- refactor: Solver could be an abstract class / interface
- refactor: Try other BDD packages (or Sylvan ZDD)
- refactor: enforce bdd-manager discipline (singleton pattern?)

Suggestions for Sylvan:
- simplify initialisation (at least for non-lace use)
- vector<bool> PickOneCube(vector<uint32_t>variables) 
- map<int,bool> PickOneCube(BDDset variables)
- resolve Bdd vs Cube vs BddSet
- vector<bool> vs vector<uint_8>
- bool 0,1 versus enum {0,1,2} (don't care values)
- VariablesCube: also when not sorted!
- sylvan_quite vs quitPackage (in example)
- why is Sylvan a class? Should be sylvan_mgr? Singleton pattern?
- ask lace for number of workers? (in case initialized with 0)
- make install target is broken on trolando, works on utwente-fmt

Challenges:
- Breakthrough: all solved
- Connect4: all solved
- BSP: all solved

- Domineering/5x6_11_bnwib.qcir
- HTTT/4x4_13_skinny_bwnib.qcir
- EP/8x8_11_e-8-1_p-2-3_bwnib.qcir
- EP-dual/
- Hex/hein_02_5x5-11_bwnib.qcir
- Hex/hein_02_5x5-13_bwnib.qcir
- Hex/hein_10_5x5-11_bwnib.qcir
- Hex/hein_10_5x5-13_bwnib.qcir
- Hex/hein_11_5x5-11_bwnib.qcir
- Hex/hein_15_5x5-15_bwnib.qcir

- Benchmarks/Hein/SN_N/hein_02_5x5-11_cp.qcir (matrix)
- Benchmarks/Hein/SN_N/hein_10_5x5-11_cp.qcir (matrix)

Note: the following could only be solved, mostly with -x=2, and often only without -q=2:

./qubi Benchmarks/Hein/SN_N/browne_5x5_09_cp.qcir -s -x=2 -e -g -v=2
./qubi Benchmarks/Hein/SN_B/browne_5x5_07.pg.qdimacs.qcir -s -x=2 -e -g -v=2
./qubi Benchmarks/Hein/SN_B/hein_09_4x4-07.pg.qdimacs.qcir -e -g -v=2 -s -f -x=2
./qubi Benchmarks/Hein/SN_N/hein_08_5x5-11_cp.qcir -s -x=2 -e -g -v=2
./qubi Benchmarks/Hein/SN_N/hein_08_5x5-11_cp.qcir -s -e -g -v=2
./qubi Benchmarks/Hein/SN_N/hein_13_5x5-09_cp.qcir -s -x=2 -e -g -v=2