does smtpp simplify?
xa72 opened this issue · 1 comments
Hi. Myebe this is a stupid question. I read on the veriT-Homepage that smtpp offers
simplifications and transformations of SMT-LIB problems (term normalization, constant propagation) as pre- or post-processing steps.
I colud compile it and run it, but I don't understand the switches to simplify a given SMT2-file (or is it -preLA and I just don't see the effect). I would like to drop unused variables, to simplify expressions and so on. I have a computer generated SMT2 file with a lot of noise and redundant things.
Thanx for your answer.
Cheers Alex
PS: to compile, I had to adapt ./configure after autoconf, because Ubuntu comes with ocamlc 04.05.0 but you allow only up to 04.04*. After this, I could compile and run it without problems.
Hey @xa72,
The wording on veriT's homepage actually states that "Our goal is to offer a platform to develop" the analyses you mentioned. We do have a platform (though unmaintained, see below) but it does not claim to have them. In particular, term normalization or constant propagation is not done.
Be also aware SMTpp has been unmaintained for the last 4 years or so. This explains the fact that the configure does not know about ocaml 4.05. The code should work as is with ocaml 4.10 as well, though.
Now, SMTpp -rm-unused option in the devel branch should do what you want regarding removing unused variables.