Fix a bug in ocaml build script (echo -n is not supported on OSX,
use /bin/echo instead)

Refactor the tracing code, store the whole tree structure in a javascript array and handle it from the javascript side.

Cosmetic changes (whitespaces) and add comments at the top of the .str files to load the correct emacs-mode when editing.

Update to latest master of remake.
Add a workaround to silence the linker warning when building remake in the configure script.

Refactor HTML Tracing to not depend on external files (style, javascript). Add a general facility to turn a file into an OCaml string. The content of file.ml.str is turned into let content = "..." in  a file file.ml.

Refactor the run module, moving out of the Make functor everything that can be moved. Slightly improve the cache module by avoiding one comparison during find on some cases and remove manual call to Gc.compact in main, since it does not seem to help.

Resurect the HTML trace. Now generates a single HTML file containing the SVG.

Rename xmark test files so that the name order respects the size order.
Fix the gen_xmark script.

Fix a bug in the test-complexity script and add more test cases.

Speed-up the run function by keeping only the set of node to be satified for each node.

WIP

Split the formula cache into a top-down and bottom-up cache.

Remove some unneeded code that was slowing down the run function.

Add missing tests for xmark_0.xml file.

Add the results of reference implementations back.

Fix typos int the test file generation script.

Add generated test files to .gitignore

Refactor the testing infrastructure.

Refine the run to have a different set of states to satisfy while going td/bu.

Fix a bug in the build script that was causing some .cmo files to have a false dependency on .cmx files.

Replace "unsafe" function tempnam by custom code.

Make remake print "Entering/Leaving directory `foo'" if it changes the current working dir.

Add a target to run tests with the bytecode version of the program.

Update to master version of remake.

Cosmetic changes (truncate long lines, remove trailing spaces…)

Implement the ranked automata evaluation to guarantee a O(|D|x|Q|)
worst case complexity. The states of an automaton are given a rank (an
integer) such that if rank(q) = i, then state q can be satisfied
during run i at the latest. The maximum rank of a state is bounded by
the number of "bi-directional" states, that is, the number of states
which depends at the same time on a state upward and on another state
downard. Therefore, the rank is at most |Q|. For the moment, we
evaluate state [q] *only* during run i. This implies the O(|D|x|Q|)
overal complexity but also means we loose a chance to discard (or
accept) [q] early. A heuristic could improve that.

Add a tiny XML file to help debug automata behaviour.

Put the move type of automata in a Move module and add auxiliary function to create and maintain tables indexed by moves. Use it to return the states of a forumla by move.

Add a utility function Boolean.iter that iterates a function over a formula.

Remove useless cycles in the generated automaton. A state now only has at most one trivial cycle with itself.

Silence an unused variable warning.

Print detailed statisticts of the run.

Add a script to output the number of states/running time/number of traversal for increasing query sizes.

Fix a bug in the compilation of * tests.

Add the .mly and .mll files as dependencies of the generated .ml

Refactor HTML tracing utility. Color the nodes that are in the same
sat configuration in the same color.

Increase the size of the border of selected nodes in the html trace.

Also print the number of states when printing automata.

Do not update the run if the todo set is empty for the current node.

Rewrite the HTML debugging output to generate an svg file directly instead going
through graphviz.

Add fold_left/right functions to the set interface (iterate in
increasing/decreasing order of keys).

Implement set-theoretic operation on 2WSATA (union, intersection,
negation, difference).

Implement reverse mapping from preorder to nodes.

Improve performance of parallel run by replacing standard hashtable with
Cache.N1 array.

Lowlevel optimizations in the Ptset module, replace some function
calls by a field access, use bit twidling hack to compute the
largest power of two inferior to a given value (was previously done
with log(WORDSIZE * 8) branching + table lookup).

Do not stupidely recompute a constant set of states for each node
in the tree, compute it once and for all before the run and store it
at each node as we traverse them.

Improve performances by moving the caching outside of the saturation
of the set of states of the current node (instead of caching and
looking-up at each step)

