Lots of refactoring to enable encoding solvers

src/it/scala/inox/InoxTestSuite.scala

src/it/scala/inox/solvers/SolvingTestSuite.scala

.../inox/solvers/unrolling/AssociativeQuantifiersSuite.scala

src/main/scala/inox/Context.scala

src/main/scala/inox/Options.scala

src/main/scala/inox/Program.scala

src/main/scala/inox/ast/Definitions.scala

src/main/scala/inox/ast/Extractors.scala

src/main/scala/inox/ast/Paths.scala

src/main/scala/inox/ast/Printers.scala

src/main/scala/inox/ast/SymbolOps.scala

src/main/scala/inox/ast/TreeOps.scala

src/main/scala/inox/ast/Trees.scala

src/main/scala/inox/evaluators/Evaluator.scala

src/main/scala/inox/evaluators/RecursiveEvaluator.scala

src/main/scala/inox/evaluators/SolvingEvaluator.scala

src/main/scala/inox/grammars/ExpressionGrammars.scala

src/main/scala/inox/package.scala

src/main/scala/inox/solvers/Solver.scala

src/main/scala/inox/solvers/SolverFactory.scala