Introduce new solver combinators

- RewritingSolver
- DNFSolver
- UnrollingSolver
Re-introduce type hierarchy for solvers, simplify factories

Solvers wrap solvers or factories, depending on the needs.
Factories no longer wrap factories, except for the special case of
timeoutsolverfactories (it does it in a typesafe way though).

Fix TupleRewrite with new posts, fix ScopeSimplified, Fix pretty printer
Starting create a BIG testcase :-)
Add 99-scala problems and solutions
Using filters for filtering simplify rules

src/main/scala/leon/solvers/lemmafilter/TrivialFilter.scala:
  - I remove checking @lemma because rewriting rules can be created from
    non-lemma annotation function definition

src/main/scala/leon/solvers/lemmafilter/Z3Lemmas.scala:
  - ...

new file:   src/main/scala/leon/solvers/rewriter/Filtering.scala
  - A wrapper for calling filters for rewrite rules. We can call a list
    of filters but now, only the first one (head) will be called

src/main/scala/leon/verification/NewAnalysisPhase.scala:
  - Calling filtering from Filtering object
Update README.md for installing python-numpy

User has to install python-numpy for running MaSh filter
Merge remote-tracking branch 'lara-leon/master'

Conflicts:
	src/main/scala/leon/solvers/z3/FairZ3Solver.scala
	src/main/scala/leon/synthesis/Synthesizer.scala

The lara-leon/master has a clearer interface for Solvers

- I remove timeout function out of uninterpretedSolver
- Fixed some mistakes when merging ;)
Fix bug cause by merge :|

- Forgot use simplified vc :(
- Adjust for correct time watching
- Change from simplifyLets into expandLets
Another mistake when merging.

But this error helps me saw the problem with Simp-tac.

Sometime it runs too slow and makes a forever-running.
I'll take a closer look into it later.

- I change test regression into alphabet filename order. This makes us
	easier to predict what file is tested, and also make the output more
	beautiful ;)
resolve #4 for speed up simplifier by using a map

- Remove code block which adds redundence rewrite rules
Resolve #7, Added timeout and remove `choose rule`

 - Default timeout = 1 sec
 - Default size expand = 8 x `original size`
 - Remove rewrite rules which contains Choose expression
 - Simplify now works with `--feelinglucky` option
 - Silent reporter for simplify solver
 - Improve speed of simplifer solver by re-use checkSAT-solvers
 - Improve speed of simplify by only checking SAT if we have
	 `proofContext.size > 0` and check if all conditions are simplified to
	 `true` boolean literal
Some ways for improving performance

  - Add --profiling option, which Leon waits 10 sec for profiler
	- Run Simp-solver without Timeout for speed up
	- Run Function invocation appy without checking type for speed up
Create big testcase, resolve #5

Merge all testcase from purescala regression test
A little improvement :p

Result report will show [nothing] whenever simplify return 'true' value.
Modify re-run testcases with new format.

Some unknown problem with nat* testcase, ref #10
resolve #9. Now we can disable timeout.

- #9 may cause by simplify timeout when convert new form back to the
	original form (we need that convert for isInstanceOf[Cons] case)

- Now, converting progress only use convert rules. No other rules can
	effect this progress

- Also, timeout can not effect this too
Resolved #12
Resolved #13
Resolved #14
Remove Z3 from simplify

- We only use simplify itself for checking conditions
- Removing recursive rewrite rules
- Reset regression test cases (many case now failed :|)
- Need improve simplify solver!
- Now, we don't add inductive hypothesis when function has precondition
	(can be improved later)