| add_binary_clause(int a, int b) | CaDiCaL::Closure | |
| add_clause_to_chain(std::vector< int >, LRAT_ID) | CaDiCaL::Closure | |
| add_ite_matching_proof_chain(Gate *g, Gate *h, int lhs1, int lhs2, std::vector< LRAT_ID > &reasons1, std::vector< LRAT_ID > &reasons2) | CaDiCaL::Closure | |
| add_ite_turned_and_binary_clauses(Gate *g) | CaDiCaL::Closure | |
| add_tmp_binary_clause(int a, int b) | CaDiCaL::Closure | |
| add_xor_matching_proof_chain(Gate *g, int lhs1, const vector< LitClausePair > &, int lhs2, vector< LRAT_ID > &, vector< LRAT_ID > &) | CaDiCaL::Closure | |
| add_xor_shrinking_proof_chain(Gate *g, int src) | CaDiCaL::Closure | |
| binaries | CaDiCaL::Closure | |
| chain | CaDiCaL::Closure | |
| check_and_add_to_proof_chain(vector< int > &clause) | CaDiCaL::Closure | |
| check_and_gate_implied(Gate *g) | CaDiCaL::Closure | |
| check_binary_implied(int a, int b) | CaDiCaL::Closure | |
| check_contained_module_rewriting(Clause *c, int lit, bool, int except) | CaDiCaL::Closure | |
| check_implied() | CaDiCaL::Closure | |
| check_ite_gate_implied(Gate *g) | CaDiCaL::Closure | |
| check_ite_implied(int lhs, int cond, int then_lit, int else_lit) | CaDiCaL::Closure | |
| check_ite_lrat_reasons(Gate *g, bool=false) | CaDiCaL::Closure | |
| check_not_tmp_binary_clause(Clause *c) | CaDiCaL::Closure | |
| check_ternary(int a, int b, int c) | CaDiCaL::Closure | |
| check_xor_gate_implied(Gate const *const) | CaDiCaL::Closure | |
| clause | CaDiCaL::Closure | |
| Closure(Internal *i) | CaDiCaL::Closure | |
| compute_rewritten_clause_lrat_simple(Clause *c, int except) | CaDiCaL::Closure | |
| condbin | CaDiCaL::Closure | |
| condeq | CaDiCaL::Closure | |
| connect_goccs(Gate *g, int lit) | CaDiCaL::Closure | |
| copy_conditional_equivalences(int lit, lit_implications &condbin) | CaDiCaL::Closure | |
| delete_proof_chain() | CaDiCaL::Closure | |
| eager_representant | CaDiCaL::Closure | |
| eager_representant_id | CaDiCaL::Closure | |
| eager_representative(int lit) | CaDiCaL::Closure | |
| eager_representative(int lit) const | CaDiCaL::Closure | |
| eager_representative_id(int lit) | CaDiCaL::Closure | |
| eager_representative_id(int lit) const | CaDiCaL::Closure | |
| extra_clauses | CaDiCaL::Closure | |
| extract_and_gates(Closure &) | CaDiCaL::Closure | |
| extract_and_gates() | CaDiCaL::Closure | |
| extract_and_gates_with_base_clause(Clause *c) | CaDiCaL::Closure | |
| extract_binaries() | CaDiCaL::Closure | |
| extract_condeq_pairs(int lit, lit_implications &condbin, lit_equivalences &condeq) | CaDiCaL::Closure | |
| extract_congruence() | CaDiCaL::Closure | |
| extract_gates() | CaDiCaL::Closure | |
| extract_ite_gates() | CaDiCaL::Closure | |
| extract_ite_gates_of_literal(int) | CaDiCaL::Closure | |
| extract_ite_gates_of_variable(int idx) | CaDiCaL::Closure | |
| extract_xor_gates() | CaDiCaL::Closure | |
| extract_xor_gates_with_base_clause(Clause *c) | CaDiCaL::Closure | |
| find_and_lits(const vector< int > &rhs, Gate *except=nullptr) | CaDiCaL::Closure | |
| find_binary(int, int) const | CaDiCaL::Closure | |
| find_conditional_equivalences(int lit, lit_implications &condbin, lit_equivalences &condeq) | CaDiCaL::Closure | |
| find_eager_representative(int) | CaDiCaL::Closure | |
| find_eager_representative_and_compress(int) | CaDiCaL::Closure | |
| find_eager_representative_lrat(int lit) | CaDiCaL::Closure | |
| find_equivalences() | CaDiCaL::Closure | |
| find_first_and_gate(Clause *base_clause, int lhs) | CaDiCaL::Closure | |
| find_gate_lits(const vector< int > &rhs, Gate_Type typ, Gate *except=nullptr) | CaDiCaL::Closure | |
| find_ite_gate(Gate *, bool &) | CaDiCaL::Closure | |
| find_large_xor_side_clause(std::vector< int > &lits) | CaDiCaL::Closure | |
| find_lit_implication_second_literal(int lit, lit_implications::const_iterator begin, lit_implications::const_iterator end) | CaDiCaL::Closure | |
| find_lrat_representative_with_marks(int lit) | CaDiCaL::Closure | |
| find_remaining_and_gate(Clause *base_clause, int lhs) | CaDiCaL::Closure | |
| find_representative(int lit) | CaDiCaL::Closure | |
| find_representative_and_compress(int, bool update_eager=true) | CaDiCaL::Closure | |
| find_representative_and_compress_both(int) | CaDiCaL::Closure | |
| find_representative_lrat(int lit) | CaDiCaL::Closure | |
| find_subsuming_clause(Clause *c) | CaDiCaL::Closure | |
| find_units() | CaDiCaL::Closure | |
| find_xor_gate(Gate *) | CaDiCaL::Closure | |
| find_xor_lits(const vector< int > &rhs) | CaDiCaL::Closure | |
| forward_subsume_matching_clauses() | CaDiCaL::Closure | |
| full_watching | CaDiCaL::Closure | |
| fully_propagate() | CaDiCaL::Closure | |
| garbage | CaDiCaL::Closure | |
| gate_sort_lrat_reasons(std::vector< LitClausePair > &, int, int except2=0, bool flip=0) | CaDiCaL::Closure | |
| gate_sort_lrat_reasons(LitClausePair &, int, int except2=0, bool flip=0) | CaDiCaL::Closure | |
| GatesTable typedef | CaDiCaL::Closure | |
| glargecounts | CaDiCaL::Closure | |
| gnew_largecounts | CaDiCaL::Closure | |
| goccs(int lit) | CaDiCaL::Closure | |
| gtab | CaDiCaL::Closure | |
| import_lazy_and_find_eager_representative_and_compress_both(int) | CaDiCaL::Closure | |
| index_gate(Gate *) | CaDiCaL::Closure | |
| init_and_gate_extraction() | CaDiCaL::Closure | |
| init_closure() | CaDiCaL::Closure | |
| init_ite_gate_extraction(std::vector< ClauseSize > &candidates) | CaDiCaL::Closure | |
| init_xor_gate_extraction(std::vector< Clause * > &candidates) | CaDiCaL::Closure | |
| internal | CaDiCaL::Closure | |
| largecount(int lit) | CaDiCaL::Closure | |
| largecounts(int lit) | CaDiCaL::Closure | |
| lazy_propagated(int lit) | CaDiCaL::Closure | |
| lazy_propagated_idx | CaDiCaL::Closure | |
| learn_binary_tmp_or_full_clause(int a, int b) | CaDiCaL::Closure | |
| learn_congruence_unit(int unit, bool=false, bool=false) | CaDiCaL::Closure | |
| learn_congruence_unit_falsifies_lrat_chain(Gate *g, int src, int dst, int clashing, int falsified, int unit) | CaDiCaL::Closure | |
| learn_congruence_unit_when_lhs_set(Gate *g, int src, LRAT_ID id1, LRAT_ID id2, int dst) | CaDiCaL::Closure | |
| lits | CaDiCaL::Closure | |
| lrat_chain | CaDiCaL::Closure | mutable |
| lrat_chain_and_gate | CaDiCaL::Closure | |
| mark_garbage(Gate *) | CaDiCaL::Closure | |
| marked(int lit) | CaDiCaL::Closure | |
| marked_mu1(int lit) | CaDiCaL::Closure | |
| marked_mu2(int lit) | CaDiCaL::Closure | |
| marked_mu4(int lit) | CaDiCaL::Closure | |
| marks | CaDiCaL::Closure | |
| maybe_add_binary_clause(int a, int b) | CaDiCaL::Closure | |
| maybe_promote_tmp_binary_clause(Clause *) | CaDiCaL::Closure | |
| merge_and_gate_lrat_produce_lrat(Gate *g, Gate *h, std::vector< LRAT_ID > &reasons_lrat, std::vector< LRAT_ID > &reasons_lrat_back, bool remove_units=true) | CaDiCaL::Closure | |
| merge_condeq(int cond, lit_equivalences &condeq, lit_equivalences ¬_condeq) | CaDiCaL::Closure | |
| merge_ite_gate_same_then_else_lrat(std::vector< LitClausePair > &clauses, std::vector< LRAT_ID > &reasons_implication, std::vector< LRAT_ID > &reasons_back) | CaDiCaL::Closure | |
| merge_literals_equivalence(int lit, int other, Clause *c1, Clause *c2) | CaDiCaL::Closure | |
| merge_literals_lrat(Gate *g, Gate *h, int lit, int other, const std::vector< LRAT_ID > &={}, const std::vector< LRAT_ID > &={}) | CaDiCaL::Closure | |
| merge_literals_lrat(int lit, int other, const std::vector< LRAT_ID > &={}, const std::vector< LRAT_ID > &={}) | CaDiCaL::Closure | |
| mu1_ids | CaDiCaL::Closure | |
| mu2_ids | CaDiCaL::Closure | |
| mu4_ids | CaDiCaL::Closure | |
| new_and_gate(Clause *, int) | CaDiCaL::Closure | |
| new_clause() | CaDiCaL::Closure | |
| new_ite_gate(int lhs, int cond, int then_lit, int else_lit, std::vector< LitClausePair > &&clauses) | CaDiCaL::Closure | |
| new_largecounts(int lit) | CaDiCaL::Closure | |
| new_tmp_clause(std::vector< int > &clause) | CaDiCaL::Closure | |
| new_unwatched_binary_clauses | CaDiCaL::Closure | |
| new_xor_gate(const vector< LitClausePair > &, int) | CaDiCaL::Closure | |
| nonces | CaDiCaL::Closure | |
| normalize_ite_lits_gate(Gate *rhs) | CaDiCaL::Closure | |
| number_from_xor_reason(const std::vector< int > &rhs, int, int except2=0, bool flip=0) | CaDiCaL::Closure | |
| number_from_xor_reason_reversed(const std::vector< int > &rhs) | CaDiCaL::Closure | |
| offsetsize | CaDiCaL::Closure | |
| produce_eager_representative_lrat(int lit) | CaDiCaL::Closure | |
| produce_ite_merge_lhs_then_else_reasons(Gate *g, std::vector< LRAT_ID > &reasons_implication, std::vector< LRAT_ID > &reasons_back, std::vector< LRAT_ID > &reasons_unit, bool, bool &) | CaDiCaL::Closure | |
| produce_ite_merge_then_else_reasons(Gate *g, int dst, int src, std::vector< LRAT_ID > &reasons_implication, std::vector< LRAT_ID > &reasons_back) | CaDiCaL::Closure | |
| produce_representative_lrat(int lit) | CaDiCaL::Closure | |
| produce_rewritten_clause_lrat(Clause *c, int execept_lhs=0, bool remove_units=true, bool=true) | CaDiCaL::Closure | |
| produce_rewritten_clause_lrat(vector< LitClausePair > &, int execept_lhs=0, bool=true) | CaDiCaL::Closure | |
| produce_rewritten_clause_lrat_and_clean(vector< LitClausePair > &, int execept_lhs=0, bool=true) | CaDiCaL::Closure | |
| produce_rewritten_clause_lrat_and_clean(std::vector< LitClausePair > &litIds, int except_lhs, size_t &old_position1, size_t &old_position2, bool remove_units=true) | CaDiCaL::Closure | |
| promote_clause(Clause *) | CaDiCaL::Closure | inline |
| propagate_equivalence(int lit) | CaDiCaL::Closure | |
| propagate_unit(int lit) | CaDiCaL::Closure | |
| propagate_units() | CaDiCaL::Closure | |
| propagate_units_and_equivalences() | CaDiCaL::Closure | |
| push_id_and_rewriting_lrat_full(Clause *c, Rewrite rewrite1, std::vector< LRAT_ID > &chain, bool=true, Rewrite rewrite2=Rewrite(), int execept_lhs=0, int except_lhs2=0) | CaDiCaL::Closure | |
| push_id_and_rewriting_lrat_unit(Clause *c, Rewrite rewrite1, std::vector< LRAT_ID > &chain, bool=true, Rewrite rewrite2=Rewrite(), int execept_lhs=0, int except_lhs2=0) | CaDiCaL::Closure | |
| push_id_on_chain(std::vector< LRAT_ID > &chain, Clause *c) | CaDiCaL::Closure | |
| push_id_on_chain(std::vector< LRAT_ID > &chain, const std::vector< LitClausePair > &c) | CaDiCaL::Closure | |
| push_id_on_chain(std::vector< LRAT_ID > &chain, Rewrite rewrite, int) | CaDiCaL::Closure | |
| push_lrat_id(const Clause *const c, int lit) | CaDiCaL::Closure | |
| push_lrat_unit(int lit) | CaDiCaL::Closure | |
| remove_gate(Gate *) | CaDiCaL::Closure | |
| remove_gate(GatesTable::iterator git) | CaDiCaL::Closure | |
| representant | CaDiCaL::Closure | |
| representant_id | CaDiCaL::Closure | |
| representative(int lit) | CaDiCaL::Closure | |
| representative(int lit) const | CaDiCaL::Closure | |
| representative_id(int lit) | CaDiCaL::Closure | |
| representative_id(int lit) const | CaDiCaL::Closure | |
| reset_and_gate_extraction() | CaDiCaL::Closure | |
| reset_closure() | CaDiCaL::Closure | |
| reset_extraction() | CaDiCaL::Closure | |
| reset_ite_gate_extraction() | CaDiCaL::Closure | |
| reset_xor_gate_extraction() | CaDiCaL::Closure | |
| resolvent_analyzed | CaDiCaL::Closure | |
| rewrite_and_gate(Gate *g, int dst, int src, LRAT_ID id1, LRAT_ID id2) | CaDiCaL::Closure | |
| rewrite_gate(Gate *g, int dst, int src, LRAT_ID id1, LRAT_ID id2) | CaDiCaL::Closure | |
| rewrite_gates(int dst, int src, LRAT_ID id1, LRAT_ID id2) | CaDiCaL::Closure | |
| rewrite_ite_gate(Gate *g, int dst, int src) | CaDiCaL::Closure | |
| rewrite_ite_gate_to_and(Gate *g, int dst, int src, size_t c, size_t d, int cond_lit_to_learn_if_degenerated) | CaDiCaL::Closure | |
| rewrite_ite_gate_update_lrat_reasons(Gate *g, int src, int dst) | CaDiCaL::Closure | |
| rewrite_xor_gate(Gate *g, int dst, int src) | CaDiCaL::Closure | |
| rewriting_lhs(Gate *g, int dst) | CaDiCaL::Closure | |
| rhs | CaDiCaL::Closure | |
| schedule | CaDiCaL::Closure | |
| schedule_literal(int lit) | CaDiCaL::Closure | |
| scheduled | CaDiCaL::Closure | |
| search_condeq(int lit, int pos_lit, lit_implications::const_iterator pos_begin, lit_implications::const_iterator pos_end, int neg_lit, lit_implications::const_iterator neg_begin, lit_implications::const_iterator neg_end, lit_equivalences &condeq) | CaDiCaL::Closure | |
| set_mu1_reason(int lit, Clause *c) | CaDiCaL::Closure | |
| set_mu2_reason(int lit, Clause *c) | CaDiCaL::Closure | |
| set_mu4_reason(int lit, Clause *c) | CaDiCaL::Closure | |
| shrink_and_gate(Gate *g, int falsified=0, int clashing=0) | CaDiCaL::Closure | |
| simplify_and_add_to_proof_chain(vector< int > &unsimplified, LRAT_ID delete_id=0) | CaDiCaL::Closure | |
| simplify_and_gate(Gate *g) | CaDiCaL::Closure | |
| simplify_and_sort_xor_lrat_clauses(const vector< LitClausePair > &, vector< LitClausePair > &, int, int except2=0, bool flip=0) | CaDiCaL::Closure | |
| simplify_gate(Gate *g) | CaDiCaL::Closure | |
| simplify_gates(int lit) | CaDiCaL::Closure | |
| simplify_ite_gate(Gate *g) | CaDiCaL::Closure | |
| simplify_ite_gate_condition_set(Gate *g, std::vector< LRAT_ID > &reasons_lrat, std::vector< LRAT_ID > &reasons_back_lrat, size_t idx1, size_t idx2) | CaDiCaL::Closure | |
| simplify_ite_gate_produce_unit_lrat(Gate *g, int lit, size_t idx1, size_t idx2) | CaDiCaL::Closure | |
| simplify_ite_gate_then_else_set(Gate *g, std::vector< LRAT_ID > &reasons_implication, std::vector< LRAT_ID > &reasons_back, size_t idx1, size_t idx2) | CaDiCaL::Closure | |
| simplify_ite_gate_to_and(Gate *g, size_t idx1, size_t idx2, int removed) | CaDiCaL::Closure | |
| simplify_unit_xor_lrat_clauses(const vector< LitClausePair > &, int) | CaDiCaL::Closure | |
| simplify_xor_clause(int lhs, Clause *) | CaDiCaL::Closure | |
| simplify_xor_gate(Gate *g) | CaDiCaL::Closure | |
| skip_and_gate(Gate *g) | CaDiCaL::Closure | |
| skip_xor_gate(Gate *g) | CaDiCaL::Closure | |
| sort_literals_by_var(vector< int > &rhs) | CaDiCaL::Closure | |
| sort_literals_by_var_except(vector< int > &rhs, int, int except2=0) | CaDiCaL::Closure | |
| subsume_clause(Clause *subsuming, Clause *subsumed) | CaDiCaL::Closure | |
| table | CaDiCaL::Closure | |
| units | CaDiCaL::Closure | |
| unmark_all() | CaDiCaL::Closure | |
| unsimplified | CaDiCaL::Closure | |
| update_and_gate(Gate *g, GatesTable::iterator, int src, int dst, LRAT_ID id1, LRAT_ID id2, int falsified=0, int clashing=0) | CaDiCaL::Closure | |
| update_and_gate_build_lrat_chain(Gate *g, Gate *h, std::vector< LRAT_ID > &extra_reasons_lit, std::vector< LRAT_ID > &extra_reasons_ulit, bool remove_units=true) | CaDiCaL::Closure | |
| update_and_gate_unit_build_lrat_chain(Gate *g, int src, LRAT_ID id1, LRAT_ID id2, int dst, std::vector< LRAT_ID > &extra_reasons_lit, std::vector< LRAT_ID > &extra_reasons_ulit) | CaDiCaL::Closure | |
| update_xor_gate(Gate *g, GatesTable::iterator) | CaDiCaL::Closure | |
