static be_ptr AtMostOnce( const BeEnc_ptr be_enc, const int k )
get_el_at_time
sbmcTableauLTLformula.c
be_ptr BmcInt_SBMCTableau_GetAtTime( const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int time, const int k, const int l )
AtMostOnce
Loop
get_f_at_time
sbmcTableauLTLformula.c
be_ptr Bmc_Gen_SBMCProblem( const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l )
sbmcGen.c
void Bmc_Hash_delete_table( hashPtr hash )
sbmcHash.c
int Bmc_Hash_find( hashPtr table, node_ptr node )
sbmcHash.c
void Bmc_Hash_insert( hashPtr table, node_ptr key, int data )
sbmcHash.c
hashPtr Bmc_Hash_new_htable( )
sbmcHash.c
unsigned Bmc_Hash_size( hashPtr hash )
sbmcHash.c
int Bmc_SBMCGenSolveLtl( Prop_ptr ltlprop, const int k, const int relative_loop, const boolean must_inc_length, const boolean must_solve, const Bmc_DumpType dump_type, const char* dump_fname_template )
Bmc_GenSolve_Action
sbmcBmc.c
be_ptr Bmc_SBMCTableau_GetAllLoops( const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l )
sbmcTableau.c
be_ptr Bmc_SBMCTableau_GetLoopCondition( const BeEnc_ptr be_enc, const int k, const int l )
Bmc_Tableau_GetAllLoopsDisjunction
sbmcTableau.c
be_ptr Bmc_SBMCTableau_GetNoLoop( const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k )
sbmcTableau.c
be_ptr Bmc_SBMCTableau_GetSingleLoop( const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l )
sbmcTableau.c
void Bmc_Stack_delete( Bmc_Stack_ptr thestack )
sbmcNodeStack.c
Bmc_Stack_ptr Bmc_Stack_new_stack( )
sbmcNodeStack.c
node_ptr Bmc_Stack_pop( Bmc_Stack_ptr thestack )
sbmcNodeStack.c
void Bmc_Stack_push( Bmc_Stack_ptr thestack, node_ptr node )
sbmcNodeStack.c
unsigned Bmc_Stack_size( Bmc_Stack_ptr thestack )
sbmcNodeStack.c
node_ptr Bmc_Stack_top( Bmc_Stack_ptr thestack )
sbmcNodeStack.c
static be_ptr Loop( const BeEnc_ptr be_enc, const int k )
sbmcTableauLTLformula.c
void SBmc_AddCmd( )
CInit_Init
sbmcPkg.c
void SBmc_Init( )
sbmcPkg.c
void SBmc_Quit( )
sbmcPkg.c
int Sbmc_CommandCheckLtlSpecSBmc( int argc, char** argv )
sbmcCmd.c
int Sbmc_CommandGenLtlSpecSBmc( int argc, char** argv )
sbmcCmd.c
int Sbmc_CommandLTLCheckZigzagInc( int argc, char** argv )
sbmcCmd.c
Trace_ptr Sbmc_Utils_fill_cntexample( BeEnc_ptr be_enc, sbmc_MetaSolver * solver, node_ptr l_var, const int k, Trace_ptr res )
Bmc_Utils_generate_cntexample
sbmcUtils.c
Trace_ptr Sbmc_Utils_generate_and_print_cntexample( BeEnc_ptr be_enc, sbmc_MetaSolver * solver, node_ptr l_var, const int k, const char * trace_name, NodeList_ptr symbols )
Bmc_Utils_generate_and_print_cntexample
Sbmc_Utils_generate_cntexample
Sbmc_Utils_fill_cntexample
sbmcUtils.c
Trace_ptr Sbmc_Utils_generate_cntexample( BeEnc_ptr be_enc, sbmc_MetaSolver * solver, node_ptr l_var, const int k, const char * trace_name, NodeList_ptr symbols )
Bmc_Utils_generate_cntexample
Sbmc_Utils_fill_cntexample
sbmcUtils.c
int Sbmc_check_psl_property( Prop_ptr prop, boolean dump_prob, boolean inc_sat, boolean do_completeness_check, boolean do_virtual_unrolling, boolean single_prob, int k, int rel_loop )
sbmcCmd.c
static be_ptr bmcSBMC_tableau_GF_FG_last( const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int k, const int l, const unsigned pastdepth, hashPtr table, hash_ptr memoiz )
bmc_tableau_GetEventuallyIL_opt
bmc_tableau_GetGloballyIL_opt
sbmcTableauLTLformula.c
static void bmc_cache_delete( )
bmc_init_cache
sbmcTableauLTLformula.c
static void bmc_cache_init( const int count, const int k, const unsigned pastdepth )
bmc_delete_cache
sbmcTableauLTLformula.c
static void bmc_expandFilename( const int k, const int l, const int prop_idx, const char* filename_to_be_expanded, char* filename_expanded, const size_t filename_expanded_maxlen )
sbmcBmc.c
static unsigned bmc_past_depth( const node_ptr ltl_wff )
sbmcTableauLTLformula.c
static be_ptr bmc_tableauGetEventuallyIL_opt( const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int k, const int l, const unsigned pastdepth, hashPtr table, hash_ptr memoiz )
sbmcTableauLTLformula.c
static be_ptr bmc_tableauGetGloballyIL_opt( const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int k, const int l, const unsigned pastdepth, hashPtr table, hash_ptr memoiz )
sbmcTableauLTLformula.c
static int find( hashPtr table, node_ptr node )
sbmcHash.c
static int formulaMap( hashPtr table, const node_ptr ltl_wff, unsigned TLcount )
sbmcTableauLTLformula.c
static be_ptr get_Eventually_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Globally_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Historically_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Once_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Since_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Trigger_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_Until_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_V_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_f_at_time
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_el_at_time( const BeEnc_ptr be_enc, const int time, const int k )
sbmcTableauLTLformula.c
static be_ptr get_f_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
get_g_at_time
sbmcTableauLTLformula.c
static be_ptr get_g_at_time( const BeEnc_ptr be_enc, const node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int time, const int k, const int l, const unsigned pastdepth )
sbmcTableauLTLformula.c
static be_ptr get_il_at_time( const BeEnc_ptr be_enc, const int time, const int k )
sbmcTableauLTLformula.c
static be_ptr get_loop_exists( const BeEnc_ptr be_enc, const int k )
sbmcTableauLTLformula.c
static be_ptr last_f( const BeEnc_ptr be_enc, node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int l, const int k, const unsigned pastdepth )
sbmcTableauLTLformula.c
static be_ptr last_g( const BeEnc_ptr be_enc, node_ptr ltl_wff, hashPtr table, hash_ptr memoiz, const int l, const int k, const unsigned pastdepth )
sbmcTableauLTLformula.c
node_ptr sbmc_1_fresh_state_var( SymbLayer_ptr layer, unsigned int * index )
sbmcUtils.c
int sbmc_E_state( )
sbmc_L_state
sbmc_real_k
sbmc_model_k
sbmc_real_k_string
sbmcUtils.c
int sbmc_L_state( )
sbmc_E_state
sbmc_real_k
sbmc_model_k
sbmc_real_k_string
sbmcUtils.c
void sbmc_MS_create_volatile_group( sbmc_MetaSolver * ms )
sbmcUtils.c
sbmc_MetaSolver * sbmc_MS_create( BeEnc_ptr be_enc )
sbmcUtils.c
void sbmc_MS_destroy_volatile_group( sbmc_MetaSolver * ms )
sbmcUtils.c
void sbmc_MS_destroy( sbmc_MetaSolver * ms )
sbmcUtils.c
void sbmc_MS_force_constraint_list( sbmc_MetaSolver * ms, lsList constraints )
sbmc_MS_force_true
sbmcUtils.c
void sbmc_MS_force_true( sbmc_MetaSolver * ms, be_ptr be_constraint )
sbmcUtils.c
Slist_ptr sbmc_MS_get_conflicts( sbmc_MetaSolver * ms )
sbmcUtils.c
Slist_ptr sbmc_MS_get_model( sbmc_MetaSolver * ms )
sbmcUtils.c
SatSolver_ptr sbmc_MS_get_solver( sbmc_MetaSolver * ms )
sbmcUtils.c
void sbmc_MS_goto_permanent_group( sbmc_MetaSolver * ms )
sbmcUtils.c
void sbmc_MS_goto_volatile_group( sbmc_MetaSolver * ms )
sbmcUtils.c
SatSolverResult sbmc_MS_solve_assume( sbmc_MetaSolver * ms, Slist_ptr assumptions )
SatSolver_solve_all_groups_assume
sbmcUtils.c
SatSolverResult sbmc_MS_solve( sbmc_MetaSolver * ms )
SatSolver_solve_all_groups
sbmcUtils.c
void sbmc_MS_switch_to_permanent_group( sbmc_MetaSolver * ms )
sbmcUtils.c
void sbmc_MS_switch_to_volatile_group( sbmc_MetaSolver * ms )
sbmcUtils.c
lsList sbmc_SimplePaths( const BeEnc_ptr be_enc, const state_vars_struct * state_vars, array_t * InLoop_array, const unsigned int k )
sbmcTableauInc.c
void sbmc_add_loop_variable( BeFsm_ptr be_fsm )
sbmcUtils.c
node_ptr sbmc_add_new_state_variable( SymbLayer_ptr layer, char * name )
sbmcUtils.c
sbmc_node_info * sbmc_alloc_node_info( )
sbmcStructs.c
void sbmc_allocate_trans_vars( sbmc_node_info * info, SymbLayer_ptr layer, lsList state_vars_formula_pd0, lsList state_vars_formula_pdx, unsigned int* new_var_index )
sbmcUtils.c
be_ptr sbmc_build_InLoop_i( const BeEnc_ptr be_enc, const state_vars_struct * state_vars, array_t * InLoop_array, const unsigned int i_model )
sbmcTableauInc.c
static Outcome sbmc_cmd_options_handling( int argc, char** argv, Prop_Type prop_type, Prop_ptr* res_prop, int* res_k, int* res_l, char** res_o, boolean* res_N, boolean* res_c, boolean* res_1 )
sbmcCmd.c
lsList sbmc_dependent( const BeEnc_ptr be_enc, const node_ptr bltlspec, const int k, const state_vars_struct * state_vars, array_t * InLoop_array, const be_ptr be_LoopExists, const hash_ptr info_map )
sbmcTableauIncLTLformula.c
be_ptr sbmc_equal_vectors_formula( const BeEnc_ptr be_enc, lsList vars, const unsigned int i, const unsigned int j )
sbmcTableauInc.c
lsList sbmc_find_formula_vars( node_ptr ltlspec )
sbmcUtils.c
void sbmc_find_relevant_vars( state_vars_struct * svs, BeFsm_ptr be_fsm, node_ptr bltlspec )
sbmcUtils.c
lsList sbmc_formula_dependent( const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int k_model, const hash_ptr info_map )
sbmcTableauIncLTLformula.c
hash_ptr sbmc_init_LTL_info( SymbLayer_ptr layer, node_ptr ltlspec, lsList state_vars_formula_pd0, lsList state_vars_formula_pdx, lsList state_vars_formula_aux, const int opt_force_state_vars, const int opt_do_virtual_unrolling )
sbmcTableauInc.c
void sbmc_init_state_vector( const BeEnc_ptr be_enc, const node_ptr ltlspec, const hash_ptr info_map, const unsigned int i_real, const node_ptr LastState_var, const be_ptr be_LoopExists )
sbmcTableauInc.c
node_ptr sbmc_loop_var_name_get( )
sbmcUtils.c
void sbmc_loop_var_name_set( node_ptr n )
sbmcUtils.c
node_ptr sbmc_make_boolean_formula( Prop_ptr ltlprop )
sbmcUtils.c
unsigned int sbmc_model_k( int k )
sbmc_L_state
sbmc_E_state
sbmc_real_k
sbmc_real_k_string
sbmcUtils.c
array_t * sbmc_n_fresh_state_vars( SymbLayer_ptr layer, const unsigned int n, unsigned int * index )
sbmcUtils.c
hash_ptr sbmc_node_info_assoc_create( )
sbmcStructs.c
sbmc_node_info * sbmc_node_info_assoc_find( hash_ptr a, node_ptr n )
sbmcStructs.c
void sbmc_node_info_assoc_free( hash_ptr * a )
sbmcStructs.c
void sbmc_node_info_assoc_insert( hash_ptr a, node_ptr n, sbmc_node_info * i )
sbmcStructs.c
void sbmc_node_info_free( sbmc_node_info * info )
sbmcStructs.c
void sbmc_print_Fvarmap( FILE * out, node_ptr var, node_ptr formula )
sbmcUtils.c
void sbmc_print_Gvarmap( FILE * out, node_ptr var, node_ptr formula )
sbmcUtils.c
void sbmc_print_node_list( FILE * out, lsList l )
sbmcUtils.c
void sbmc_print_node( FILE * out, const char * prefix, node_ptr node, const char * postfix )
sbmcUtils.c
void sbmc_print_varmap( FILE * out, node_ptr node, sbmc_node_info * info )
sbmcUtils.c
char* sbmc_real_k_string( const unsigned int k_real )
sbmc_L_state
sbmc_E_state
sbmc_real_k
sbmc_model_k
sbmcUtils.c
int sbmc_real_k( int k )
sbmc_L_state
sbmc_E_state
sbmc_model_k
sbmc_real_k_string
sbmcUtils.c
void sbmc_remove_loop_variable( BeFsm_ptr be_fsm )
sbmcUtils.c
hash_ptr sbmc_set_create( )
sbmcStructs.c
void sbmc_set_destroy( hash_ptr hash )
sbmcStructs.c
void sbmc_set_insert( hash_ptr hash, node_ptr bexp )
sbmcStructs.c
int sbmc_set_is_in( hash_ptr hash, node_ptr bexp )
sbmcStructs.c
state_vars_struct* sbmc_state_vars_create( )
sbmcStructs.c
void sbmc_state_vars_destroy( state_vars_struct* svs )
sbmcStructs.c
node_ptr sbmc_state_vars_get_LastState_var( const state_vars_struct * ss )
sbmcStructs.c
node_ptr sbmc_state_vars_get_LoopExists_var( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_formula_input_vars( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_formula_state_vars( const state_vars_struct * ss )
sbmcStructs.c
node_ptr sbmc_state_vars_get_l_var( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_simple_path_system_vars( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_trans_state_vars( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_translation_vars_aux( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_translation_vars_pd0( const state_vars_struct * ss )
sbmcStructs.c
lsList sbmc_state_vars_get_translation_vars_pdx( const state_vars_struct * ss )
sbmcStructs.c
void sbmc_state_vars_print( state_vars_struct * svs, FILE* out )
sbmcStructs.c
void sbmc_state_vars_set_LastState_var( state_vars_struct * ss, node_ptr f )
sbmcStructs.c
void sbmc_state_vars_set_LoopExists_var( state_vars_struct * ss, node_ptr f )
sbmcStructs.c
void sbmc_state_vars_set_formula_input_vars( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_formula_state_vars( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_l_var( state_vars_struct * ss, node_ptr f )
sbmcStructs.c
void sbmc_state_vars_set_simple_path_system_vars( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_trans_state_vars( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_translation_vars_aux( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_translation_vars_pd0( state_vars_struct * ss, lsList f )
sbmcStructs.c
void sbmc_state_vars_set_translation_vars_pdx( state_vars_struct * ss, lsList f )
sbmcStructs.c
lsList sbmc_unroll_base( const BeEnc_ptr be_enc, const node_ptr ltlspec, const hash_ptr info_map, const be_ptr be_LoopExists, const int do_optimization )
sbmcTableauIncLTLformula.c
static lsList sbmc_unroll_invariant_f( const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const be_ptr be_LastState_i, const be_ptr be_LoopExists, const int do_optimization )
sbmcTableauIncLTLformula.c
lsList sbmc_unroll_invariant_propositional( const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const int do_optimization )
sbmcTableauIncLTLformula.c
static lsList sbmc_unroll_invariant_p( const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const int do_optimization )
sbmcTableauIncLTLformula.c
lsList sbmc_unroll_invariant( const BeEnc_ptr be_enc, const node_ptr bltlspec, const int previous_k, const int new_k, const state_vars_struct * state_vars, array_t * InLoop_array, const hash_ptr info_map, const be_ptr be_LoopExists, const int opt_do_optimization )
sbmcTableauIncLTLformula.c