cprover
|
#include <smt2_conv.h>
Classes | |
struct | identifiert |
class | smt2_symbolt |
Public Types | |
enum | solvert { solvert::GENERIC, solvert::BOOLECTOR, solvert::CPROVER_SMT2, solvert::CVC3, solvert::CVC4, solvert::MATHSAT, solvert::YICES, solvert::Z3 } |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::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 | wheret { wheret::BEGIN, wheret::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 34 of file smt2_conv.h.
|
protected |
Definition at line 211 of file smt2_conv.h.
|
protected |
Definition at line 220 of file smt2_conv.h.
|
protected |
Definition at line 205 of file smt2_conv.h.
|
protected |
Definition at line 225 of file smt2_conv.h.
|
strong |
Enumerator | |
---|---|
GENERIC | |
BOOLECTOR | |
CPROVER_SMT2 | |
CVC3 | |
CVC4 | |
MATHSAT | |
YICES | |
Z3 |
Definition at line 37 of file smt2_conv.h.
|
strongprotected |
Enumerator | |
---|---|
BEGIN | |
END |
Definition at line 180 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 46 of file smt2_conv.cpp.
|
overridedefault |
Definition at line 698 of file smt2_conv.cpp.
|
protected |
Definition at line 606 of file smt2_conv.cpp.
|
protected |
Definition at line 2762 of file smt2_conv.cpp.
|
protected |
Definition at line 3367 of file smt2_conv.cpp.
|
protected |
Definition at line 885 of file smt2_conv.cpp.
|
protected |
Definition at line 851 of file smt2_conv.cpp.
|
protected |
Definition at line 3411 of file smt2_conv.cpp.
|
protected |
Definition at line 3347 of file smt2_conv.cpp.
|
protected |
Definition at line 3506 of file smt2_conv.cpp.
|
protected |
Definition at line 3211 of file smt2_conv.cpp.
|
protected |
Definition at line 2488 of file smt2_conv.cpp.
|
protected |
Definition at line 776 of file smt2_conv.cpp.
|
protected |
Definition at line 3780 of file smt2_conv.cpp.
|
protected |
Definition at line 2912 of file smt2_conv.cpp.
|
protected |
Definition at line 739 of file smt2_conv.cpp.
|
protected |
Definition at line 3878 of file smt2_conv.cpp.
|
protected |
Definition at line 3250 of file smt2_conv.cpp.
|
protected |
Definition at line 2893 of file smt2_conv.cpp.
|
protected |
Definition at line 3431 of file smt2_conv.cpp.
|
protected |
Definition at line 3032 of file smt2_conv.cpp.
|
protected |
Definition at line 2949 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 3154 of file smt2_conv.cpp.
|
protected |
Definition at line 2634 of file smt2_conv.cpp.
|
protected |
Definition at line 4502 of file smt2_conv.cpp.
|
protected |
Definition at line 1955 of file smt2_conv.cpp.
|
protected |
Definition at line 2729 of file smt2_conv.cpp.
|
protected |
Definition at line 3773 of file smt2_conv.cpp.
|
protected |
Definition at line 3526 of file smt2_conv.cpp.
|
overrideprotectedvirtual |
Run the decision procedure to solve the problem.
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 242 of file smt2_conv.cpp.
|
overridevirtual |
Return a textual description of the decision procedure.
Implements decision_proceduret.
Reimplemented in smt2_dect.
Definition at line 105 of file smt2_conv.cpp.
Definition at line 204 of file smt2_conv.cpp.
|
protected |
Definition at line 4271 of file smt2_conv.cpp.
|
protected |
Definition at line 4637 of file smt2_conv.cpp.
Definition at line 4643 of file smt2_conv.cpp.
|
protected |
Definition at line 3939 of file smt2_conv.cpp.
|
protected |
produce a flat bit-vector for a given array of fixed size
Definition at line 2698 of file smt2_conv.cpp.
|
protected |
Definition at line 844 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 249 of file smt2_conv.cpp.
|
overridevirtual |
Return the number of incremental solver calls.
Implements decision_proceduret.
Definition at line 4847 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 730 of file smt2_conv.cpp.
Definition at line 120 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 4224 of file smt2_conv.cpp.
|
protected |
Definition at line 437 of file smt2_conv.cpp.
|
protected |
Definition at line 299 of file smt2_conv.cpp.
Definition at line 542 of file smt2_conv.cpp.
|
protected |
Definition at line 483 of file smt2_conv.cpp.
|
protected |
Definition at line 467 of file smt2_conv.cpp.
|
overridevirtual |
Currently, only implements a single stack element (no nested contexts)
Implements stack_decision_proceduret.
Definition at line 771 of file smt2_conv.cpp.
Perform steps necessary before an expression is passed to convert_expr.
expr | expression to prepare |
Definition at line 4256 of file smt2_conv.cpp.
|
overridevirtual |
Print satisfying assignment to out
.
Implements decision_proceduret.
Definition at line 110 of file smt2_conv.cpp.
|
overridevirtual |
|
overridevirtual |
Currently, only implements a single stack element (no nested contexts)
Implements stack_decision_proceduret.
Definition at line 764 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 4132 of file smt2_conv.cpp.
|
inlineprotected |
Definition at line 170 of file smt2_conv.h.
|
protected |
Definition at line 807 of file smt2_conv.cpp.
Definition at line 4028 of file smt2_conv.cpp.
|
protected |
Definition at line 4481 of file smt2_conv.cpp.
|
protected |
Definition at line 163 of file smt2_conv.cpp.
|
protected |
Definition at line 133 of file smt2_conv.cpp.
|
protected |
Definition at line 87 of file smt2_conv.h.
|
protected |
Definition at line 84 of file smt2_conv.h.
|
protected |
Definition at line 88 of file smt2_conv.h.
|
protected |
Definition at line 230 of file smt2_conv.h.
|
protected |
Definition at line 155 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.
bool smt2_convt::emit_set_logic |
Definition at line 62 of file smt2_conv.h.
|
protected |
Definition at line 207 of file smt2_conv.h.
|
protected |
Definition at line 142 of file smt2_conv.h.
|
protected |
Definition at line 84 of file smt2_conv.h.
|
protected |
Definition at line 229 of file smt2_conv.h.
|
protected |
Definition at line 84 of file smt2_conv.h.
|
protected |
Definition at line 82 of file smt2_conv.h.
|
protected |
Definition at line 90 of file smt2_conv.h.
|
protected |
Definition at line 223 of file smt2_conv.h.
|
protected |
Definition at line 83 of file smt2_conv.h.
|
protected |
Definition at line 185 of file smt2_conv.h.
|
protected |
Definition at line 226 of file smt2_conv.h.
|
protected |
Definition at line 85 of file smt2_conv.h.
bool smt2_convt::use_array_of_bool |
Definition at line 61 of file smt2_conv.h.
bool smt2_convt::use_datatypes |
Definition at line 60 of file smt2_conv.h.
bool smt2_convt::use_FPA_theory |
Definition at line 59 of file smt2_conv.h.