Add README and INSTALL file

INSTALL.adoc

+
+== Compilation
+
+ With http://opam.ocaml.org/[opam] the needed library can be installed
+
+[source,sh]
+opam install ounit zarith ocamlgraph cryptokit
+
+
+Then the compilation is done in the directory with:
+
+[source,sh]
+make
+
+It builds the binary `popop.native`
+
+== Tests
+
+The tool can be tested by running
+
+[source,sh]
+make tests
+
+The tests are composed by unit tests, hand written tests and
+delta-debugged bugs. Moreover part of the solver that need to do an
+arbitrary choice are randomized in 10 different ways (using the
+`--seed` argument of `popop.native` and `tests.native``). Example of
+such arbitrary choices are:
+* which class becomes the representative during a merge
+* on which class to do the pivot during the equality of linear arithmetic
+  polynomial
+* in which order the arguments of associative and commutative
+  operators are parsed and treated.
+
+This fuzzing of the tests allows to exercise more behavior with the
+same number of tests. Often a bug can be found with one seed but will
+avoid a bug when tested with another seed. However we don't use a
+random seed because we want a commit to succeed or fail the tests in a
+deterministic way.

README.adoc

+
+== Popop
+
+Popop is a solver based on an extension of MC-SAT framework developed
+in the SOPRANO ANR project. It proposes an architecture allowing easy
+additions of new domains and theories.
+
+It features parsers for:
+* Dimacs
+* SMTLIB
+* Alt-Ergo language
+
+== Roadmap
+
+Two main parts remain to be done in the implementation of Popop:
+theories and the conflict framework. The current conflict framework is
+functional and very generic however it is quite hard to use, so when
+working on new theories we will have to factorize the boilerplate and
+simplify the API as possible. For the theories the current roadmap is:
+
+* reimplement the rational linear arithmetic theory and extend it
+* finish the implementation of bitvectors on bitvectors operators
+* structures, algebraic datatypes, arrays
+* floating point
+* non-linear rational arithmetics
+* integer linear arithmetic and bitvectors on arithmetic operators

_tags

+true: -traverse