******************************************************************************
 *                           FuzzSMT                                          *
 ******************************************************************************

  This is a release of FuzzSMT which is a fuzzing tool for SMT formulas. See
  www.smtlib.org for more details about SMT. For more info about fuzz
  testing SMT solvers see our paper: 'Robert Brummayer and Armin Biere. 
  Fuzzing and Delta-Debugging SMT Solvers', presented at SMT'09. FuzzSMT is
  released under GPL. A copy of the license can be found in the file COPYING. 

  The fuzzer is written in Java 5. I assume that you work on a UNIX/LINUX
  system with Sun's JDK 5 or higher installed.  However, it should be easy
  to follow the introductions and to use FuzzSMT on any other operating
  system that supports Java. Note that if you do not want to compile the
  fuzzer yourself, you just need a compatible Java runtime environment
  (supporting Java 5 or higher) in order to run the fuzzer.

  To build the fuzzer, go to the working directory of FuzzSMT and run
  './build.sh'. It compiles the sources with javac and packages them into
  'fuzzsmt.jar', so a JDK is all you need. The jar is not kept in the
  repository, so this is the first thing to do after cloning. Anyone who
  would rather use Apache Ant can still type 'ant' instead; the build-file
  'build.xml' does the same thing. For UNIX/LINUX system I provide a simple
  wrapper shell script 'fuzzsmt' which is convenient to use.

  If you want to enable the debugging code of the fuzzer, then compile with
  debugging info: add '-g' to the javac line in 'build.sh', or with Ant set
  it in the build file 'build.xml':

  <javac debug="yes" srcdir="${src}" destdir="${build}"/>

  The code of the fuzzer contains assertions. If you want to enable these
  assertions at run time, you have to call the java interpreter with the
  option '-ea'. Simply add this option to the script 'fuzzsmt'. If you just
  want to run the fuzzer, skip the two steps above.

  In contrast to my previous fuzzing tool called FuzzSMTBV, FuzzSMT is not
  limited to bit-vector theories. Call 'fuzzsmt -h' to get an overview of the
  supported theories. I tried to support all theories that are supported
  by the current version of the SMT-LIB. As you can imagine it was a lot of
  work. I still have some ideas and improvements that I want to implement,
  maybe in future releases.

  The fuzzer has been designed to be highly customizable. Therefore, there
  are many commandline options available. You should experiment with them
  in order to adjust the fuzzer to your needs. Call the fuzzer with '-h' in
  order to get an overview of the available options. As the usage message is
  quite large, it is a good idea to pipe it to a pager such as less. Do not
  worry, each option has a default value, so you do not have to adjust them
  if you do not want to. I tried to configure the fuzzer with reasonable
  default values. So, if you do not want to change the default values,
  just call the fuzzer with the specified logic, e.g. 'fuzzsmt QF_IDL'.

  The fuzzer has been designed to randomize itself. Typically, for each
  option, e.g. the number of variables in the input layer, you can specify
  a minimum and a maximum value. The fuzzer randomly chooses a value within
  this domain.  This takes the load off the user, i.e. the user does not have
  to write a script that randomizes the fuzzer options. If you do not want
  this behavior, e.g. you are interested in random formulas that have exactly
  'n' variables, then simply set the minimum and the maximum value to 'n'.

  If you have comments, questions, improvements or bug reports, then just
  send them to my mail address: robert.brummayer@gmail.com 
  I will try to answer your mails as soon as possible.

  Robert


 ******************************************************************************
 *                              FuzzSMT 0.33                                  *
 ******************************************************************************
Changes in 0.3
--------------
* By default, FuzzSMT now outputs SMT-LIB2 format. To output SMT-LIB1 format put
  the -smtlib1 command line argument after the name of the logic.
* The -bulk-export option creates instances in the current directory.
  Files are named f_[0..n).smt or f_[0..n).smt2. This feature was added because the
  JVM is slow to load, the JVM takes perhaps 100ms to load, but it only takes around
  1ms to generate each instance. Using this feature means that 100 instances can be
  generated in around 200ms instead of 10s. i.e. FuzzSMT is asymptotically 100 times
  faster.
* The QF_AUFBV logic now has a default maximum number of uninterpreted predicates
  and uninterpreted functions of 2. Previously it had a maximum of zero, so no
  uninterpreted functions would be output by default.
