Searched refs:expl_queue (Results 1 – 5 of 5) sorted by relevance
325 q = &egraph->expl_queue; in mark_path()943 queue = &egraph->expl_queue; in build_explanation_vector()1086 assert(egraph->expl_queue.size == 0); in egraph_explain_equality()1223 assert(egraph->expl_queue.size == 0); in egraph_expand_diseq_pre_expl()1359 assert(egraph->expl_queue.size == 0);1381 assert(egraph->expl_queue.size == 0 && ! tst_bit(egraph->stack.mark, i)); in egraph_inconsistent_edge()1428 enqueue_edge(&egraph->expl_queue, egraph->stack.mark, i); in egraph_inconsistent_edge()1448 assert(egraph->expl_queue.size == 0); in egraph_inconsistent_distinct()1519 assert(egraph->expl_queue.size == 0); in egraph_inconsistent_not_distinct()1659 queue = &egraph->expl_queue; in egraph_search_for_reconcile_edge()[all …]
1398 ivector_t expl_queue; // vector used as a queue of edges (explanation queue) member
6770 init_ivector(&egraph->expl_queue, DEFAULT_EXPL_VECTOR_SIZE); in init_egraph()6906 delete_ivector(&egraph->expl_queue); in delete_egraph()
513 ivector_t expl_queue; // also for explanations member835 ivector_t expl_queue; // vector used as a queue for building explanations member
1257 init_ivector(&tmp->expl_queue, 20); in simplex_alloc_eqprop()1301 ivector_reset(&eqprop->expl_queue); in simplex_reset_eqprop()4129 v = &solver->expl_queue; in conflict_set_for_increase()4170 v = &solver->expl_queue; in conflict_set_for_decrease()4406 queue = &solver->expl_queue; in simplex_build_explanation()4472 queue = &solver->expl_queue; in simplex_explain_bound()4680 queue = &eqprop->expl_queue; in simplex_expand_th_explanation()5264 q = &solver->expl_queue; in record_derived_conflict()7496 v = &solver->expl_queue; in build_gcd_conflict()7528 w = &solver->expl_queue; in build_dsolver_conflict()[all …]