cprover
|
#include <cvc_dec.h>
Public Member Functions | |
cvc_dect (const namespacet &_ns) | |
virtual resultt | dec_solve () |
![]() | |
cvc_convt (const namespacet &_ns, std::ostream &_out) | |
virtual | ~cvc_convt () |
virtual void | set_to (const exprt &expr, bool value) |
virtual literalt | convert (const exprt &expr) |
virtual tvt | l_get (literalt) const |
virtual void | print_assignment (std::ostream &out) const |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
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 |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual exprt | get (const exprt &expr) 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 | |
resultt | read_cvcl_result () |
void | read_assert (std::istream &in, std::string &line) |
![]() | |
cvc_temp_filet () | |
~cvc_temp_filet () | |
![]() | |
virtual void | convert_expr (const exprt &expr) |
virtual void | convert_type (const typet &type) |
virtual void | convert_address_of_rec (const exprt &expr) |
cvc_convt (const namespacet &_ns, std::ostream &_out) | |
virtual | ~cvc_convt () |
virtual void | set_to (const exprt &expr, bool value) |
virtual literalt | convert (const exprt &expr) |
virtual tvt | l_get (literalt) const |
virtual void | print_assignment (std::ostream &out) const |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
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 |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual exprt | get (const exprt &expr) 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 |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
![]() | |
typedef std::unordered_map< irep_idt, identifiert, irep_id_hash > | identifier_mapt |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
![]() | |
std::ofstream | temp_out |
std::string | temp_out_filename |
std::string | temp_result_filename |
![]() | |
std::ostream & | out |
pointer_logict | pointer_logic |
unsigned | no_boolean_variables |
identifier_mapt | identifier_map |
std::vector< bool > | boolean_assignment |
![]() | |
const namespacet & | ns |
|
inlineexplicit |
|
virtual |
Implements decision_proceduret.
Definition at line 52 of file cvc_dec.cpp.
References cvc_temp_filet::temp_out, cvc_temp_filet::temp_out_filename, and cvc_temp_filet::temp_result_filename.
|
protected |
Definition at line 73 of file cvc_dec.cpp.
References has_prefix(), pos(), size_type(), and unsafe_string2unsigned().
|
protected |
Definition at line 132 of file cvc_dec.cpp.
References has_prefix(), and cvc_temp_filet::temp_result_filename.