* The LRA & QF_ABV logics have been added. No old logics have been removed, for
  instance QF_A remains even though it is not an SMT-LIB2 logic.
* The amount to rotate left and rotate right are now taken from
  [0,2 + bitwidth), previously it was in [0, bitwidth). This generates instances
  that rely on the modulo-bitwidth behaviour of rotate left/right.

Changes in 0.31
---------------
* The version number has been changed.
* QF_RDL no longer outputs single arity pluses, e.g. (+ v12). The specification of QF_RDL was changed in December 2010.
* It's possible to specify a prefix now when outputing bulk files. This is to help when multiple threads are operating in the same directory.
* The default file prefix when bulk exporting is now _file_

Changes in 0.32
---------------
* The SMT-LIB 2 bit-vector overflow-detection predicates are now generated for
  the bit-vector logics (QF_BV, QF_ABV, QF_AUFBV, QF_UFBV):
  bvnego, bvuaddo, bvsaddo, bvusubo, bvssubo, bvumulo, bvsmulo, bvsdivo.
  These are SMT-LIB 2 only, so they are never emitted in -smtlib1 mode.
  Use -no-overflow to suppress them (e.g. when targeting a solver that does
  not yet support them).
* Operators that SMT-LIB 2 declares left-associative or variadic are now
  emitted with a random number of arguments between 2 and the -nary limit,
  rather than always exactly two. This applies to the bit-vector operators
  bvand, bvor, bvadd, bvmul and bvxor, and to the core Boolean operators
  and, or, xor, =>, = and distinct. It exercises solver parser paths that
  binary-only output never reaches.
  NOTE: the default limit is 3, so the default output of 0.32 differs from
  0.31 even with no new options given. Pass -nary 2 to restore the previous
  binary-only behaviour. Like the overflow predicates, this is SMT-LIB 2
  only and never affects -smtlib1 output.
* The Boolean layer now seeds its operand pool with the constants true and
  false, so they appear in generated instances instead of never being used.
* Distinct with more than two operands is now generated, lifting a 0.31
  limitation. Because distinct over three or more Booleans is trivially false
  by pigeonhole, the n-ary form is deliberately made very rare (well under one
  occurrence in ten thousand generated instances): it stays reachable, so a
  long fuzzing run still covers the n-ary parser path, but in practice
  distinct is binary.

Changes in 0.33
---------------
* The SMT-LIB 2 FloatingPoint theory is now supported, adding the logics
  QF_FP, QF_FPLRA, QF_BVFP, QF_BVFPLRA, QF_ABVFP, QF_ABVFPLRA and
  QF_AUFBVFP. The theory was added to SMT-LIB after 0.31 was written, which
  is why it was missing.
* Generated floating point terms cover fp.abs, fp.neg, fp.sqrt,
  fp.roundToIntegral, fp.add, fp.sub, fp.mul, fp.div, fp.rem, fp.min,
  fp.max, fp.fma and ite. Generated predicates cover fp.leq, fp.lt, fp.geq,
  fp.gt, fp.eq, the seven classification predicates (fp.isNormal,
  fp.isSubnormal, fp.isZero, fp.isInfinite, fp.isNaN, fp.isNegative,
  fp.isPositive) and core = and distinct.
* All the literal forms are generated: the (fp sign exponent significand)
  triple, +oo, -oo, +zero, -zero, NaN, and the conversions from a bit
  pattern and from signed and unsigned machine integers.
* Rounding modes are drawn from the five constants, in both their short and
  their long spelling, and from declared RoundingMode variables. Use
  -mvrm/-Mvrm to control how many such variables are declared.
* Operands of an fp operator have to agree on both the exponent and the
  significand width. Where they do not, the operand is converted with the
  theory's own to_fp rather than with the extract/extend that the
  bit-vector layers use, so conversions appear throughout the output.
* Sorts are drawn from Float16, Float32, Float64 and Float128, and the
  abbreviated names are emitted about half the time. -fp-any instead draws
  arbitrary (eb,sb) pairs, bounded by -Mfpeb and -Mfpsb.
