Add dsl bindings to bit-vectors

[ptitjes]

This is a tentative to add dsl bindings to bit-vectors.

• Commits 1/4 and 2/4 are only adding missing bindings in Z3Context from native layer. So I guess they are OK.

• Commit 3/4 is adding dsl tree bindings only for the operations on bit-vectors. I would need advice on:

  • whether the operands are correctly named (or the symbol is appropriately chosen) in BitVectorOperands
  • what name symbol to choose for the remaining ones (shifts, rotates and no-{over|under}flow arithmetic; cf. TODO)

• Commit 4/4 is a tentative to add dsl tree nodes (and corresponding implicits) for the char Java type. This how I use them in my project, but clearly something more general could be added. I need advice on this too.

Also, please tell if the overall code quality and code style are not adequate for ScalaZ3.

[samarion]

This seems mostly fine to me (see comments in diff).

For shift operators, you probably want to use something like << and >>. Not sure about rotates. The char stuff (commit 4) seems fine to me.

[ptitjes]

Fix all the things you commented and finished BitVectorOperands' methods. For the bit-vector creation I finally used mkInt(...) with a bit-vector sort. That works perfectly. Also squashed in the fourth commit the implicits to convert from z3 ast to chars.

[samarion]

LGTM. Thanks! If you have some simple code using this, please consider adding it as a test to make sure people don't break stuff in the future.

[samarion]

Ah I hadn't noticed but this seems to break our current tests unfortunately. I think we have an issue with the implicits intTreeToIntOperand and bvTreeToBVOperand as they will both work on Val trees (they have BottomSort).

I'm not quite sure why Val is a tree with BottomSort. BottomSort doesn't exist in SMT right? It seems to me that we should be providing type class mappings from Scala types to SMT sorts. Any insights about this @colder @psuter?

[samarion]

@ptitjes by the way, depending on your application you may want to look into our more active projects Inox and Stainless (both based on Leon) which gives you a more high-level interface to the solver. The DSL there is not quite as complete as ScalaZ3's, but you get lots of other useful goodies such as tree operations, evaluators, frontends, etc.

[ptitjes]

@samarion Yeah, I've seen that while looking at your pinned projects. However, there is not much documentation on both projects and it is not clear to me which is better for what I want to do. Maybe, you have some more pointers that their readme (pages, articles, ... but preferably not slides) or you would have a little time to explain me more in private (#scala on FreeNode).

[ptitjes]

The (new) last commit handles the implicit ambiguities by removing Val[A]'s inheritance of Tree[BottomSort]. As a replacement, it makes Val be concrete and introduces a new type ValTree and corresponding new implicits.

[ptitjes]

In fact this attempt was to make it work correctly. I think the whole DSL thing would need a rework. Indeed I'd rather make a unique glue class that links a sort (eg. IntSort) , its corresponding Scala type (eg. Int) and all the methods to build corresponding constant AST object (eg. IntConstant), and operand object (eg. IntegerOperand), ...

I attempting to do that currently, but I fail to use that to factorize out the implicits (in order, for instance, to only have one implicit to build constant AST object from Scala constant value in replacement for all the <Scala-type>ValueTo<Z3Sort>Tree(...) implicit functions).

[ptitjes]

OK. I fixed it by adding an explicit abstract type definition ValSort in ValHandler for now, in order to get this PR in master if possible.

I will make a new PR for an improved glue between Scala types and Z3 sorts asap.

[samarion]

Merged, thanks!

[ptitjes]

Thank you!