cprover
|
#include <string_refinement.h>
Classes | |
struct | configt |
struct | infot |
string_refinementt constructor arguments More... | |
Public Member Functions | |
string_refinementt (const infot &) | |
std::string | decision_procedure_text () const override |
Return a textual description of the decision procedure. | |
exprt | get (const exprt &expr) const override |
Evaluates the given expression in the valuation found by string_refinementt::dec_solve. | |
void | set_to (const exprt &expr, bool value) override |
Record the constraints to ensure that the expression is true when the boolean is true and false otherwise. | |
![]() | |
bv_refinementt (const infot &info) | |
![]() | |
bv_pointerst (const namespacet &, propt &, message_handlert &, bool get_array_constraints=false) | |
void | finish_eager_conversion () override |
endianness_mapt | endianness_map (const typet &, bool little_endian) const override |
![]() | |
boolbvt (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false) | |
virtual const bvt & | convert_bv (const exprt &expr, const std::optional< std::size_t > expected_width={}) |
Convert expression to vector of literalts, using an internal cache to speed up conversion if available. | |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . | |
exprt | handle (const exprt &) 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. | |
void | clear_cache () override |
mp_integer | get_value (const bvt &bv) |
mp_integer | get_value (const bvt &bv, std::size_t offset, std::size_t width) |
const boolbv_mapt & | get_map () const |
virtual std::size_t | boolbv_width (const typet &type) const |
virtual endianness_mapt | endianness_map (const typet &type) const |
![]() | |
arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false) | |
literalt | record_array_equality (const equal_exprt &expr) |
void | record_array_index (const index_exprt &expr) |
![]() | |
equalityt (propt &_prop, message_handlert &message_handler) | |
virtual literalt | equality (const exprt &e1, const exprt &e2) |
void | finish_eager_conversion () override |
![]() | |
prop_conv_solvert (propt &_prop, message_handlert &message_handler) | |
virtual | ~prop_conv_solvert ()=default |
void | print_assignment (std::ostream &out) const override |
Print satisfying assignment to out . | |
tvt | l_get (literalt a) const override |
Return value of literal l from satisfying assignment. | |
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. | |
void | set_frozen (literalt) |
void | set_frozen (const bvt &) |
void | set_all_frozen () |
literalt | convert (const exprt &expr) override |
Convert a Boolean expression and return the corresponding literal. | |
bool | is_in_conflict (const exprt &expr) const override |
Returns true if an expression is in the final conflict leading to UNSAT. | |
void | push () override |
Push a new context on the stack This context becomes a child context nested in the current context. | |
void | push (const std::vector< exprt > &assumptions) override |
Push assumptions in form of literal_exprt | |
void | pop () override |
Pop whatever is on top of the stack. | |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
void | set_time_limit_seconds (uint32_t lim) override |
Set the limit for the solver to time out in seconds. | |
std::size_t | get_number_of_solver_calls () const override |
Return the number of incremental solver calls. | |
hardness_collectort * | get_hardness_collector () |
![]() | |
virtual | ~conflict_providert ()=default |
![]() | |
virtual | ~prop_convt () |
![]() | |
virtual | ~stack_decision_proceduret ()=default |
![]() | |
void | set_to_true (const exprt &) |
For a Boolean expression expr , add the constraint 'expr'. | |
void | set_to_false (const exprt &) |
For a Boolean expression expr , add the constraint 'not expr'. | |
resultt | operator() () |
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. | |
resultt | operator() (const exprt &assumption) |
Run the decision procedure to solve the problem under the given assumption. | |
virtual | ~decision_proceduret () |
![]() | |
virtual | ~solver_resource_limitst ()=default |
Protected Member Functions | |
decision_proceduret::resultt | dec_solve (const exprt &) override |
Main decision procedure of the solver. | |
![]() | |
void | finish_eager_conversion_arrays () override |
generate array constraints | |
bvt | convert_mult (const mult_exprt &expr) override |
bvt | convert_div (const div_exprt &expr) override |
bvt | convert_mod (const mod_exprt &expr) override |
bvt | convert_floatbv_op (const ieee_float_op_exprt &) override |
![]() | |
std::size_t | get_object_width (const pointer_typet &) const |
std::size_t | get_offset_width (const pointer_typet &) const |
std::size_t | get_address_width (const pointer_typet &) const |
bvt | encode (const mp_integer &object, const pointer_typet &) const |
virtual bvt | convert_pointer_type (const exprt &) |
virtual bvt | add_addr (const exprt &) |
literalt | convert_rest (const exprt &) override |
bvt | convert_bitvector (const exprt &) override |
Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit. | |
exprt | bv_get_rec (const exprt &, const bvt &, std::size_t offset) const override |
std::optional< bvt > | convert_address_of_rec (const exprt &) |
bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &) |
bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const exprt &index) |
bvt | offset_arithmetic (const pointer_typet &type, const bvt &bv, const exprt &factor, const exprt &index) |
bvt | offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const bvt &index_bv) |
std::pair< exprt, exprt > | prepare_postponed_is_dynamic_object (std::vector< symbol_exprt > &placeholders) const |
Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholders as input Boolean variables representing object bits. | |
std::unordered_map< exprt, exprt, irep_hash > | prepare_postponed_object_size (std::vector< symbol_exprt > &placeholders) const |
Create Boolean functions describing all objects of each known object size over placeholders as input Boolean variables representing object bits. | |
bvt | object_literals (const bvt &bv, const pointer_typet &type) const |
Given a pointer encoded in bv , extract the literals identifying the object that the pointer points to. | |
bvt | offset_literals (const bvt &bv, const pointer_typet &type) const |
Given a pointer encoded in bv , extract the literals representing the offset into an object that the pointer points to. | |
![]() | |
virtual bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
bvt | conversion_failed (const exprt &expr) |
Print that the expression of x has failed conversion, then return a vector of x's width. | |
bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
virtual literalt | convert_bv_rel (const binary_relation_exprt &) |
Flatten <, >, <= and >= expressions. | |
virtual literalt | convert_typecast (const typecast_exprt &expr) |
conversion from bitvector types to boolean | |
virtual literalt | convert_reduction (const unary_exprt &expr) |
virtual literalt | convert_onehot (const unary_exprt &expr) |
virtual literalt | convert_extractbit (const extractbit_exprt &expr) |
virtual literalt | convert_binary_overflow (const binary_overflow_exprt &expr) |
virtual literalt | convert_unary_overflow (const unary_overflow_exprt &expr) |
virtual literalt | convert_equality (const equal_exprt &expr) |
virtual literalt | convert_verilog_case_equality (const binary_relation_exprt &expr) |
virtual literalt | convert_ieee_float_rel (const binary_relation_exprt &) |
virtual literalt | convert_quantifier (const quantifier_exprt &expr) |
virtual bvt | convert_index (const exprt &array, const mp_integer &index) |
index operator with constant index | |
virtual bvt | convert_index (const index_exprt &expr) |
virtual bvt | convert_bswap (const bswap_exprt &expr) |
virtual bvt | convert_byte_extract (const byte_extract_exprt &expr) |
virtual bvt | convert_byte_update (const byte_update_exprt &expr) |
virtual bvt | convert_constraint_select_one (const exprt &expr) |
virtual bvt | convert_if (const if_exprt &expr) |
virtual bvt | convert_struct (const struct_exprt &expr) |
virtual bvt | convert_array (const exprt &expr) |
Flatten array. | |
virtual bvt | convert_complex (const complex_exprt &expr) |
virtual bvt | convert_complex_real (const complex_real_exprt &expr) |
virtual bvt | convert_complex_imag (const complex_imag_exprt &expr) |
virtual bvt | convert_array_comprehension (const array_comprehension_exprt &) |
virtual bvt | convert_let (const let_exprt &) |
virtual bvt | convert_array_of (const array_of_exprt &expr) |
Flatten arrays constructed from a single element. | |
virtual bvt | convert_union (const union_exprt &expr) |
virtual bvt | convert_empty_union (const empty_union_exprt &expr) |
virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
virtual bvt | convert_add_sub (const exprt &expr) |
virtual bvt | convert_floatbv_mod_rem (const binary_exprt &) |
virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
virtual bvt | convert_member (const member_exprt &expr) |
virtual bvt | convert_with (const with_exprt &expr) |
virtual bvt | convert_update (const update_exprt &) |
virtual bvt | convert_update_bit (const update_bit_exprt &) |
virtual bvt | convert_update_bits (const update_bits_exprt &) |
virtual bvt | convert_case (const exprt &expr) |
virtual bvt | convert_cond (const cond_exprt &) |
virtual bvt | convert_shift (const binary_exprt &expr) |
virtual bvt | convert_bitwise (const exprt &expr) |
virtual bvt | convert_unary_minus (const unary_minus_exprt &expr) |
virtual bvt | convert_abs (const abs_exprt &expr) |
virtual bvt | convert_concatenation (const concatenation_exprt &expr) |
virtual bvt | convert_replication (const replication_exprt &expr) |
virtual bvt | convert_constant (const constant_exprt &expr) |
virtual bvt | convert_extractbits (const extractbits_exprt &expr) |
virtual bvt | convert_symbol (const exprt &expr) |
virtual bvt | convert_bv_reduction (const unary_exprt &expr) |
virtual bvt | convert_not (const not_exprt &expr) |
virtual bvt | convert_power (const binary_exprt &expr) |
virtual bvt | convert_function_application (const function_application_exprt &expr) |
virtual bvt | convert_bitreverse (const bitreverse_exprt &expr) |
virtual bvt | convert_saturating_add_sub (const binary_exprt &expr) |
virtual bvt | convert_overflow_result (const overflow_result_exprt &expr) |
bvt | convert_update_bits (bvt src, const exprt &index, const bvt &new_value) |
void | convert_with (const typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_bv (const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_array (const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_union (const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_struct (const struct_typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv) |
void | convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv) |
virtual exprt | bv_get_unbounded_array (const exprt &) const |
exprt | bv_get (const bvt &bv, const typet &type) const |
exprt | bv_get_cache (const exprt &expr) const |
bool | is_unbounded_array (const typet &type) const override |
void | finish_eager_conversion_quantifiers () |
offset_mapt | build_offset_map (const struct_typet &src) |
binding_exprt::variablest | fresh_binding (const binding_exprt &) |
create new, unique variables for the given binding | |
![]() | |
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
adds array constraints (refine=true...lazily for the refinement loop) | |
void | display_array_constraint_count () |
std::string | enum_to_string (constraint_typet) |
void | add_array_constraints () |
void | add_array_Ackermann_constraints () |
void | add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality) |
void | add_array_constraints (const index_sett &index_set, const exprt &expr) |
void | add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt) |
void | add_array_constraints_with (const index_sett &index_set, const with_exprt &expr) |
void | add_array_constraints_update (const index_sett &index_set, const update_exprt &expr) |
void | add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt) |
void | add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt) |
void | add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr) |
void | update_index_map (bool update_all) |
void | update_index_map (std::size_t i) |
merge the indices into the root | |
void | collect_arrays (const exprt &a) |
void | collect_indices () |
void | collect_indices (const exprt &a) |
![]() | |
virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
virtual void | add_equality_constraints () |
virtual void | add_equality_constraints (const typestructt &typestruct) |
![]() | |
virtual std::optional< bool > | get_bool (const exprt &expr) const |
Get a boolean value from the model if the formula is satisfiable. | |
virtual literalt | convert_bool (const exprt &expr) |
virtual bool | set_equality_to_true (const equal_exprt &expr) |
virtual literalt | get_literal (const irep_idt &symbol) |
virtual void | ignoring (const exprt &expr) |
![]() |
Private Types | |
typedef bv_refinementt | supert |
Private Member Functions | |
string_refinementt (const infot &, bool) | |
void | add_lemma (const exprt &lemma, bool simplify_lemma=true) |
Add the given lemma to the solver. | |
Private Attributes | |
const configt | config_ |
std::size_t | loop_bound_ |
string_constraint_generatort | generator |
std::set< exprt > | seen_instances |
string_axiomst | axioms |
std::vector< exprt > | current_constraints |
index_set_pairt | index_sets |
union_find_replacet | symbol_resolve |
std::vector< exprt > | equations |
string_dependenciest | dependencies |
Related Symbols | |
(Note that these are not member symbols.) | |
std::vector< exprt > | instantiate_not_contains (const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt > > &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses) |
Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms. | |
Additional Inherited Members | |
![]() | |
enum class | unbounded_arrayt { U_NONE , U_ALL , U_AUTO } |
![]() | |
typedef equalityt | SUB |
![]() | |
using | SUB = prop_conv_solvert |
![]() | |
typedef std::map< irep_idt, literalt > | symbolst |
typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
![]() | |
enum class | resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR } |
Result of running the decision procedure. More... | |
![]() | |
unbounded_arrayt | unbounded_array |
![]() | |
bool | use_cache = true |
bool | equality_propagation = true |
bool | freeze_all = false |
![]() | |
typedef boolbvt | SUB |
typedef std::list< postponedt > | postponed_listt |
![]() | |
typedef arrayst | SUB |
typedef std::unordered_map< const exprt, bvt, irep_hash > | bv_cachet |
typedef std::list< quantifiert > | quantifier_listt |
typedef std::vector< std::size_t > | offset_mapt |
![]() | |
enum class | lazy_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET } |
enum class | constraint_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY , ARRAY_LET } |
typedef std::list< array_equalityt > | array_equalitiest |
typedef std::set< exprt > | index_sett |
typedef std::map< std::size_t, index_sett > | index_mapt |
typedef std::map< constraint_typet, size_t > | array_constraint_countt |
![]() | |
typedef std::unordered_map< const exprt, unsigned, irep_hash > | elementst |
typedef std::map< std::pair< unsigned, unsigned >, literalt > | equalitiest |
typedef std::map< unsigned, exprt > | elements_revt |
typedef std::unordered_map< const typet, typestructt, irep_hash > | typemapt |
![]() | |
static bvt | object_offset_encoding (const bvt &object, const bvt &offset) |
Construct a pointer encoding from given encodings of object and offset . | |
![]() | |
configt | config_ |
![]() | |
pointer_logict | pointer_logic |
postponed_listt | postponed_list |
![]() | |
boolbv_widtht | bv_width |
bv_utilst | bv_utils |
functionst | functions |
boolbv_mapt | map |
bv_cachet | bv_cache |
quantifier_listt | quantifier_list |
numberingt< irep_idt > | string_numbering |
std::size_t | scope_counter = 0 |
![]() | |
const namespacet & | ns |
messaget | log |
message_handlert & | message_handler |
array_equalitiest | array_equalities |
union_find< exprt, irep_hash > | arrays |
index_mapt | index_map |
bool | lazy_arrays |
bool | incremental_cache |
bool | get_array_constraints |
std::list< lazy_constraintt > | lazy_array_constraints |
std::map< exprt, bool > | expr_map |
array_constraint_countt | array_constraint_count |
std::set< std::size_t > | update_indices |
std::unordered_set< irep_idt > | array_comprehension_args |
![]() | |
typemapt | typemap |
![]() | |
bool | post_processing_done = false |
symbolst | symbols |
cachet | cache |
propt & | prop |
messaget | log |
bvt | assumption_stack |
Assumptions on the stack. | |
std::size_t | context_literal_counter = 0 |
To generate unique literal names for contexts. | |
std::vector< size_t > | context_size_stack |
assumption_stack is segmented in contexts; Number of assumptions in each context on the stack | |
![]() | |
static const char * | context_prefix = "prop_conv::context$" |
Definition at line 63 of file string_refinement.h.
Definition at line 93 of file string_refinement.h.
|
explicit |
Definition at line 165 of file string_refinement.cpp.
|
private |
Definition at line 157 of file string_refinement.cpp.
|
private |
Add the given lemma to the solver.
lemma | a Boolean expression |
simplify_lemma | whether the lemma should be simplified before being given to the underlying solver. |
Definition at line 908 of file string_refinement.cpp.
|
overrideprotectedvirtual |
Main decision procedure of the solver.
Looks for a valuation of variables compatible with the constraints that have been given to set_to
so far.
The decision procedure initiated by string_refinementt::dec_solve is composed of several steps detailed below.
Pointer symbols which are set to be equal by constraints, are replaced by an single symbol in the solver. The symbol_solvert
object used for this substitution is constructed by generate_symbol_resolution_from_equations(const std::vector<equal_exprt>&,const namespacet&,messaget::mstreamt&)
. All these symbols are then replaced using replace_symbols_in_equations(const union_find_replacet &, std::vector<equal_exprt> &)
.
Each string primitive is converted to a list of first order formulas by the function substitute_function_applications_in_equations(std::vector<equal_exprt>&,string_constraint_generatort&)
. These formulas should be unquantified or be either a string_constraintt
or a string_not_contains_constraintt
. The constraints corresponding to each primitive can be found by following the links in section String primitives.
Since only arrays appear in the string constraints, during the conversion to first order formulas, pointers are associated to arrays. The string_constraint_generatort
object keeps track of this association. It can either be set manually using the primitives cprover_associate_array_to_pointer
or a fresh array is created.
We use super_dec_solve
and super_get
to denote the methods of the underlying solver (bv_refinementt
by default). The refinement loop relies on functions string_refinementt::check_axioms
which returns true when the set of quantified constraints q
is satisfied by the valuation given bysuper_get
and string_refinementt::instantiate
which gives propositional formulas implied by a string constraint. If the following algorithm returns SAT
or UNSAT
, the given constraints are SAT
or UNSAT
respectively:
resultt::D_SATISFIABLE
if the constraints are satisfiable, resultt::D_UNSATISFIABLE
if they are unsatisfiable, resultt::D_ERROR
if the limit of iteration was reached. Reimplemented from bv_refinementt.
Definition at line 615 of file string_refinement.cpp.
|
inlineoverridevirtual |
Return a textual description of the decision procedure.
Reimplemented from bv_refinementt.
Definition at line 80 of file string_refinement.h.
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
Arrays of characters are interpreted differently from the result of supert::get: values are propagated to the left to fill unknown.
expr | an expression |
Reimplemented from boolbvt.
Definition at line 1829 of file string_refinement.cpp.
|
overridevirtual |
Record the constraints to ensure that the expression is true when the boolean is true and false otherwise.
expr | an expression of type bool |
value | the boolean value to set it to |
Reimplemented from boolbvt.
Definition at line 283 of file string_refinement.cpp.
|
related |
Instantiates a quantified formula representing not_contains
by substituting the quantifiers and generating axioms.
[in] | axiom | the axiom to instantiate |
[in] | index_pairs | pair of indexes for axiom.s0() and axiom.s1() |
[in] | witnesses | axiom 's witnesses for non containment |
Definition at line 203 of file string_constraint_instantiation.cpp.
|
private |
Definition at line 104 of file string_refinement.h.
|
private |
Definition at line 97 of file string_refinement.h.
|
private |
Definition at line 107 of file string_refinement.h.
|
private |
Definition at line 117 of file string_refinement.h.
|
private |
Definition at line 115 of file string_refinement.h.
|
private |
Definition at line 99 of file string_refinement.h.
|
private |
Definition at line 112 of file string_refinement.h.
|
private |
Definition at line 98 of file string_refinement.h.
|
private |
Definition at line 102 of file string_refinement.h.
|
private |
Definition at line 113 of file string_refinement.h.