Drastically improve performances by simplifying the book-keeping
of pending transitions during a topdown run.
Before:
      - we were keeping for each node
        (1) sat: the set of states satisfied at that node
        (2) unsat: the set of states unsatisfied at that node
        (3) todo: the hashconsed list of pending transitions (of the
            form q, {a,b,c} -> f
            where f has been simplified w.r.t to sat and unsat (that is
            atoms containing states in either have been simplified to True
            or False) and q is neither in sat nor unsat.
      - during each run, for each node, we were scanning todo and rebuilding
        it removing satisfied or unsatisfied transitions. This lead to excessive
        hashconsing, and a lot of time spent in the hashconsing module (in turn
        spending a lot of time in the GC)
After:
       - we keep for each node:
         (1) sat: the set of states satisfied at that node
         (2) todo: the set of undetermined *states*
       - we perform the book-keeping as before but do not materialize the
         simplified transitions. Also unsat is made inplicit (a state is
         unsat if it is neither in sat nor todo).

Revert "Tentative optimization"

This reverts commit e9b4969905125718589b18ff6286e05688f7a929.
Avoiding the computation of a simplified formula does not help.

Add gmon.out to .gitignore

Tentative optimization

Factor Remakefie  and add more tests for parallel query composition.

Add Makefile to .gitignore

Add a Makefile to drive the build process.

Fix invalid variable substitution in buildscript.

Update the output of the reference implementation to the new format.

Remove un-needed scripts

Factorise common bits of Remakefile in tools/ocamldriver.sh

Refactor the build process. Piggyback on remake's dependency tracking
to perform a topological sort of the object files, used during linking.
This is done by generating a .dep file for each object file keeping in
a .dep the transitive closure of its dependencies.
Also, packed modules must now be described by:
- a directory
- a file with the .pack extension, with the same basename as the directory,
listing the module names (relative to the directory containing the .ml files)

Add more tests (broken, needs a refactoring of the build script)

Add tests for parallel query evaluation.

Implement the multiple-starters feature:
- implement automata merging and concatenation
- change the command line parsing to allow multiple queries
- update the output format to denote which query a result set belongs to
- implement full evaluation of automata (associate each selecting state
with its result set)

Given queries Q1 ... QN on the command line, we can now:
- compute Q1, then Q2, ... , then QN on the same document, sequentially
- build one automaton that computes Q1, ..., QN in parallel
- compute QN(... Q2(Q1(root))) sequentially (materializing intermediate
results)
- build one automaton that computes QN(...(Q2(Q1(root)))) in one run.

Change command line options:
       * -d, --doc set the input document (default to stdin)
       * -o, --out set the output file (default to stdout)

Implement copy and composition of automata.

Preliminary work for multiple starters evaluation.

Refactor the Ata module:
         - add a builder class to ensure we only manipulate well-formed automata
         - move all the caching infrastructure to the computation of the run
         - rename the Eval module to Run

Sanitize the representation of formula
- rename the toplevel Formula module to Boolean
- rename Ata.SFormula to Formula
- move the flag saying whether an atom is positive or negative
  to Boolean
- distinguish predicates that are moves from generic predicates.

Add a bullet symbol.

Add an int_of_bool cast function.

Add an interface for the evaluation module.

Make remake change to the directory where ./remake (and the Remakefile) are.

Remove the timestamp header in source files. This information is
better kept in git.

Fix a bug where the content of variables are appended instead of being
overwritten. Thus, when several sub-process send variable A=foo to the
server, the content of A becomes foofoofoofoo instead of just foo.

Fix a typo which causes mis-detection of the ocaml-expat bindings.

Migrate to new remake.

Remove the 'round' counter from the hashconsed configurations.

Add a clean logger infrastructure.

Add a bitmap to keep track of whether a subtree needs to be
recomputed or not.
A subtree needs to be recomputed when:
(1) it's todo transition list is not empty or
(2) one of its subtrees needs to be recomputed.

Introduce a bitvector module to efficiently represent arrays of
booleans.

Update test results.

Make the html trace tools use colors to represent the round at
which an node was satisfied.

Add a new test suite.

Cosmetic changes.

Add generated files to the .gitignore.

Last tweaking of the Remakefile for automated testing.

Tune the Remakefile to re-run tests when the binary changes.

Use the Remakefile to perform non-regression tests.

Implement command line options, clean-up screen output.

Merge branch 'feature/precise-sat'

Hashcons transition evaluation based on node configuration.

Store a summary of the node (kind, topology) in the Ata.Config.t type.

add OCaml object files to .gitignore

Hash-conses each node configuration.

Fix the Remakefile and testing script.

Maintain the set of unsatisfiable states.

Fix the Remakefile and testing script.

Add an INSTALL file.

Re-organize the Remakefile.
Fixes a few typos and make remake.cpp callable from subdirectories.

Make the main target more generic, to allow compilation of
tools/*.native too, instead of only src/*.native.

Add a distclean target that removes every file generated by the
configure/remake scripts.

Modified building instructions.