TracePkg_execution_engine_from_string()
Converts an engine name into an engine identifier
Trace_execute_partial_trace()
Partial trace re-execution and fill-in
Trace_execute_trace()
Complete trace re-execution
bmc_add_be_into_solver_positively()
Converts Be into CNF, and adds it into a group of a solver, sets polarity to 1, and then destroys the CNF.
bmc_add_be_into_solver()
Converts Be into CNF, and adds it into a group of a solver.
extract_bdd_trace()
Extracts a complete trace Description [This function is a private service of trace_bdd_execute_partial_trace
trace_bdd_execute_partial_trace()
Executes a trace on the given fsm using BDDs
trace_bdd_execute_trace()
Executes a trace on the given fsm using BDDs
trace_exec_get_initial_state()
Builds the initial state formula
trace_exec_get_transition_relation()
Builds the transition relation formula
trace_sat_execute_trace()
Executes a trace on the given fsm using SAT solver

Last updated on 2010/05/19 22h:26