Simulator Configuration Options¶
Grackle has a large number of configuration options that can be set at runtime via the symbolic_config function.
- 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.
- default_solver : string The solver to use when calling operations that invoke a
- solver such as check_sat or grackle_check_sat. The supported
sat(for any DIMACS solver),
- 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
-s <int64>scale by
<int64>and round all coeff’s
-venable verbose output
-yenable 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
$1to denote the name of the solver.
- yices_path : path
- The path to yices.
- z3_path : path
- The path to Z3.