satcheck_glucose_simplifiert Class Reference
#include <satcheck_glucose.h>
Inheritance diagram for satcheck_glucose_simplifiert: Collaboration diagram for satcheck_glucose_simplifiert:Public Member Functions | |
| std::string | solver_text () const override |
| void | set_frozen (literalt a) override |
| bool | is_eliminated (literalt a) const |
| Public Member Functions inherited from satcheck_glucose_baset< Glucose::SimpSolver > | |
| satcheck_glucose_baset (message_handlert &message_handler) | |
| ~satcheck_glucose_baset () override | |
A default destructor defined in the .cpp is used to ensure the unique_ptr to the solver is correctly destroyed. More... | |
| tvt | l_get (literalt a) const override |
| void | lcnf (const bvt &bv) override |
| void | set_assignment (literalt a, bool value) override |
| void | set_polarity (literalt a, bool value) |
| bool | is_in_conflict (literalt a) const override |
| Returns true if an assumption is in the final conflict. More... | |
| bool | has_assumptions () const override |
| bool | has_is_in_conflict () const override |
| Public Member Functions inherited from cnf_solvert | |
| cnf_solvert (message_handlert &message_handler) | |
| virtual size_t | no_clauses () const override |
| Public Member Functions inherited from cnft | |
| cnft (message_handlert &message_handler) | |
| 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... | |
| bvt | new_variables (std::size_t width) override |
| Generate a vector of new variables. More... | |
| virtual size_t | no_variables () const override |
| virtual void | set_no_variables (size_t no) |
| Public Member Functions inherited from propt | |
| propt (message_handlert &message_handler) | |
| 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 &) |
| resultt | prop_solve () |
| resultt | prop_solve (const bvt &assumptions) |
| virtual void | set_time_limit_seconds (uint32_t) |
| std::size_t | get_number_of_solver_calls () const |
Additional Inherited Members | |
| Public Types inherited from propt | |
| enum class | resultt { P_SATISFIABLE , P_UNSATISFIABLE , P_ERROR } |
| Public Attributes inherited from hardness_collectort | |
| std::unique_ptr< clause_hardness_collectort > | solver_hardness |
| Protected Types inherited from cnf_solvert | |
| enum class | statust { INIT , SAT , UNSAT , ERROR } |
| Protected Member Functions inherited from satcheck_glucose_baset< Glucose::SimpSolver > | |
| resultt | do_prop_solve (const bvt &assumptions) override |
| void | add_variables () |
| Protected Member Functions inherited from cnft | |
| 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... | |
| bool | process_clause (const bvt &bv, bvt &dest) const |
| filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses More... | |
| Static Protected Member Functions inherited from cnft | |
| static bvt | eliminate_duplicates (const bvt &) |
| eliminate duplicates from given vector of literals More... | |
| static bool | is_all (const bvt &bv, literalt l) |
| Protected Attributes inherited from satcheck_glucose_baset< Glucose::SimpSolver > | |
| std::unique_ptr< Glucose::SimpSolver > | solver |
| Protected Attributes inherited from cnf_solvert | |
| statust | status |
| size_t | clause_counter |
| Protected Attributes inherited from cnft | |
| size_t | _no_variables |
| Protected Attributes inherited from propt | |
| bvt | lcnf_bv |
| messaget | log |
| std::size_t | number_of_solver_calls = 0 |
Detailed Description
Definition at line 73 of file satcheck_glucose.h.
Member Function Documentation
◆ is_eliminated()
| bool satcheck_glucose_simplifiert::is_eliminated | ( | literalt | a | ) | const |
Definition at line 296 of file satcheck_glucose.cpp.
◆ set_frozen()
|
overridevirtual |
Reimplemented from propt.
Definition at line 278 of file satcheck_glucose.cpp.
◆ solver_text()
|
overridevirtual |
Implements propt.
Definition at line 96 of file satcheck_glucose.cpp.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.h
- /home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp
