Benchmark Scrambler

This year we intend to use the same scrambler as in 2008, modified slightly to be aware of new SMT-COMP divisions and to handle non-standard SMT-LIB formulas in many :pat annotations in UFNIA benchmarks. The implementation is thanks to Aaron Stump.

• Source tarball

To build: tar xfz scrambler.tgz; cd scrambler; make allj
To use: java -jar scrambler.jar [+pats] seed file.smt

+pats (if specified) directs the scrambler to scramble (but leave in) :pat annotations in quantified logics, rather than the default of removing them.

[seed] is a seed for the pseudo-random number generator.

You can do "make" instead of "make allj", if you have gcj installed. The executable will then appear in opt/.

The scrambler performs the following functions:

• it drops annotations (except for :pat annotations when +pats is specified);
• it hides benchmark name and status;
• it renames all variables; and
• it randomly permutes arguments to AC logical connectives and theory function symbols.

Last modified: Tue 17 Feb 2015 15:03 UTC