Convert SMT2 to DIMACS CNF

[leonbo...@gmail.com]

Hi!
Is it possible to use Boolector to convert a problem which is in SMT2 format into DIMACS CNF format?
I read a question asking about a specific aspect of this but couldn't find it in the docu.
Thanks and BR,
David

[Mathias Preiner]

Hi David,

You can use Boolector to dump in AIGER format and then use aigtocnf from
the AIGER tools (http://fmv.jku.at/aiger/) to get the CNF:

boolector -dai -dam <input_file> | aigtocnf


Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To post to this group, send email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/boolector.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/6005bb63-a0d7-465a-92c7-95ce112acd21%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/6005bb63-a0d7-465a-92c7-95ce112acd21%40googlegroups.com?utm_medium=email&utm_source=footer>.
> For more options, visit https://groups.google.com/d/optout.