qdimacs_coret Class Referenceabstract
#include <qdimacs_core.h>
Inheritance diagram for qdimacs_coret: Collaboration diagram for qdimacs_coret:Public Types | |
| enum | modeltypet { M_TRUE , M_FALSE , M_DONTCARE , M_COMPLEX } |
| typedef std::pair< exprt, unsigned > | symbol_mapt |
| typedef std::map< unsigned, symbol_mapt > | variable_mapt |
| Public Types inherited from qdimacs_cnft | |
| typedef std::vector< quantifiert > | quantifierst |
| Public Types inherited from cnf_clause_listt | |
| typedef std::list< bvt > | clausest |
| Public Types inherited from propt | |
| enum class | resultt { P_SATISFIABLE , P_UNSATISFIABLE , P_ERROR } |
Public Member Functions | |
| qdimacs_coret (message_handlert &message_handler) | |
| virtual tvt | l_get (literalt a) const =0 |
| virtual bool | is_in_core (literalt l) const =0 |
| virtual modeltypet | m_get (literalt a) const =0 |
| virtual const exprt | f_get (literalt v)=0 |
| void | simplify_extractbits (exprt &expr) const |
| Public Member Functions inherited from qdimacs_cnft | |
| qdimacs_cnft (message_handlert &message_handler) | |
| virtual void | write_qdimacs_cnf (std::ostream &out) |
| std::string | solver_text () const override |
| virtual void | add_quantifier (const quantifiert &quantifier) |
| void | add_quantifier (const quantifiert::typet type, const literalt l) |
| void | add_existential_quantifier (const literalt l) |
| void | add_universal_quantifier (const literalt l) |
| bool | is_quantified (const literalt l) const |
| bool | find_quantifier (const literalt l, quantifiert &q) const |
| virtual void | set_quantifier (const quantifiert::typet type, const literalt l) |
| void | copy_to (qdimacs_cnft &cnf) const |
| bool | operator== (const qdimacs_cnft &other) const |
| size_t | hash () const |
| Public Member Functions inherited from dimacs_cnft | |
| dimacs_cnft (message_handlert &) | |
| virtual | ~dimacs_cnft () |
| virtual void | write_dimacs_cnf (std::ostream &out) const |
| std::string | solver_text () const override |
| void | set_assignment (literalt a, bool value) override |
| bool | is_in_conflict (literalt l) const override |
| Returns true if an assumption is in the final conflict. More... | |
| Public Member Functions inherited from cnf_clause_listt | |
| cnf_clause_listt (message_handlert &message_handler) | |
| virtual | ~cnf_clause_listt () |
| void | lcnf (const bvt &bv) override |
| tvt | l_get (literalt) const override |
| size_t | no_clauses () const override |
| clausest & | get_clauses () |
| void | copy_to (cnft &cnf) const |
| size_t | hash () const |
| 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 bool | has_assumptions () const |
| virtual void | set_variable_name (literalt, const irep_idt &) |
| resultt | prop_solve () |
| resultt | prop_solve (const bvt &assumptions) |
| virtual bool | has_is_in_conflict () const |
| virtual void | set_frozen (literalt) |
| virtual void | set_time_limit_seconds (uint32_t) |
| std::size_t | get_number_of_solver_calls () const |
Public Attributes | |
| variable_mapt | variable_map |
| Public Attributes inherited from qdimacs_cnft | |
| quantifierst | quantifiers |
Additional Inherited Members | |
| Static Public Member Functions inherited from dimacs_cnft | |
| static void | write_dimacs_clause (const bvt &, std::ostream &, bool break_lines) |
| Static Public Member Functions inherited from cnf_clause_listt | |
| static size_t | hash_clause (const bvt &bv) |
| Protected Member Functions inherited from qdimacs_cnft | |
| void | write_prefix (std::ostream &out) const |
| Protected Member Functions inherited from dimacs_cnft | |
| void | write_problem_line (std::ostream &out) const |
| void | write_clauses (std::ostream &out) const |
| Protected Member Functions inherited from cnf_clause_listt | |
| resultt | do_prop_solve (const bvt &) override |
| 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 dimacs_cnft | |
| bool | break_lines |
| Protected Attributes inherited from cnf_clause_listt | |
| clausest | clauses |
| 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 19 of file qdimacs_core.h.
Member Typedef Documentation
◆ symbol_mapt
| typedef std::pair<exprt, unsigned> qdimacs_coret::symbol_mapt |
Definition at line 33 of file qdimacs_core.h.
◆ variable_mapt
| typedef std::map<unsigned, symbol_mapt> qdimacs_coret::variable_mapt |
Definition at line 34 of file qdimacs_core.h.
Member Enumeration Documentation
◆ modeltypet
| Enumerator | |
|---|---|
| M_TRUE | |
| M_FALSE | |
| M_DONTCARE | |
| M_COMPLEX | |
Definition at line 30 of file qdimacs_core.h.
Constructor & Destructor Documentation
◆ qdimacs_coret()
|
inlineexplicit |
Definition at line 22 of file qdimacs_core.h.
Member Function Documentation
◆ f_get()
Implemented in qbf_qube_coret, qbf_squolem_coret, and qbf_bdd_certificatet.
◆ is_in_core()
|
pure virtual |
Implemented in qbf_squolem_coret, qbf_skizzo_coret, qbf_qube_coret, and qbf_bdd_coret.
◆ l_get()
Implements propt.
Implemented in qbf_squolem_coret, qbf_qube_coret, qbf_bdd_coret, and qbf_bdd_certificatet.
◆ m_get()
|
pure virtual |
Implemented in qbf_squolem_coret, qbf_skizzo_coret, qbf_qube_coret, and qbf_bdd_coret.
◆ simplify_extractbits()
| void qdimacs_coret::simplify_extractbits | ( | exprt & | expr | ) | const |
Definition at line 16 of file qdimacs_core.cpp.
Member Data Documentation
◆ variable_map
| variable_mapt qdimacs_coret::variable_map |
Definition at line 35 of file qdimacs_core.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/qbf/qdimacs_core.h
- /home/runner/work/cbmc/cbmc/src/solvers/qbf/qdimacs_core.cpp
