|
cprover
|
This is the complete list of members for aig_prop_solvert, including all inherited members.
| aig | aig_prop_solvert | |
| aig_prop_baset(aigt &_dest) | aig_prop_baset | inlineexplicit |
| aig_prop_constraintt(aig_plus_constraintst &_dest) | aig_prop_constraintt | inlineexplicit |
| aig_prop_solvert(propt &_solver) | aig_prop_solvert | inlineexplicit |
| cnf_handled_well() const override | aig_prop_baset | inlinevirtual |
| compute_phase(std::vector< bool > &n_pos, std::vector< bool > &n_neg) | aig_prop_solvert | protected |
| convert_aig() | aig_prop_solvert | protected |
| convert_node(unsigned n, const aigt::nodet &node, bool n_pos, bool n_neg, std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count) | aig_prop_solvert | protected |
| copy_assignment_from(const propt &prop) | propt | virtual |
| debug() | messaget | inline |
| dest | aig_prop_constraintt | |
| endl(mstreamt &m) | messaget | inlinestatic |
| eom(mstreamt &m) | messaget | inlinestatic |
| error() | messaget | inline |
| get_message_handler() | messaget | inline |
| get_mstream(unsigned message_level) | messaget | inline |
| has_is_in_conflict() const | propt | inlinevirtual |
| has_set_assumptions() const | propt | inlinevirtual |
| has_set_to() const override | aig_prop_constraintt | inlinevirtual |
| is_in_conflict(literalt l) const | propt | virtual |
| l_get(literalt a) const override | aig_prop_solvert | virtual |
| l_set_to(literalt a, bool value) override | aig_prop_constraintt | inlinevirtual |
| l_set_to_false(literalt a) | propt | inline |
| l_set_to_true(literalt a) | propt | inline |
| land(literalt a, literalt b) override | aig_prop_baset | virtual |
| land(const bvt &bv) override | aig_prop_baset | virtual |
| lcnf(const bvt &clause) override | aig_prop_constraintt | inlinevirtual |
| propt::lcnf(literalt l0, literalt l1) | propt | inline |
| propt::lcnf(literalt l0, literalt l1, literalt l2) | propt | inline |
| propt::lcnf(literalt l0, literalt l1, literalt l2, literalt l3) | propt | inline |
| lcnf_bv | propt | protected |
| lequal(literalt a, literalt b) override | aig_prop_baset | virtual |
| limplies(literalt a, literalt b) override | aig_prop_baset | virtual |
| lnand(literalt a, literalt b) override | aig_prop_baset | virtual |
| lnor(literalt a, literalt b) override | aig_prop_baset | virtual |
| lor(literalt a, literalt b) override | aig_prop_baset | virtual |
| lor(const bvt &bv) override | aig_prop_baset | virtual |
| lselect(literalt a, literalt b, literalt c) override | aig_prop_baset | virtual |
| lxor(literalt a, literalt b) override | aig_prop_baset | virtual |
| lxor(const bvt &bv) override | aig_prop_baset | 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 | |
| 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 | protected |
| new_variable() override | aig_prop_baset | inlinevirtual |
| new_variables(std::size_t width) | propt | |
| no_variables() const override | aig_prop_baset | inlinevirtual |
| progress() | messaget | inline |
| prop_solve() override | aig_prop_solvert | virtual |
| propt() | propt | inline |
| result() | messaget | inline |
| resultt enum name | propt | |
| set_assignment(literalt a, bool value) | propt | virtual |
| set_assumptions(const bvt &_assumptions) | propt | inlinevirtual |
| set_equal(literalt a, literalt b) override | aig_prop_baset | virtual |
| set_frozen(literalt a) | propt | inlinevirtual |
| set_message_handler(message_handlert &m) override | aig_prop_solvert | inlinevirtual |
| set_variable_name(literalt a, const std::string &name) | propt | inlinevirtual |
| solver | aig_prop_solvert | protected |
| solver_text() override | aig_prop_solvert | inlinevirtual |
| statistics() | messaget | inline |
| status() | messaget | inline |
| usage_count(std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count) | aig_prop_solvert | protected |
| warning() | messaget | inline |
| ~messaget() | messaget | virtual |
| ~prop_assignmentt() | prop_assignmentt | virtual |
| ~propt() | propt | inlinevirtual |