Loading...

Searching...

No Matches

cnft Member List

This is the complete list of members for cnft, including all inherited members.

_no_variables cnft protected

cnf_handled_well() const propt inlinevirtual

cnft(message_handlert &message_handler) cnft inlineexplicit

do_prop_solve(const bvt &assumptions)=0 propt protectedpure virtual

eliminate_duplicates(const bvt &) cnft protectedstatic

gate_and(literalt a, literalt b, literalt o) cnft

gate_equal(literalt a, literalt b, literalt o) cnft

gate_implies(literalt a, literalt b, literalt o) cnft

gate_nand(literalt a, literalt b, literalt o) cnft

gate_nor(literalt a, literalt b, literalt o) cnft

gate_or(literalt a, literalt b, literalt o) cnft

gate_xor(literalt a, literalt b, literalt o) cnft

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_all(const bvt &bv, literalt l) cnft inlineprotectedstatic

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) override cnft virtual

land(const bvt &bv) override cnft 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) 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 =0 cnft pure virtual

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)=0 propt pure 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 =0 propt pure virtual

~cnft() cnft inlinevirtual

~propt() propt inlinevirtual

CBMC: Member List