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.