CBMC
|
This is the complete list of members for propt, including all inherited members.
cnf_handled_well() const | propt | inlinevirtual |
do_prop_solve(const bvt &assumptions)=0 | propt | protectedpure virtual |
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 |
is_in_conflict(literalt l) const =0 | propt | pure virtual |
l_get(literalt a) const =0 | propt | pure virtual |
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)=0 | propt | pure virtual |
land(const bvt &bv)=0 | propt | pure virtual |
lcnf(literalt l0, literalt l1) | propt | inline |
lcnf(literalt l0, literalt l1, literalt l2) | propt | inline |
lcnf(literalt l0, literalt l1, literalt l2, literalt l3) | propt | inline |
lcnf(const bvt &bv)=0 | propt | pure virtual |
lcnf_bv | propt | protected |
lequal(literalt a, literalt b)=0 | propt | pure virtual |
limplies(literalt a, literalt b)=0 | propt | pure virtual |
lnand(literalt a, literalt b)=0 | propt | pure virtual |
lnor(literalt a, literalt b)=0 | propt | pure virtual |
log | propt | protected |
lor(literalt a, literalt b)=0 | propt | pure virtual |
lor(const bvt &bv)=0 | propt | pure virtual |
lselect(literalt a, literalt b, literalt c)=0 | propt | pure virtual |
lxor(literalt a, literalt b)=0 | propt | pure virtual |
lxor(const bvt &bv)=0 | propt | pure virtual |
new_variable()=0 | propt | pure virtual |
new_variables(std::size_t width) | propt | virtual |
no_variables() const =0 | propt | pure virtual |
number_of_solver_calls | propt | 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)=0 | propt | pure virtual |
set_equal(literalt a, literalt b) | propt | virtual |
set_frozen(literalt) | propt | inlinevirtual |
set_time_limit_seconds(uint32_t) | propt | inlinevirtual |
set_variable_name(literalt, const irep_idt &) | propt | inlinevirtual |
solver_text() const =0 | propt | pure virtual |
~propt() | propt | inlinevirtual |