dplib_dect Class Reference
#include <dplib_dec.h>
Inheritance diagram for dplib_dect:
Collaboration diagram for dplib_dect:
Public Member Functions | |
| dplib_dect (const namespacet &_ns) | |
| virtual resultt | dec_solve () |
 Public Member Functions inherited from dplib_convt | |
| dplib_convt (const namespacet &_ns, std::ostream &_out) | |
| virtual | ~dplib_convt () |
| Public Member Functions inherited from prop_convt | |
| prop_convt (const namespacet &_ns) | |
| virtual | ~prop_convt () |
| virtual literalt | convert (const exprt &expr)=0 |
| literalt | operator() (const exprt &expr) |
| virtual tvt | l_get (literalt a) const =0 |
| virtual void | set_frozen (literalt a) |
| virtual void | set_frozen (const bvt &) |
| virtual void | set_assumptions (const bvt &_assumptions) |
| virtual bool | has_set_assumptions () const |
| virtual void | set_all_frozen () |
| virtual bool | is_in_conflict (literalt l) const |
| determine whether a variable is in the final conflict More... | |
| virtual bool | has_is_in_conflict () const |
| Public Member Functions inherited from decision_proceduret | |
| decision_proceduret (const namespacet &_ns) | |
| virtual exprt | get (const exprt &expr) const =0 |
| virtual void | print_assignment (std::ostream &out) const =0 |
| void | set_to_true (const exprt &expr) |
| void | set_to_false (const exprt &expr) |
| resultt | operator() () |
| virtual bool | in_core (const exprt &expr) |
| virtual std::string | decision_procedure_text () const =0 |
| Public Member Functions inherited from messaget | |
Protected Member Functions | |
| resultt | read_dplib_result () |
| void | read_assert (std::istream &in, std::string &line) |
| Protected Member Functions inherited from dplib_temp_filet | |
| dplib_temp_filet () | |
| ~dplib_temp_filet () | |
| Protected Member Functions inherited from dplib_convt | |
| virtual literalt | convert_rest (const exprt &expr) |
| virtual void | convert_dplib_expr (const exprt &expr) |
| virtual void | convert_dplib_type (const typet &type) |
| virtual void | set_to (const exprt &expr, bool value) |
| virtual void | convert_address_of_rec (const exprt &expr) |
| dplib_convt (const namespacet &_ns, std::ostream &_out) | |
| virtual | ~dplib_convt () |
| Protected Member Functions inherited from prop_convt | |
| prop_convt (const namespacet &_ns) | |
| virtual | ~prop_convt () |
| virtual literalt | convert (const exprt &expr)=0 |
| literalt | operator() (const exprt &expr) |
| virtual tvt | l_get (literalt a) const =0 |
| virtual void | set_frozen (literalt a) |
| virtual void | set_frozen (const bvt &) |
| virtual void | set_assumptions (const bvt &_assumptions) |
| virtual bool | has_set_assumptions () const |
| virtual void | set_all_frozen () |
| virtual bool | is_in_conflict (literalt l) const |
| determine whether a variable is in the final conflict More... | |
| virtual bool | has_is_in_conflict () const |
| Protected Member Functions inherited from decision_proceduret | |
| decision_proceduret (const namespacet &_ns) | |
| virtual exprt | get (const exprt &expr) const =0 |
| virtual void | print_assignment (std::ostream &out) const =0 |
| void | set_to_true (const exprt &expr) |
| void | set_to_false (const exprt &expr) |
| resultt | operator() () |
| virtual bool | in_core (const exprt &expr) |
| virtual std::string | decision_procedure_text () const =0 |
| Protected Member Functions inherited from messaget | |
Additional Inherited Members | |
| Public Types inherited from decision_proceduret | |
| enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
| Public Types inherited from messaget | |
| Static Public Member Functions inherited from messaget | |
| Protected Types inherited from decision_proceduret | |
| enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
| Protected Types inherited from messaget | |
| Static Protected Member Functions inherited from messaget | |
| Protected Attributes inherited from dplib_temp_filet | |
| std::ofstream | temp_out |
| std::string | temp_out_filename |
| std::string | temp_result_filename |
| Protected Attributes inherited from dplib_convt | |
| std::ostream & | out |
| pointer_logict | pointer_logic |
| Protected Attributes inherited from decision_proceduret | |
| const namespacet & | ns |
| Protected Attributes inherited from messaget | |
Detailed Description
Definition at line 28 of file dplib_dec.h.
Constructor & Destructor Documentation
◆ dplib_dect()
|
inlineexplicit |
Definition at line 31 of file dplib_dec.h.
Member Function Documentation
◆ dec_solve()
|
virtual |
Implements decision_proceduret.
Definition at line 51 of file dplib_dec.cpp.
References read_dplib_result(), messaget::status(), dplib_temp_filet::temp_out, dplib_temp_filet::temp_out_filename, and dplib_temp_filet::temp_result_filename.
◆ read_assert()
|
protected |
Definition at line 74 of file dplib_dec.cpp.
References has_prefix(), pos(), and size_type().
Referenced by read_dplib_result().
◆ read_dplib_result()
|
protected |
Definition at line 132 of file dplib_dec.cpp.
References messaget::error(), has_prefix(), read_assert(), and dplib_temp_filet::temp_result_filename.
Referenced by dec_solve().
The documentation for this class was generated from the following files:
- solvers/dplib/dplib_dec.h
- solvers/dplib/dplib_dec.cpp
