Added some functionality to the API

[thorstent]

Please review and approve. Thanks.

[psuter]

Hi Thorstent,

thanks for the patches, they're very welcome. I see that this pull request is an extension of the one you closed? I was actually trying that out yesterday and my local copy of Z3 kept crashing. It's extremely unlikely to be related to your changes, which seem perfectly fine, but I'd like to find the root of the problem before I merge anyway.

[thorstent]

Hey,

My test env is windows. I build the latest branch of Z3 manually in VS2012 and compile ScalaZ3 against that. Please have a look at this pull request, it works for me.

The main thing that bugs me about these functional additions is that they are not complete, only those functions i absolutely need for my current work. Anyhow, if everyone adds what he needs we'll get closer.

Btw. you can create a solver like this and it'll magically start solving quantifiers it wouldn't solve earlier:
val tactic1 = z3.mkTactic("qe")
val tactic2 = z3.mkTactic("smt")
tactic = z3.mkTacticAndThen(tactic1, tactic2)
tactic1.delete()
tactic2.delete()
solver = z3.mkSolverFromTactic(tactic)

[psuter]

Thanks again!

[psuter]

(Also note that I reverted the hardcoding of LIB_SEPARATOR = "/" in a subsequent commit. If you need this, I'd be curious to know why.)

[thorstent]

There is a reason for that: First of all the / works fine on windows. But the \ won't work for getResourceAsStream (line 84).

[psuter]

I see, jar resources are accessed uniformly across platforms. That makes sense. Reverted my revert. Thanks.

[vo1stv]

Sounds good. I guess the tip at the bottom of http://www.inonit.com/cygwin/jni/helloWorld/load.html is confirmed and recommended.