|
| satcheck_minisat1_coret () |
|
| ~satcheck_minisat1_coret () |
|
virtual const std::string | solver_text () override |
|
virtual resultt | prop_solve () override |
|
virtual bool | has_in_core () const |
|
virtual bool | is_in_core (literalt l) const |
|
| satcheck_minisat1_prooft () |
|
| ~satcheck_minisat1_prooft () |
|
simple_prooft & | get_resolution_proof () |
|
| satcheck_minisat1t () |
|
| satcheck_minisat1_baset () |
|
virtual | ~satcheck_minisat1_baset () |
|
virtual tvt | l_get (literalt a) const override |
|
virtual void | lcnf (const bvt &bv) final |
|
virtual void | set_assignment (literalt a, bool value) override |
|
virtual void | set_assumptions (const bvt &_assumptions) override |
|
virtual bool | has_set_assumptions () const override |
|
virtual bool | has_is_in_conflict () const override |
|
virtual bool | is_in_conflict (literalt l) const override |
| Returns true if an assumption is in the final conflict. More...
|
|
| cnf_solvert () |
|
virtual size_t | no_clauses () const override |
|
| cnft () |
|
virtual | ~cnft () |
|
virtual literalt | land (literalt a, literalt b) override |
|
virtual literalt | lor (literalt a, literalt b) override |
|
virtual literalt | land (const bvt &bv) override |
| Tseitin encoding of conjunction between multiple literals. More...
|
|
virtual literalt | lor (const bvt &bv) override |
| Tseitin encoding of disjunction between multiple literals. More...
|
|
virtual literalt | lxor (const bvt &bv) override |
| Tseitin encoding of XOR between multiple literals. More...
|
|
virtual literalt | lxor (literalt a, literalt b) override |
|
virtual literalt | lnand (literalt a, literalt b) override |
|
virtual literalt | lnor (literalt a, literalt b) override |
|
virtual literalt | lequal (literalt a, literalt b) override |
|
virtual literalt | limplies (literalt a, literalt b) override |
|
virtual literalt | lselect (literalt a, literalt b, literalt c) override |
|
virtual literalt | new_variable () override |
| Generate a new variable and return it as a literal. More...
|
|
virtual size_t | no_variables () const override |
|
virtual void | set_no_variables (size_t no) |
|
void | gate_and (literalt a, literalt b, literalt o) |
| Tseitin encoding of conjunction of two literals. More...
|
|
void | gate_or (literalt a, literalt b, literalt o) |
| Tseitin encoding of disjunction of two literals. More...
|
|
void | gate_xor (literalt a, literalt b, literalt o) |
| Tseitin encoding of XOR of two literals. More...
|
|
void | gate_nand (literalt a, literalt b, literalt o) |
| Tseitin encoding of NAND of two literals. More...
|
|
void | gate_nor (literalt a, literalt b, literalt o) |
| Tseitin encoding of NOR of two literals. More...
|
|
void | gate_equal (literalt a, literalt b, literalt o) |
| Tseitin encoding of equality between two literals. More...
|
|
void | gate_implies (literalt a, literalt b, literalt o) |
| Tseitin encoding of implication between two literals. More...
|
|
| propt () |
|
virtual | ~propt () |
|
virtual void | set_equal (literalt a, literalt b) |
| asserts a==b in the propositional formula More...
|
|
virtual void | l_set_to (literalt a, bool value) |
|
void | l_set_to_true (literalt a) |
|
void | l_set_to_false (literalt a) |
|
void | lcnf (literalt l0, literalt l1) |
|
void | lcnf (literalt l0, literalt l1, literalt l2) |
|
void | lcnf (literalt l0, literalt l1, literalt l2, literalt l3) |
|
virtual bool | has_set_to () const |
|
virtual bool | cnf_handled_well () const |
|
virtual void | set_variable_name (literalt, const irep_idt &) |
|
bvt | new_variables (std::size_t width) |
| generates a bitvector of given width with new variables More...
|
|
virtual void | set_frozen (literalt) |
|
virtual void | set_time_limit_seconds (uint32_t) |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
|
enum | resultt { resultt::P_SATISFIABLE,
resultt::P_UNSATISFIABLE,
resultt::P_ERROR
} |
|
enum | message_levelt {
M_ERROR =1,
M_WARNING =2,
M_RESULT =4,
M_STATUS =6,
M_STATISTICS =8,
M_PROGRESS =9,
M_DEBUG =10
} |
|
static bvt | eliminate_duplicates (const bvt &) |
| eliminate duplicates from given vector of literals More...
|
|
static unsigned | eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) |
| Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
|
|
static commandt | command (unsigned c) |
| Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
|
|
static eomt | eom |
|
static const commandt | reset |
| return to default formatting, as defined by the terminal More...
|
|
static const commandt | red |
| render text with red foreground color More...
|
|
static const commandt | green |
| render text with green foreground color More...
|
|
static const commandt | yellow |
| render text with yellow foreground color More...
|
|
static const commandt | blue |
| render text with blue foreground color More...
|
|
static const commandt | magenta |
| render text with magenta foreground color More...
|
|
static const commandt | cyan |
| render text with cyan foreground color More...
|
|
static const commandt | bright_red |
| render text with bright red foreground color More...
|
|
static const commandt | bright_green |
| render text with bright green foreground color More...
|
|
static const commandt | bright_yellow |
| render text with bright yellow foreground color More...
|
|
static const commandt | bright_blue |
| render text with bright blue foreground color More...
|
|
static const commandt | bright_magenta |
| render text with bright magenta foreground color More...
|
|
static const commandt | bright_cyan |
| render text with bright cyan foreground color More...
|
|
static const commandt | bold |
| render text with bold font More...
|
|
static const commandt | faint |
| render text with faint font More...
|
|
static const commandt | italic |
| render italic text More...
|
|
static const commandt | underline |
| render underlined text More...
|
|
enum | statust { statust::INIT,
statust::SAT,
statust::UNSAT,
statust::ERROR
} |
|
void | add_variables () |
|
bool | process_clause (const bvt &bv, bvt &dest) |
| filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses More...
|
|
static bool | is_all (const bvt &bv, literalt l) |
|
Definition at line 74 of file satcheck_minisat.h.