symbolic

Function symbolic 

Source
pub fn symbolic<B: BV>(
    ty: &Ty<Name>,
    shared_state: &SharedState<'_, B>,
    solver: &mut Solver<'_, B>,
) -> Result<Val<B>, ExecError>
Expand description

Create a Symbolic value of a specified type. Can return a concrete value if the type only permits a single value, such as for the unit type or the zero-length bitvector type (which is ideal because SMT solvers don’t allow zero-length bitvectors). Compound types like structs will be a concrete structure with symbolic values for each field. Returns the NoSymbolicType error if the type cannot be represented in the SMT solver.