Transform java boolean expressions to SMTlib

Question

I have some problems trying to transform java boolean expressions to a format that Z3 is able to understand. I cannot use any other tool for evaluating the expressions due to some of the requirements of the project. Only identifiers could be used in the expressions, not functions or more complex types.

The possibilities I have considered are:

• Build a parser using parboiled or a similar tool. The drawback for this is that I only want to move where the operator is placed after converting it to the SMT equivalent and maybe add parentheses, so this solution and the work involving AST processing seems overworked to me. Moreover, I found defining a grammar that could fit all the nested levels a bit complicated.

• Use a lexer or another kind of tool for getting the tokens and then reordering them with an algorithm similar to the Shunting-yard algorithm. In this case maybe the input should be required to have all the parentheses for avoiding some problems.

• Use a library that could parse the expression and let it be edited. So far, I have not found anything but tools that let you evaluate the expression.

• Use something that could directly transform between notations. I have been searching but I was not able to find that. It would make my day, though.

I have looked up for similar questions but I have not found anything. I will appreciate any ideas you could have. Thanks in advance!

Answer 1

Have you considered TXL? TXL provides support for parsing files, applying transformations to the abstract syntax tree and printing the result. It is easy to use, and they have a lot of documentation and a big library of grammars (Java included).

Answer 2

You could use the free software tool bc2ncf to translate your boolean expressions to CNF (Conjunctive Normal Form) rather than to SMT. Z3 is capable to input CNF and tackle the included satisfiability problem.

The commandline syntax of Z3 tends to change now and then. Some time ago, I used something like the following:

bc2cnf.exe -v test.bc.txt test.dimacs.txt

z3.exe /dimacs /v:1 test.dimacs.txt > test.solution.txt