satcheck_glucose_simplifiert Member List

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

_no_variables	cnft	protected
add_variables()	satcheck_glucose_baset< Glucose::SimpSolver >	protected
assumptions	satcheck_glucose_baset< Glucose::SimpSolver >	protected
blue	messaget	static
bold	messaget	static
bright_blue	messaget	static
bright_cyan	messaget	static
bright_green	messaget	static
bright_magenta	messaget	static
bright_red	messaget	static
bright_yellow	messaget	static
clause_counter	cnf_solvert	protected
cnf_handled_well() const	propt	inlinevirtual
cnf_solvert()	cnf_solvert	inline
cnft()	cnft	inline
command(unsigned c)	messaget	inlinestatic
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const	messaget
cyan	messaget	static
debug() const	messaget	inline
eliminate_duplicates(const bvt &)	cnft	static
eom	messaget	static
error() const	messaget	inline
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)	messaget	static
faint	messaget	static
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_message_handler()	messaget	inline
get_mstream(unsigned message_level) const	messaget	inline
green	messaget	static
has_is_in_conflict() const	satcheck_glucose_baset< Glucose::SimpSolver >	inlinevirtual
has_set_assumptions() const	satcheck_glucose_baset< Glucose::SimpSolver >	inlinevirtual
has_set_to() const	propt	inlinevirtual
is_all(const bvt &bv, literalt l)	cnft	inlineprotectedstatic
is_eliminated(literalt a) const	satcheck_glucose_simplifiert
is_in_conflict(literalt a) const	satcheck_glucose_baset< Glucose::SimpSolver >	virtual
italic	messaget	static
l_get(literalt a) const	satcheck_glucose_baset< Glucose::SimpSolver >	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(const bvt &bv)	satcheck_glucose_baset< Glucose::SimpSolver >	virtual
cnf_solvert::lcnf(literalt l0, literalt l1)	propt	inline
cnf_solvert::lcnf(literalt l0, literalt l1, literalt l2)	propt	inline
cnf_solvert::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
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
M_DEBUG enum value	messaget
M_ERROR enum value	messaget
M_PROGRESS enum value	messaget
M_RESULT enum value	messaget
M_STATISTICS enum value	messaget
M_STATUS enum value	messaget
M_WARNING enum value	messaget
magenta	messaget	static
message_handler	messaget	protected
message_levelt enum name	messaget
messaget()	messaget	inline
messaget(const messaget &other)	messaget	inline
messaget(message_handlert &_message_handler)	messaget	inlineexplicit
mstream	messaget	mutableprotected
new_variable() override	cnft	virtual
new_variables(std::size_t width)	propt
no_clauses() const override	cnf_solvert	inlinevirtual
no_variables() const override	cnft	inlinevirtual
operator=(const messaget &other)	messaget	inline
process_clause(const bvt &bv, bvt &dest)	cnft	protected
progress() const	messaget	inline
prop_solve()	satcheck_glucose_baset< Glucose::SimpSolver >	virtual
propt()	propt	inline
red	messaget	static
reset	messaget	static
result() const	messaget	inline
resultt enum name	propt
satcheck_glucose_baset(Glucose::SimpSolver *)	satcheck_glucose_baset< Glucose::SimpSolver >	explicit
satcheck_glucose_simplifiert()	satcheck_glucose_simplifiert
set_assignment(literalt a, bool value)	satcheck_glucose_baset< Glucose::SimpSolver >	virtual
set_assumptions(const bvt &_assumptions)	satcheck_glucose_baset< Glucose::SimpSolver >	virtual
set_equal(literalt a, literalt b)	propt	virtual
set_frozen(literalt a)	satcheck_glucose_simplifiert	virtual
set_message_handler(message_handlert &_message_handler)	messaget	inlinevirtual
set_no_variables(size_t no)	cnft	inlinevirtual
set_polarity(literalt a, bool value)	satcheck_glucose_baset< Glucose::SimpSolver >
set_time_limit_seconds(uint32_t)	propt	inlinevirtual
set_variable_name(literalt, const irep_idt &)	propt	inlinevirtual
solver	satcheck_glucose_baset< Glucose::SimpSolver >	protected
solver_text()	satcheck_glucose_simplifiert	virtual
statistics() const	messaget	inline
status	cnf_solvert	protected
cnft::status() const	messaget	inline
statust enum name	cnf_solvert	protected
underline	messaget	static
warning() const	messaget	inline
yellow	messaget	static
~cnft()	cnft	inlinevirtual
~messaget()	messaget	virtual
~propt()	propt	inlinevirtual
~satcheck_glucose_baset()	satcheck_glucose_baset< Glucose::SimpSolver >	virtual