cprover
|
This is the complete list of members for qbf_squolem_coret, including all inherited members.
_no_variables | cnft | protected |
add_existential_quantifier(const literalt l) | qdimacs_cnft | inline |
add_quantifier(const quantifiert &quantifier) | qbf_squolem_coret | virtual |
qdimacs_coret::add_quantifier(const quantifiert::typet type, const literalt l) | qdimacs_cnft | inline |
add_universal_quantifier(const literalt l) | qdimacs_cnft | inline |
break_lines | dimacs_cnft | protected |
clauses | cnf_clause_listt | protected |
clausest typedef | cnf_clause_listt | |
cnf_clause_listt() | cnf_clause_listt | inline |
cnf_handled_well() const | propt | inlinevirtual |
cnft() | cnft | inline |
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const | messaget | |
copy_assignment_from(const propt &prop) | propt | virtual |
copy_to(qdimacs_cnft &cnf) const | qdimacs_cnft | |
dimacs_cnft::copy_to(cnft &cnf) const | cnf_clause_listt | inline |
debug() const | messaget | inline |
dimacs_cnft() | dimacs_cnft | |
early_decision | qbf_squolem_coret | protected |
eliminate_duplicates(const bvt &) | cnft | static |
endl(mstreamt &m) | messaget | inlinestatic |
eom(mstreamt &m) | messaget | inlinestatic |
error() const | messaget | inline |
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) | messaget | static |
f_get(literalt l) | qbf_squolem_coret | virtual |
f_get_cnf(WitnessStack *wsp) | qbf_squolem_coret | private |
f_get_dnf(WitnessStack *wsp) | qbf_squolem_coret | private |
find_quantifier(const literalt l, quantifiert &q) const | qdimacs_cnft | |
function_cache | qbf_squolem_coret | private |
function_cachet typedef | qbf_squolem_coret | private |
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_clauses() | cnf_clause_listt | inline |
get_message_handler() | messaget | inline |
get_mstream(unsigned message_level) const | messaget | inline |
has_is_in_conflict() const | propt | inlinevirtual |
has_set_assumptions() 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 | propt | virtual |
is_in_core(literalt l) const | qbf_squolem_coret | virtual |
is_quantified(const literalt l) const | qdimacs_cnft | |
l_get(literalt a) const | qbf_squolem_coret | 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) | qbf_squolem_coret | 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 |
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_DEBUG enum value | messaget | |
M_DONTCARE enum value | qdimacs_coret | |
M_ERROR enum value | messaget | |
M_FALSE enum value | qdimacs_coret | |
m_get(literalt a) const | qbf_squolem_coret | virtual |
M_PROGRESS enum value | messaget | |
M_RESULT enum value | messaget | |
M_STATISTICS enum value | messaget | |
M_STATUS enum value | messaget | |
M_TRUE enum value | qdimacs_coret | |
M_WARNING enum value | messaget | |
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 |
modeltypet enum name | qdimacs_coret | |
mstream | messaget | mutableprotected |
new_variable() override | cnft | virtual |
new_variables(std::size_t width) | propt | |
no_clauses() const | qbf_squolem_coret | inlinevirtual |
no_variables() const override | cnft | inlinevirtual |
operator=(const messaget &other) | messaget | inline |
operator==(const qdimacs_cnft &other) const | qdimacs_cnft | |
process_clause(const bvt &bv, bvt &dest) | cnft | protected |
progress() const | messaget | inline |
prop_solve() | qbf_squolem_coret | virtual |
propt() | propt | inline |
qbf_squolem_coret() | qbf_squolem_coret | |
qdimacs_cnft() | qdimacs_cnft | inline |
quantifiers | qdimacs_cnft | |
quantifierst typedef | qdimacs_cnft | |
reset(void) | qbf_squolem_coret | |
result() const | messaget | inline |
resultt enum name | propt | |
set_assignment(literalt a, bool value) | propt | virtual |
set_assumptions(const bvt &_assumptions) | propt | inlinevirtual |
set_debug_filename(const std::string &str) | qbf_squolem_coret | |
set_equal(literalt a, literalt b) | propt | virtual |
set_frozen(literalt a) | propt | inlinevirtual |
set_message_handler(message_handlert &_message_handler) | messaget | inlinevirtual |
set_no_variables(size_t no) | qbf_squolem_coret | virtual |
set_quantifier(const quantifiert::typet type, const literalt l) | qbf_squolem_coret | virtual |
qdimacs_coret::set_quantifier(const quantifiert::typet type, const literalt l) | qdimacs_cnft | virtual |
set_time_limit_seconds(uint32_t lim) | propt | inlinevirtual |
set_variable_name(literalt a, const irep_idt &name) | propt | inlinevirtual |
setup(void) | qbf_squolem_coret | private |
simplify_extractbits(exprt &expr) const | qdimacs_coret | |
solver_text() | qbf_squolem_coret | virtual |
squolem | qbf_squolem_coret | protected |
statistics() const | messaget | inline |
status() const | messaget | inline |
symbol_mapt typedef | qdimacs_coret | |
variable_map | qdimacs_coret | |
variable_mapt typedef | qdimacs_coret | |
warning() const | messaget | inline |
write_clauses(std::ostream &out) | dimacs_cnft | protected |
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) | qbf_squolem_coret | virtual |
~cnf_clause_listt() | cnf_clause_listt | inlinevirtual |
~cnft() | cnft | inlinevirtual |
~dimacs_cnft() | dimacs_cnft | inlinevirtual |
~messaget() | messaget | virtual |
~propt() | propt | inlinevirtual |
~qbf_squolem_coret() | qbf_squolem_coret | virtual |
~qdimacs_cnft() | qdimacs_cnft | inlinevirtual |