| add(int elit) | CaDiCaL::External | |
| add_observed_var(int elit) | CaDiCaL::External | |
| assume(int elit) | CaDiCaL::External | |
| assumptions | CaDiCaL::External | |
| check_assignment(int(External::*assignment)(int) const) | CaDiCaL::External | |
| check_assumptions_satisfied() | CaDiCaL::External | |
| check_constraint_satisfied() | CaDiCaL::External | |
| check_failing() | CaDiCaL::External | |
| check_learned_clause() | CaDiCaL::External | inline |
| check_learned_empty_clause() | CaDiCaL::External | inline |
| check_learned_unit_clause(int unit) | CaDiCaL::External | inline |
| check_no_solution_after_learning_empty_clause() | CaDiCaL::External | |
| check_satisfiable() | CaDiCaL::External | |
| check_shrunken_clause(Clause *c) | CaDiCaL::External | inline |
| check_solution_on_learned_clause() | CaDiCaL::External | |
| check_solution_on_learned_unit_clause(int unit) | CaDiCaL::External | |
| check_solution_on_shrunken_clause(Clause *) | CaDiCaL::External | |
| check_solve_result(int res) | CaDiCaL::External | |
| check_unsatisfiable() | CaDiCaL::External | |
| conclude_sat() | CaDiCaL::External | |
| conclude_unknown() | CaDiCaL::External | |
| concluded | CaDiCaL::External | |
| constrain(int elit) | CaDiCaL::External | |
| constraint | CaDiCaL::External | |
| copy_flags(External &other) const | CaDiCaL::External | |
| e2i | CaDiCaL::External | |
| eclause | CaDiCaL::External | |
| elit2ulit(int elit) const | CaDiCaL::External | inline |
| enlarge(int new_max_var) | CaDiCaL::External | |
| ervars | CaDiCaL::External | |
| export_learned_empty_clause() | CaDiCaL::External | |
| export_learned_large_clause(const vector< int > &) | CaDiCaL::External | |
| export_learned_unit_clause(int ilit) | CaDiCaL::External | |
| ext_flags | CaDiCaL::External | |
| ext_units | CaDiCaL::External | |
| extend() | CaDiCaL::External | |
| extended | CaDiCaL::External | |
| extension | CaDiCaL::External | |
| External(Internal *) | CaDiCaL::External | |
| failed(int elit) | CaDiCaL::External | |
| failed_constraint() | CaDiCaL::External | |
| fixed(int elit) const | CaDiCaL::External | inline |
| fixed_listener | CaDiCaL::External | |
| flip(int elit) | CaDiCaL::External | |
| flippable(int elit) | CaDiCaL::External | |
| force_backtrack(size_t new_level) | CaDiCaL::External | |
| forgettable_original | CaDiCaL::External | |
| freeze(int elit) | CaDiCaL::External | |
| frozen(int elit) | CaDiCaL::External | inline |
| frozentab | CaDiCaL::External | |
| generate_cubes(int, int) | CaDiCaL::External | |
| implied(std::vector< int > &entrailed) | CaDiCaL::External | |
| init(int new_max_var, bool extension=false) | CaDiCaL::External | |
| internal | CaDiCaL::External | |
| internalize(int, bool extension=false) | CaDiCaL::External | |
| is_decision(int elit) | CaDiCaL::External | |
| is_observed | CaDiCaL::External | |
| is_valid_input(int elit) | CaDiCaL::External | inline |
| is_witness(int elit) | CaDiCaL::External | |
| ival(int elit) const | CaDiCaL::External | inline |
| learner | CaDiCaL::External | |
| lookahead() | CaDiCaL::External | |
| mark(vector< bool > &map, int elit) | CaDiCaL::External | inline |
| marked(const vector< bool > &map, int elit) const | CaDiCaL::External | inline |
| max_var | CaDiCaL::External | |
| melt(int elit) | CaDiCaL::External | |
| moltentab | CaDiCaL::External | |
| observed(int elit) | CaDiCaL::External | |
| original | CaDiCaL::External | |
| phase(int elit) | CaDiCaL::External | |
| propagate_assumptions() | CaDiCaL::External | |
| propagator | CaDiCaL::External | |
| push_binary_clause_on_extension_stack(int64_t id, int witness, int other) | CaDiCaL::External | |
| push_clause_literal_on_extension_stack(int ilit) | CaDiCaL::External | |
| push_clause_on_extension_stack(Clause *) | CaDiCaL::External | |
| push_clause_on_extension_stack(Clause *, int witness) | CaDiCaL::External | |
| push_external_clause_and_witness_on_extension_stack(const vector< int > &clause, const vector< int > &witness, int64_t id) | CaDiCaL::External | |
| push_id_on_extension_stack(int64_t id) | CaDiCaL::External | |
| push_witness_literal_on_extension_stack(int ilit) | CaDiCaL::External | |
| push_zero_on_extension_stack() | CaDiCaL::External | |
| remove_observed_var(int elit) | CaDiCaL::External | |
| reset_assumptions() | CaDiCaL::External | |
| reset_concluded() | CaDiCaL::External | |
| reset_constraint() | CaDiCaL::External | |
| reset_extended() | CaDiCaL::External | |
| reset_limits() | CaDiCaL::External | |
| reset_observed_vars() | CaDiCaL::External | |
| restore_clause(const vector< int >::const_iterator &begin, const vector< int >::const_iterator &end, const int64_t id) | CaDiCaL::External | |
| restore_clauses() | CaDiCaL::External | |
| sol(int elit) const | CaDiCaL::External | inline |
| solution | CaDiCaL::External | |
| solution_size | CaDiCaL::External | |
| solve(bool preprocess_only) | CaDiCaL::External | |
| tainted | CaDiCaL::External | |
| terminate() | CaDiCaL::External | |
| terminator | CaDiCaL::External | |
| traverse_all_frozen_units_as_clauses(ClauseIterator &) | CaDiCaL::External | |
| traverse_all_non_frozen_units_as_witnesses(WitnessIterator &) | CaDiCaL::External | |
| traverse_witnesses_backward(WitnessIterator &) | CaDiCaL::External | |
| traverse_witnesses_forward(WitnessIterator &) | CaDiCaL::External | |
| unmark(vector< bool > &map, int elit) | CaDiCaL::External | inline |
| unphase(int elit) | CaDiCaL::External | |
| update_molten_literals() | CaDiCaL::External | |
| vals | CaDiCaL::External | |
| vars | CaDiCaL::External | |
| vidx(int elit) const | CaDiCaL::External | inline |
| vlit(int elit) const | CaDiCaL::External | inline |
| vsize | CaDiCaL::External | |
| witness | CaDiCaL::External | |
| ~External() | CaDiCaL::External | |
