search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

Added some functionality to the API #12

Closed thorstent closed 11 years ago

thorstent commented 11 years ago

Please review and approve. Thanks.

psuter commented 11 years ago

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 commented 11 years ago

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 commented 11 years ago

Thanks again!

psuter commented 11 years ago

(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 commented 11 years ago

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

psuter commented 11 years ago

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

vo1stv commented 11 years ago

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