* In the mixed logics the theory boundary is crossed in both directions:
  to_fp and to_fp_unsigned build floating point terms out of bit-vectors
  and reals, and fp.to_ubv, fp.to_sbv and fp.to_real go the other way. The
  partial conversions are deliberately left unguarded, so NaN, the
  infinities and out-of-range values do reach them. -mconv/-Mconv set how
  many conversions are generated per direction.
* fp.div, fp.rem, fp.fma and fp.sqrt are not generated for sorts wider than
  Float64, i.e. for Float128 and for anything at least as wide drawn by
  -fp-any. On those sorts they bit-blast into circuits that solvers do not
  get through, and a timed out instance tells a fuzzing run nothing.
  Measured over 50 QF_FP instances with z3 5.0.0 and a ten second limit,
  leaving them out takes the timeouts from 10 to 6, the median solving time
  from 520ms to 103ms and the third quartile from 6.1s to 1.1s. Pass
  -fp-wide-ops to generate them anyway. All the other operators are
  generated on every sort, and all four are still generated on Float16,
  Float32 and Float64.
* Floating point exists only in SMT-LIB 2, so -smtlib1 together with any of
  the floating point logics is rejected rather than silently ignored.

* distinct is now generated wherever = between terms of the same sort is,
  and with 2 to -nary operands rather than always two. It reaches arrays,
  which it did not before: QF_ABV and QF_AUFBV only ever compared arrays
  with =, and QF_A and QF_AX only ever compared them two at a time. An
  n-ary distinct over arrays makes a solver reason about how many distinct
  arrays a sort can hold, e.g. five pairwise distinct
  (Array (_ BitVec 1) (_ BitVec 1)) terms are unsatisfiable by pigeonhole.
  Operands are sampled without repetition, since a distinct naming the same
  term twice is false whatever else it lists.
* Array distinct needs extensionality just as array = does, so it is
  generated only when -mxn/-Mxn ask for array comparisons. Those still
  default to 0, which keeps the output usable by solvers without
  extensionality.
* A parenthesis was missing from the bit-vector array extensionality layer,
  so every instance generated with -mxn/-Mxn above 0 was unbalanced and no
  parser would take it. The layer had never run before, since the options
  default to 0.

Limitations
-----------
* No QF_UFFPDTNIRA: it needs algebraic datatypes, which are not generated
  for any logic.
* A binary distinct may name the same term twice, i.e. be trivially false.
  Only the n-ary form samples without repetition.
* The arrays in QF_ABVFP, QF_ABVFPLRA and QF_AUFBVFP are bit-vector indexed
  arrays of bit-vectors. Arrays with floating point elements are not
  generated.
* The LRA output is the same as QF_LRA, i.e. no variables are quantified over.
* No UFLRA & UFNIA logics. Both logics have benchmarks, but aren't currently listed on:
	http://goedel.cs.uiowa.edu/smtlib/logics.html
* Sometimes QF_UFBV outputs divisions where the denominator isn't constrained to be non-zero.

Testing of 0.31
---------------
Example validation. The below script was run for a while; Z3 2.16 & "CVC3 2010-09-25" were able to parse most of the generated instances.

while [ 1 -eq 1 ]; do
	for t in  'QF_ABV' 'QF_AUFBV' 'QF_AUFLIA' 'QF_AX' 'QF_BV' 'QF_IDL' 'QF_L
IA' 'QF_LRA'  'QF_NIA' 'QF_NRA'  'QF_RDL' 'QF_UF' 'QF_UFBV' 'QF_UFIDL' 'QF_UFLIA
' 'QF_UFLRA' 'QF_UFNRA'   'AUFLIA' 'AUFLIRA' 'AUFNIRA' 'LRA' ; do
		java FuzzSMT  $t -bulk-export 100 
		for f in `ls -1 _file_*.smt2` ; do
			cvc3=`(ulimit -t 25; cat $f | ~/tools/cvc3_ex -lang smt2)`
			z3=`(ulimit -t 25;z3 MBQI=true ELIM_QUANTIFIERS=true $f)
`			z3=`echo $z3 | rev | cut -d " " -f1 | rev`
			echo $cvc3 $z3
			if [ "$cvc3" = "sat" -a "$z3" = "unsat" ]; then
				mv $f `tempfile --directory=cvc3`
			fi
			if [  "$cvc3" = "unsat" -a "$z3" = "sat"  ]; then
				mv $f `tempfile --directory=cvc3`
			fi
		done
	done
done