qbf_bdd_certificatet Member List

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

_no_variables	cnft	protected
add_existential_quantifier(const literalt l)	qdimacs_cnft	inline
add_quantifier(const quantifiert &quantifier)	qdimacs_cnft	inlinevirtual
add_quantifier(const quantifiert::typet type, const literalt l)	qdimacs_cnft	inline
add_universal_quantifier(const literalt l)	qdimacs_cnft	inline
bdd_manager	qbf_bdd_certificatet	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(qdimacs_cnft &cnf) const	qdimacs_cnft
dimacs_cnft::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
f_get(literalt l) override	qbf_bdd_certificatet	virtual
find_quantifier(const literalt l, quantifiert &q) const	qdimacs_cnft
function_cache	qbf_bdd_certificatet	protected
function_cachet typedef	qbf_bdd_certificatet	protected
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	qdimacs_cnft
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
is_in_core(literalt l) const =0	qdimacs_coret	pure virtual
is_quantified(const literalt l) const	qdimacs_cnft
l_get(literalt a) const override	qbf_bdd_certificatet	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) 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
M_COMPLEX enum value	qdimacs_coret
M_DONTCARE enum value	qdimacs_coret
M_FALSE enum value	qdimacs_coret
m_get(literalt a) const =0	qdimacs_coret	pure virtual
M_TRUE enum value	qdimacs_coret
model_bdds	qbf_bdd_certificatet	protected
model_bddst typedef	qbf_bdd_certificatet	protected
modeltypet enum name	qdimacs_coret
new_variable(void) override	qbf_bdd_certificatet	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
operator==(const qdimacs_cnft &other) const	qdimacs_cnft
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
qbf_bdd_certificatet(void)	qbf_bdd_certificatet
qdimacs_cnft(message_handlert &message_handler)	qdimacs_cnft	inlineexplicit
qdimacs_coret(message_handlert &message_handler)	qdimacs_coret	inlineexplicit
quantifiers	qdimacs_cnft
quantifierst typedef	qdimacs_cnft
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_quantifier(const quantifiert::typet type, const literalt l)	qdimacs_cnft	virtual
set_time_limit_seconds(uint32_t)	propt	inlinevirtual
set_variable_name(literalt, const irep_idt &)	propt	inlinevirtual
simplify_extractbits(exprt &expr) const	qdimacs_coret
solver_text() const override	qdimacs_cnft	inlinevirtual
symbol_mapt typedef	qdimacs_coret
variable_map	qdimacs_coret
variable_mapt typedef	qdimacs_coret
write_clauses(std::ostream &out)	dimacs_cnft	protected
write_dimacs_clause(const bvt &, std::ostream &, bool break_lines)	dimacs_cnft	static
write_dimacs_cnf(std::ostream &out)	dimacs_cnft	virtual
write_prefix(std::ostream &out) const	qdimacs_cnft	protected
write_problem_line(std::ostream &out)	dimacs_cnft	protected
write_qdimacs_cnf(std::ostream &out)	qdimacs_cnft	virtual
~cnf_clause_listt()	cnf_clause_listt	inlinevirtual
~cnft()	cnft	inlinevirtual
~dimacs_cnft()	dimacs_cnft	inlinevirtual
~propt()	propt	inlinevirtual
~qbf_bdd_certificatet(void) override	qbf_bdd_certificatet