.. _config_chapter: Simulator Configuration Options =============================== Grackle has a large number of configuration options that can be set at runtime via the :ref:`symbolic_config_fun` 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 :ref:`math_check_sat` or :ref:`llvm_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 `` set denominator precision to ```` - ``-s `` scale by ```` and round all coeff's - ``-v`` enable verbose output - ``-y`` enable sound mode (requires Yices) The format for combining options is `` ...``. 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.