Which tool is the best to convert clauses in CNF (or even better DIMACS CNF)?

Question

I am automatically generating clauses like this with a C++ program:

((((((condition1#0 and not action1#0 and not action2#0 and TRUE) and (action1#1 and not action2#1 and not condition1#1 and TRUE) and TRUE)) or (not action1#0 and not action2#0 and not condition1#0 and action2#1 and not action1#1 and not condition1#1 and TRUE) or FALSE)))

I need then to check their satisfiability with some tool (something like MiniSat), but before inputing them in such a tool I need to convert them in DIMACS CNF, do you know any tool that can do it automatically for me?

Thank you!

Edit:

Also a non-CNF sat solver would work fine!

Answer 1

In pysmt there is a parser called human readable parser (hrparser) that should be able to parse those expressions. [1] .

Pysmt is integrated with both picosat and the cudd bdd package,so that you can check for satisfiability easily. In general, smt solvers are more flexible in the structure of the input (non cnf) . If you can change the output of the c++ code, it might be easy enough to create an smtlib file and use an smt silver (eg yices, z3, or cvc4).

Note: I am one of the developers of pysmt [1] http://pysmt.readthedocs.io/en/latest/_modules/pysmt/parsing.html#HRParser