# Simulator Configuration Options¶

Grackle has a large number of configuration options that can be set at runtime via the symbolic_config function.

## Simulation Options¶

- verbosity : integer
- Control the amount of information that the simulator prints during execution. 1 is the default; 0 supresses warning messages; and greater than 0 prints out successively more detailed information. The maximum verbosity is 10.
- use_cache : Boolean
- Controls whether the simulator uses hashing to map each symbolic expression
to a canonical term. This defaults to
`true`

, but this can be disabled to eliminate the storage required to store previously generated formulas. - prefer_symbolic_arrays : Boolean
- Controls whether the simulator will default to generating symbolic arrays
in operations. This defaults to
`false`

, but can be turned on to make greater use of symbolic arrays. - backend.bvdomain_range_limit : integer
- This controls the number of distinct subranges that are tracked for bitvector expressions that take a finite number of values.
- backend.unary_threshold : integer
- This sets the maximum number of concrete predicates that may be used to
defined a formula when using the
*unary representation*.

## Solver Options¶

- default_solver : string The solver to use when calling operations that invoke a
- solver such as check_sat or grackle_check_sat. The supported
values are
`abc`

,`blt`

,`boolector`

,`cvc4`

,`dreal`

,`sat`

(for any DIMACS solver),`yices`

,`z3`

. - abc.qbf_max_iterations : integer
- The number of iterations that ABC runs when trying to solve exists forall problems.
- blt_params : string
This contains parameters passed to BLT. The supported options are:

`-p <int>`

set denominator precision to`<int>`

`-s <int64>`

scale by`<int64>`

and round all coeff’s`-v`

enable verbose output`-y`

enable sound mode (requires Yices)

The format for combining options is

`<option1> <option2> ...`

.- boolector_path : path
- The path to find Boolector.
- cvc4_path : path
- The path to find CVC4.
- dreal_path : path
- The path to dreal.
- sat_command : string
- The command to run when calling a DIMACS compatible SAT solver. Use
`$1`

to denote the name of the solver. - yices_path : path
- The path to yices.
- z3_path : path
- The path to Z3.