cprover
|
Decision procedure interface for various SMT 2.x solvers. More...
#include <smt2_dec.h>
Public Member Functions | |
smt2_dect (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver) | |
resultt | dec_solve () override |
Run the decision procedure to solve the problem. More... | |
std::string | decision_procedure_text () const override |
Return a textual description of the decision procedure. More... | |
![]() | |
smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out) | |
~smt2_convt () override=default | |
exprt | handle (const exprt &expr) override |
Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More... | |
void | set_to (const exprt &expr, bool value) override |
For a Boolean expression expr , add the constraint 'expr' if value is true , otherwise add 'not expr'. More... | |
exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . More... | |
void | push () override |
Unimplemented. More... | |
void | push (const std::vector< exprt > &_assumptions) override |
Currently, only implements a single stack element (no nested contexts) More... | |
void | pop () override |
Currently, only implements a single stack element (no nested contexts) More... | |
std::size_t | get_number_of_solver_calls () const override |
Return the number of incremental solver calls. More... | |
![]() | |
virtual | ~stack_decision_proceduret ()=default |
![]() | |
void | set_to_true (const exprt &expr) |
For a Boolean expression expr , add the constraint 'expr'. More... | |
void | set_to_false (const exprt &expr) |
For a Boolean expression expr , add the constraint 'not expr'. More... | |
resultt | operator() () |
Run the decision procedure to solve the problem. More... | |
virtual | ~decision_proceduret () |
Protected Member Functions | |
resultt | read_result (std::istream &in) |
![]() | |
void | write_header () |
void | write_footer (std::ostream &) |
bool | use_array_theory (const exprt &) |
void | flatten_array (const exprt &) |
produce a flat bit-vector for a given array of fixed size More... | |
void | convert_typecast (const typecast_exprt &expr) |
void | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
void | convert_struct (const struct_exprt &expr) |
void | convert_union (const union_exprt &expr) |
void | convert_constant (const constant_exprt &expr) |
void | convert_relation (const binary_relation_exprt &) |
void | convert_is_dynamic_object (const unary_exprt &) |
void | convert_plus (const plus_exprt &expr) |
void | convert_minus (const minus_exprt &expr) |
void | convert_div (const div_exprt &expr) |
void | convert_mult (const mult_exprt &expr) |
void | convert_rounding_mode_FPA (const exprt &expr) |
Converting a constant or symbolic rounding mode to SMT-LIB. More... | |
void | convert_floatbv_plus (const ieee_float_op_exprt &expr) |
void | convert_floatbv_minus (const ieee_float_op_exprt &expr) |
void | convert_floatbv_div (const ieee_float_op_exprt &expr) |
void | convert_floatbv_mult (const ieee_float_op_exprt &expr) |
void | convert_mod (const mod_exprt &expr) |
void | convert_index (const index_exprt &expr) |
void | convert_member (const member_exprt &expr) |
void | convert_with (const with_exprt &expr) |
void | convert_update (const exprt &expr) |
std::string | convert_identifier (const irep_idt &identifier) |
void | convert_expr (const exprt &) |
void | convert_type (const typet &) |
void | convert_literal (const literalt) |
literalt | convert (const exprt &expr) |
tvt | l_get (literalt l) const |
exprt | prepare_for_convert_expr (const exprt &expr) |
Perform steps necessary before an expression is passed to convert_expr. More... | |
exprt | lower_byte_operators (const exprt &expr) |
Lower byte_update and byte_extract operations within expr . More... | |
void | find_symbols (const exprt &expr) |
void | find_symbols (const typet &type) |
void | find_symbols_rec (const typet &type, std::set< irep_idt > &recstack) |
constant_exprt | parse_literal (const irept &, const typet &type) |
struct_exprt | parse_struct (const irept &s, const struct_typet &type) |
exprt | parse_union (const irept &s, const union_typet &type) |
exprt | parse_array (const irept &s, const array_typet &type) |
exprt | parse_rec (const irept &s, const typet &type) |
void | convert_floatbv (const exprt &expr) |
std::string | type2id (const typet &) const |
std::string | floatbv_suffix (const exprt &) const |
const smt2_symbolt & | to_smt2_symbol (const exprt &expr) |
void | flatten2bv (const exprt &) |
void | unflatten (wheret, const typet &, unsigned nesting=0) |
void | convert_address_of_rec (const exprt &expr, const pointer_typet &result_type) |
void | define_object_size (const irep_idt &id, const exprt &expr) |
smt2_convt (const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out) | |
~smt2_convt () override=default | |
exprt | handle (const exprt &expr) override |
Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More... | |
void | set_to (const exprt &expr, bool value) override |
For a Boolean expression expr , add the constraint 'expr' if value is true , otherwise add 'not expr'. More... | |
exprt | get (const exprt &expr) const override |
Return expr with variables replaced by values from satisfying assignment if available. More... | |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . More... | |
void | push () override |
Unimplemented. More... | |
void | push (const std::vector< exprt > &_assumptions) override |
Currently, only implements a single stack element (no nested contexts) More... | |
void | pop () override |
Currently, only implements a single stack element (no nested contexts) More... | |
std::size_t | get_number_of_solver_calls () const override |
Return the number of incremental solver calls. More... | |
![]() | |
virtual | ~stack_decision_proceduret ()=default |
void | set_to_true (const exprt &expr) |
For a Boolean expression expr , add the constraint 'expr'. More... | |
void | set_to_false (const exprt &expr) |
For a Boolean expression expr , add the constraint 'not expr'. More... | |
resultt | operator() () |
Run the decision procedure to solve the problem. More... | |
virtual | ~decision_proceduret () |
Decision procedure interface for various SMT 2.x solvers.
Definition at line 27 of file smt2_dec.h.
|
inline |
Definition at line 32 of file smt2_dec.h.
|
overridevirtual |
Run the decision procedure to solve the problem.
Reimplemented from smt2_convt.
Definition at line 37 of file smt2_dec.cpp.
|
overridevirtual |
Return a textual description of the decision procedure.
Reimplemented from smt2_convt.
Definition at line 21 of file smt2_dec.cpp.
|
protected |
Definition at line 133 of file smt2_dec.cpp.