cprover
|
#include <smt2_conv.h>
Classes | |
struct | identifiert |
class | smt2_symbolt |
Public Types | |
enum class | solvert { GENERIC , BOOLECTOR , CPROVER_SMT2 , CVC3 , CVC4 , MATHSAT , YICES , Z3 } |
![]() | |
enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
Result of running the decision procedure. More... | |
Public Member Functions | |
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... | |
std::string | decision_procedure_text () const override |
Return a textual description of the decision procedure. 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 () |
Public Attributes | |
bool | use_FPA_theory |
bool | use_datatypes |
bool | use_array_of_bool |
bool | emit_set_logic |
Protected Types | |
enum class | wheret { BEGIN , END } |
typedef std::unordered_map< irep_idt, identifiert > | identifier_mapt |
typedef std::map< typet, std::string > | datatype_mapt |
typedef std::map< exprt, irep_idt > | defined_expressionst |
typedef std::set< std::string > | smt2_identifierst |
Protected Member Functions | |
resultt | dec_solve () override |
Run the decision procedure to solve the problem. More... | |
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) |
Protected Attributes | |
const namespacet & | ns |
std::ostream & | out |
std::string | benchmark |
std::string | notes |
std::string | logic |
solvert | solver |
std::vector< exprt > | assumptions |
boolbv_widtht | boolbv_width |
std::size_t | number_of_solver_calls = 0 |
letifyt | letify |
std::set< irep_idt > | bvfp_set |
pointer_logict | pointer_logic |
identifier_mapt | identifier_map |
datatype_mapt | datatype_map |
defined_expressionst | defined_expressions |
defined_expressionst | object_sizes |
smt2_identifierst | smt2_identifiers |
std::size_t | no_boolean_variables |
std::vector< bool > | boolean_assignment |
Definition at line 35 of file smt2_conv.h.
|
protected |
Definition at line 212 of file smt2_conv.h.
|
protected |
Definition at line 221 of file smt2_conv.h.
|
protected |
Definition at line 206 of file smt2_conv.h.
|
protected |
Definition at line 226 of file smt2_conv.h.
|
strong |
Enumerator | |
---|---|
GENERIC | |
BOOLECTOR | |
CPROVER_SMT2 | |
CVC3 | |
CVC4 | |
MATHSAT | |
YICES | |
Z3 |
Definition at line 38 of file smt2_conv.h.
|
strongprotected |
Enumerator | |
---|---|
BEGIN | |
END |
Definition at line 181 of file smt2_conv.h.
smt2_convt::smt2_convt | ( | const namespacet & | _ns, |
const std::string & | _benchmark, | ||
const std::string & | _notes, | ||
const std::string & | _logic, | ||
solvert | _solver, | ||
std::ostream & | _out | ||
) |
Definition at line 48 of file smt2_conv.cpp.
|
overridedefault |
Definition at line 700 of file smt2_conv.cpp.
|
protected |
Definition at line 608 of file smt2_conv.cpp.
|
protected |
Definition at line 2804 of file smt2_conv.cpp.
|
protected |
Definition at line 3409 of file smt2_conv.cpp.
|
protected |
Definition at line 887 of file smt2_conv.cpp.
|
protected |
Definition at line 853 of file smt2_conv.cpp.
|
protected |
Definition at line 3453 of file smt2_conv.cpp.
|
protected |
Definition at line 3389 of file smt2_conv.cpp.
|
protected |
Definition at line 3548 of file smt2_conv.cpp.
|
protected |
Definition at line 3253 of file smt2_conv.cpp.
|
protected |
Definition at line 2530 of file smt2_conv.cpp.
|
protected |
Definition at line 778 of file smt2_conv.cpp.
|
protected |
Definition at line 3822 of file smt2_conv.cpp.
|
protected |
Definition at line 2954 of file smt2_conv.cpp.
|
protected |
Definition at line 741 of file smt2_conv.cpp.
|
protected |
Definition at line 3920 of file smt2_conv.cpp.
|
protected |
Definition at line 3292 of file smt2_conv.cpp.
|
protected |
Definition at line 2935 of file smt2_conv.cpp.
|
protected |
Definition at line 3473 of file smt2_conv.cpp.
|
protected |
Definition at line 3074 of file smt2_conv.cpp.
|
protected |
Definition at line 2991 of file smt2_conv.cpp.
|
protected |
Converting a constant or symbolic rounding mode to SMT-LIB.
Only called when use_FPA_theory is enabled
Definition at line 3196 of file smt2_conv.cpp.
|
protected |
Definition at line 2676 of file smt2_conv.cpp.
|
protected |
Definition at line 4544 of file smt2_conv.cpp.
|
protected |
Definition at line 1997 of file smt2_conv.cpp.
|
protected |
Definition at line 2771 of file smt2_conv.cpp.
|
protected |
Definition at line 3815 of file smt2_conv.cpp.
|
protected |
Definition at line 3568 of file smt2_conv.cpp.
|
overrideprotectedvirtual |
Run the decision procedure to solve the problem.
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 244 of file smt2_conv.cpp.
|
overridevirtual |
Return a textual description of the decision procedure.
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 107 of file smt2_conv.cpp.
Definition at line 206 of file smt2_conv.cpp.
|
protected |
Definition at line 4313 of file smt2_conv.cpp.
|
protected |
Definition at line 4679 of file smt2_conv.cpp.
Definition at line 4685 of file smt2_conv.cpp.
|
protected |
Definition at line 3981 of file smt2_conv.cpp.
|
protected |
produce a flat bit-vector for a given array of fixed size
Definition at line 2740 of file smt2_conv.cpp.
|
protected |
Definition at line 846 of file smt2_conv.cpp.
Return expr
with variables replaced by values from satisfying assignment if available.
Return nil
if not available
Implements decision_proceduret.
Definition at line 251 of file smt2_conv.cpp.
|
overridevirtual |
Return the number of incremental solver calls.
Implements decision_proceduret.
Definition at line 4889 of file smt2_conv.cpp.
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.
The returned expression may be the expression itself or a more compact but solver-specific representation.
Implements decision_proceduret.
Definition at line 732 of file smt2_conv.cpp.
Definition at line 122 of file smt2_conv.cpp.
Lower byte_update and byte_extract operations within expr
.
Return an equivalent expression that doesn't use byte operators. Note this replaces operators post-order (compare lower_byte_operators, which uses a pre-order walk, replacing in child expressions before the parent). Pre-order replacement currently fails regression tests: see https://github.com/diffblue/cbmc/issues/4380
Definition at line 4266 of file smt2_conv.cpp.
|
protected |
Definition at line 439 of file smt2_conv.cpp.
|
protected |
Definition at line 301 of file smt2_conv.cpp.
Definition at line 544 of file smt2_conv.cpp.
|
protected |
Definition at line 485 of file smt2_conv.cpp.
|
protected |
Definition at line 469 of file smt2_conv.cpp.
|
overridevirtual |
Currently, only implements a single stack element (no nested contexts)
Implements stack_decision_proceduret.
Definition at line 773 of file smt2_conv.cpp.
Perform steps necessary before an expression is passed to convert_expr.
expr | expression to prepare |
Definition at line 4298 of file smt2_conv.cpp.
|
overridevirtual |
Print satisfying assignment to out
.
Implements decision_proceduret.
Definition at line 112 of file smt2_conv.cpp.
|
overridevirtual |
|
overridevirtual |
Currently, only implements a single stack element (no nested contexts)
Implements stack_decision_proceduret.
Definition at line 766 of file smt2_conv.cpp.
|
overridevirtual |
For a Boolean expression expr
, add the constraint 'expr' if value
is true
, otherwise add 'not expr'.
Implements decision_proceduret.
Definition at line 4174 of file smt2_conv.cpp.
|
inlineprotected |
Definition at line 171 of file smt2_conv.h.
|
protected |
Definition at line 809 of file smt2_conv.cpp.
Definition at line 4070 of file smt2_conv.cpp.
|
protected |
Definition at line 4523 of file smt2_conv.cpp.
|
protected |
Definition at line 165 of file smt2_conv.cpp.
|
protected |
Definition at line 135 of file smt2_conv.cpp.
|
protected |
Definition at line 88 of file smt2_conv.h.
|
protected |
Definition at line 85 of file smt2_conv.h.
|
protected |
Definition at line 89 of file smt2_conv.h.
|
protected |
Definition at line 231 of file smt2_conv.h.
|
protected |
Definition at line 156 of file smt2_conv.h.
|
protected |
Definition at line 213 of file smt2_conv.h.
|
protected |
Definition at line 222 of file smt2_conv.h.
bool smt2_convt::emit_set_logic |
Definition at line 63 of file smt2_conv.h.
|
protected |
Definition at line 208 of file smt2_conv.h.
|
protected |
Definition at line 143 of file smt2_conv.h.
|
protected |
Definition at line 85 of file smt2_conv.h.
|
protected |
Definition at line 230 of file smt2_conv.h.
|
protected |
Definition at line 85 of file smt2_conv.h.
|
protected |
Definition at line 83 of file smt2_conv.h.
|
protected |
Definition at line 91 of file smt2_conv.h.
|
protected |
Definition at line 224 of file smt2_conv.h.
|
protected |
Definition at line 84 of file smt2_conv.h.
|
protected |
Definition at line 186 of file smt2_conv.h.
|
protected |
Definition at line 227 of file smt2_conv.h.
|
protected |
Definition at line 86 of file smt2_conv.h.
bool smt2_convt::use_array_of_bool |
Definition at line 62 of file smt2_conv.h.
bool smt2_convt::use_datatypes |
Definition at line 61 of file smt2_conv.h.
bool smt2_convt::use_FPA_theory |
Definition at line 60 of file smt2_conv.h.