| active() const | CaDiCaL::Solver | |
| add(int lit) | CaDiCaL::Solver | |
| add_observed_var(int var) | CaDiCaL::Solver | |
| App class | CaDiCaL::Solver | friend |
| assume(int lit) | CaDiCaL::Solver | |
| build(FILE *file, const char *prefix="c ") | CaDiCaL::Solver | static |
| clause(int) | CaDiCaL::Solver | |
| clause(int, int) | CaDiCaL::Solver | |
| clause(int, int, int) | CaDiCaL::Solver | |
| clause(int, int, int, int) | CaDiCaL::Solver | |
| clause(int, int, int, int, int) | CaDiCaL::Solver | |
| clause(const std::vector< int > &) | CaDiCaL::Solver | |
| clause(const int *, size_t) | CaDiCaL::Solver | |
| close_proof_trace(bool print=false) | CaDiCaL::Solver | |
| conclude() | CaDiCaL::Solver | |
| configurations() | CaDiCaL::Solver | static |
| configure(const char *) | CaDiCaL::Solver | |
| connect_external_propagator(ExternalPropagator *propagator) | CaDiCaL::Solver | |
| connect_fixed_listener(FixedAssignmentListener *fixed_listener) | CaDiCaL::Solver | |
| connect_learner(Learner *learner) | CaDiCaL::Solver | |
| connect_proof_tracer(Tracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Solver | |
| connect_proof_tracer(InternalTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Solver | |
| connect_proof_tracer(StatTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Solver | |
| connect_proof_tracer(FileTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Solver | |
| connect_terminator(Terminator *terminator) | CaDiCaL::Solver | |
| constrain(int lit) | CaDiCaL::Solver | |
| constraint_failed() | CaDiCaL::Solver | |
| copy(Solver &other) const | CaDiCaL::Solver | |
| disconnect_external_propagator() | CaDiCaL::Solver | |
| disconnect_fixed_listener() | CaDiCaL::Solver | |
| disconnect_learner() | CaDiCaL::Solver | |
| disconnect_proof_tracer(Tracer *tracer) | CaDiCaL::Solver | |
| disconnect_proof_tracer(StatTracer *tracer) | CaDiCaL::Solver | |
| disconnect_proof_tracer(FileTracer *tracer) | CaDiCaL::Solver | |
| disconnect_terminator() | CaDiCaL::Solver | |
| DisconnectCall | CaDiCaL::Solver | friend |
| DumpCall | CaDiCaL::Solver | friend |
| failed(int lit) | CaDiCaL::Solver | |
| fixed(int lit) const | CaDiCaL::Solver | |
| flip(int lit) | CaDiCaL::Solver | |
| flippable(int lit) | CaDiCaL::Solver | |
| flush_proof_trace(bool print=false) | CaDiCaL::Solver | |
| force_backtrack(size_t new_level) | CaDiCaL::Solver | |
| freeze(int lit) | CaDiCaL::Solver | |
| frozen(int lit) const | CaDiCaL::Solver | |
| generate_cubes(int, int min_depth=0) | CaDiCaL::Solver | |
| get(const char *name) | CaDiCaL::Solver | |
| implied(std::vector< int > &implicants) | CaDiCaL::Solver | |
| inconsistent() | CaDiCaL::Solver | |
| irredundant() const | CaDiCaL::Solver | |
| is_decision(int lit) | CaDiCaL::Solver | |
| is_preprocessing_option(const char *name) | CaDiCaL::Solver | static |
| is_valid_configuration(const char *) | CaDiCaL::Solver | static |
| is_valid_limit(const char *arg) | CaDiCaL::Solver | |
| is_valid_long_option(const char *arg) | CaDiCaL::Solver | static |
| is_valid_option(const char *name) | CaDiCaL::Solver | static |
| LemmaCall | CaDiCaL::Solver | friend |
| limit(const char *arg, int val) | CaDiCaL::Solver | |
| lookahead(void) | CaDiCaL::Solver | |
| melt(int lit) | CaDiCaL::Solver | |
| Mobical class | CaDiCaL::Solver | friend |
| MockPropagator class | CaDiCaL::Solver | friend |
| ObserveCall | CaDiCaL::Solver | friend |
| optimize(int val) | CaDiCaL::Solver | |
| options() | CaDiCaL::Solver | |
| Parser class | CaDiCaL::Solver | friend |
| phase(int lit) | CaDiCaL::Solver | |
| prefix(const char *verbose_message_prefix) | CaDiCaL::Solver | |
| propagate() | CaDiCaL::Solver | |
| read_dimacs(FILE *file, const char *name, int &vars, int strict=1) | CaDiCaL::Solver | |
| read_dimacs(const char *path, int &vars, int strict=1) | CaDiCaL::Solver | |
| read_dimacs(FILE *file, const char *name, int &vars, int strict, bool &incremental, std::vector< int > &cubes) | CaDiCaL::Solver | |
| read_dimacs(const char *path, int &vars, int strict, bool &incremental, std::vector< int > &cubes) | CaDiCaL::Solver | |
| redundant() const | CaDiCaL::Solver | |
| remove_observed_var(int var) | CaDiCaL::Solver | |
| reserve(int min_max_var) | CaDiCaL::Solver | |
| reserve_difference(int number_of_vars) | CaDiCaL::Solver | |
| reset_assumptions() | CaDiCaL::Solver | |
| reset_constraint() | CaDiCaL::Solver | |
| reset_observed_vars() | CaDiCaL::Solver | |
| resources() | CaDiCaL::Solver | |
| set(const char *name, int val) | CaDiCaL::Solver | |
| set_long_option(const char *arg) | CaDiCaL::Solver | |
| signature() | CaDiCaL::Solver | static |
| simplify(int rounds=3) | CaDiCaL::Solver | |
| solve() | CaDiCaL::Solver | |
| Solver() | CaDiCaL::Solver | |
| state() const | CaDiCaL::Solver | inline |
| statistics() | CaDiCaL::Solver | |
| status() const | CaDiCaL::Solver | inline |
| terminate() | CaDiCaL::Solver | |
| Testing class | CaDiCaL::Solver | friend |
| trace_proof(FILE *file, const char *name) | CaDiCaL::Solver | |
| trace_proof(const char *path) | CaDiCaL::Solver | |
| traverse_clauses(ClauseIterator &) const | CaDiCaL::Solver | |
| traverse_witnesses_backward(WitnessIterator &) const | CaDiCaL::Solver | |
| traverse_witnesses_forward(WitnessIterator &) const | CaDiCaL::Solver | |
| unphase(int lit) | CaDiCaL::Solver | |
| usage() | CaDiCaL::Solver | static |
| val(int lit) | CaDiCaL::Solver | |
| vars() | CaDiCaL::Solver | |
| version() | CaDiCaL::Solver | static |
| write_dimacs(const char *path, int min_max_var=0) | CaDiCaL::Solver | |
| write_extension(const char *path) | CaDiCaL::Solver | |
| ~Solver() | CaDiCaL::Solver | |
