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-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.