CBMC
|
This is the complete list of members for dimacs_cnft, including all inherited members.
_no_variables | cnft | protected |
break_lines | dimacs_cnft | protected |
clauses | cnf_clause_listt | protected |
clausest typedef | cnf_clause_listt | |
cnf_clause_listt(message_handlert &message_handler) | cnf_clause_listt | inlineexplicit |
cnf_handled_well() const | propt | inlinevirtual |
cnft(message_handlert &message_handler) | cnft | inlineexplicit |
copy_to(cnft &cnf) const | cnf_clause_listt | inline |
dimacs_cnft(message_handlert &) | dimacs_cnft | explicit |
do_prop_solve(const bvt &) override | cnf_clause_listt | inlineprotectedvirtual |
eliminate_duplicates(const bvt &) | cnft | protectedstatic |
gate_and(literalt a, literalt b, literalt o) | cnft | protected |
gate_equal(literalt a, literalt b, literalt o) | cnft | protected |
gate_implies(literalt a, literalt b, literalt o) | cnft | protected |
gate_nand(literalt a, literalt b, literalt o) | cnft | protected |
gate_nor(literalt a, literalt b, literalt o) | cnft | protected |
gate_or(literalt a, literalt b, literalt o) | cnft | protected |
gate_xor(literalt a, literalt b, literalt o) | cnft | protected |
get_clauses() | cnf_clause_listt | inline |
get_number_of_solver_calls() const | propt | |
has_assumptions() const | propt | inlinevirtual |
has_is_in_conflict() const | propt | inlinevirtual |
has_set_to() const | propt | inlinevirtual |
hash() const | cnf_clause_listt | inline |
hash_clause(const bvt &bv) | cnf_clause_listt | inlinestatic |
is_all(const bvt &bv, literalt l) | cnft | inlineprotectedstatic |
is_in_conflict(literalt l) const override | dimacs_cnft | virtual |
l_get(literalt) const override | cnf_clause_listt | inlinevirtual |
l_set_to(literalt a, bool value) | propt | inlinevirtual |
l_set_to_false(literalt a) | propt | inline |
l_set_to_true(literalt a) | propt | inline |
land(literalt a, literalt b) override | cnft | virtual |
land(const bvt &bv) override | cnft | virtual |
lcnf(const bvt &bv) override | cnf_clause_listt | virtual |
cnft::lcnf(literalt l0, literalt l1) | propt | inline |
cnft::lcnf(literalt l0, literalt l1, literalt l2) | propt | inline |
cnft::lcnf(literalt l0, literalt l1, literalt l2, literalt l3) | propt | inline |
lcnf_bv | propt | protected |
lequal(literalt a, literalt b) override | cnft | virtual |
limplies(literalt a, literalt b) override | cnft | virtual |
lnand(literalt a, literalt b) override | cnft | virtual |
lnor(literalt a, literalt b) override | cnft | virtual |
log | propt | protected |
lor(literalt a, literalt b) override | cnft | virtual |
lor(const bvt &bv) override | cnft | virtual |
lselect(literalt a, literalt b, literalt c) override | cnft | virtual |
lxor(const bvt &bv) override | cnft | virtual |
lxor(literalt a, literalt b) override | cnft | virtual |
new_variable() override | cnft | virtual |
new_variables(std::size_t width) override | cnft | virtual |
no_clauses() const override | cnf_clause_listt | inlinevirtual |
no_variables() const override | cnft | inlinevirtual |
number_of_solver_calls | propt | protected |
process_clause(const bvt &bv, bvt &dest) const | cnft | protected |
prop_solve() | propt | |
prop_solve(const bvt &assumptions) | propt | |
propt(message_handlert &message_handler) | propt | inlineexplicit |
resultt enum name | propt | |
set_assignment(literalt a, bool value) override | dimacs_cnft | virtual |
set_equal(literalt a, literalt b) | propt | virtual |
set_frozen(literalt) | propt | inlinevirtual |
set_no_variables(size_t no) | cnft | inlinevirtual |
set_time_limit_seconds(uint32_t) | propt | inlinevirtual |
set_variable_name(literalt, const irep_idt &) | propt | inlinevirtual |
solver_text() const override | dimacs_cnft | inlinevirtual |
write_clauses(std::ostream &out) const | dimacs_cnft | protected |
write_dimacs_clause(const bvt &, std::ostream &, bool break_lines) | dimacs_cnft | static |
write_dimacs_cnf(std::ostream &out) const | dimacs_cnft | virtual |
write_problem_line(std::ostream &out) const | dimacs_cnft | protected |
~cnf_clause_listt() | cnf_clause_listt | inlinevirtual |
~cnft() | cnft | inlinevirtual |
~dimacs_cnft() | dimacs_cnft | inlinevirtual |
~propt() | propt | inlinevirtual |