coreStar now uses Z3 expressions for everything

- this commit is incomplete: tests that use function arguments do not
  work yet. Next commit on the way. Everything but arguments should be
  functional right now.

- removed prover/expression.ml{,i}, replaced by prover/syntax.ml{,i}

  this module defines helpers for coreStar's specific representation
  of formulas, eg variables manipulations, mk_emp, mk_star, as well as
  generally useful shorthands such as on_or, on_app, on_big_star, ...

  Things generally missing from Z3's API go there (eg expr_equal... we
  should probably bug report some of those upstream!). For everything
  else, use Z3's API directly (eg Z3.Boolean.mk_and to build a boolean
  conjunction expression)

  The name change for the module is due to the fact that it's about
  expressions, but also sorts, etc., ie everything syntax. I think it
  makes more sense but YMMV

- every expression now comes with a type

  this is a side-effect of moving our expression representation to Z3

- in particular, out and in arguments of functions are typed

  thus, they are not the same for every function, which entailed some
  changes here and there as we need to keep track of this info per
  function, per triple, and per assign/call statements.

- function and triples arguments and return values are now named

  Got rid of @parameter0:, $ret_v1, etc., which I think is for the best
  anyway because this syntax was ugly? Since we have to give the type of
  each of these variables now, we might as well choose their names while
  we're at it.

- the parser assumes everything not at the predicate level to be
  integers, for simplicity

  This avoids defining a syntax for declaring types, etc. for now.
  Front-ends will be using the coreStar and Z3 APIs directly anyway and
  are free to define their own syntax and typing mechanism.
syntax for parameters and return variables, and taking them into account

This syntax is bad and I feel bad.

Substitution of parameters and return values works better now (there was
a bug in symexec.ml).

It would still be nice to check numbers of parameters/return values
after parsing to get error messages instead of runtime exceptions.
reuse StringHash in syntax.ml (Radu's review)
merge with alt-abd branch
updated abstraction.ml to use Z3.Expr module
renamed Prover.is_true to Prover.is_emp
Merge remote-tracking branch 'origin/z3integration' into alt-abd

Conflicts:
	TODO
	src/prover/expression.ml
	src/prover/expression.mli
	src/prover/prover.ml
	src/symexec/symexec.ml
	tests/infer_tests/cfg.star