cprover
|
#include <string_refinement.h>
Public Member Functions | |
string_refinementt (const namespacet &_ns, propt &_prop, unsigned refinement_bound) | |
void | set_mode () |
determine which language should be used More... | |
virtual std::string | decision_procedure_text () const |
![]() | |
bv_refinementt (const namespacet &_ns, propt &_prop) | |
~bv_refinementt () | |
void | set_ui (language_uit::uit _ui) |
![]() | |
bv_pointerst (const namespacet &_ns, propt &_prop) | |
void | post_process () override |
![]() | |
boolbvt (const namespacet &_ns, propt &_prop) | |
virtual const bvt & | convert_bv (const exprt &expr) |
exprt | get (const exprt &expr) const override |
void | print_assignment (std::ostream &out) const override |
void | clear_cache () override |
virtual bool | literal (const exprt &expr, std::size_t bit, literalt &literal) const |
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 |
![]() | |
arrayst (const namespacet &_ns, propt &_prop) | |
literalt | record_array_equality (const equal_exprt &expr) |
void | record_array_index (const index_exprt &expr) |
![]() | |
equalityt (const namespacet &_ns, propt &_prop) | |
virtual literalt | equality (const exprt &e1, const exprt &e2) |
void | post_process () override |
![]() | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert () |
virtual tvt | l_get (literalt a) const override |
virtual void | set_frozen (literalt a) override |
virtual bool | has_set_assumptions () const override |
virtual void | set_all_frozen () override |
virtual literalt | convert (const exprt &expr) override |
virtual bool | is_in_conflict (literalt l) const override |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const override |
virtual bool | literal (const exprt &expr, literalt &literal) const |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
Static Public Member Functions | |
static exprt | is_positive (const exprt &x) |
Public Attributes | |
bool | use_counter_example |
![]() | |
unsigned | max_node_refinement |
bool | do_array_refinement |
bool | do_arithmetic_refinement |
![]() | |
unbounded_arrayt | unbounded_array |
boolbv_widtht | boolbv_width |
![]() | |
bool | use_cache |
bool | equality_propagation |
bool | freeze_all |
Protected Types | |
typedef std::set< exprt > | expr_sett |
![]() | |
typedef std::list< approximationt > | approximationst |
![]() | |
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 | lazy_typet { lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF, lazy_typet::ARRAY_TYPECAST } |
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::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 |
Protected Member Functions | |
virtual bvt | convert_symbol (const exprt &expr) |
if the expression as string type, look up for the string in the list of string symbols that we maintain, and convert it; otherwise use the method of the parent class More... | |
virtual bvt | convert_function_application (const function_application_exprt &expr) |
generate an expression, add lemmas stating that this expression corresponds to the result of the given function call, and convert this expression More... | |
decision_proceduret::resultt | dec_solve () |
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more indexes if needed. More... | |
bvt | convert_bool_bv (const exprt &boole, const exprt &orig) |
fills as many 0 as necessary in the bit vectors to have the right width More... | |
![]() | |
resultt | prop_solve () |
approximationt & | add_approximation (const exprt &expr, bvt &bv) |
void | check_SAT (approximationt &approximation) |
inspect if satisfying assignment extends to original formula, otherwise refine overapproximation More... | |
void | check_UNSAT (approximationt &approximation) |
inspect if proof holds on original formula, otherwise refine underapproximation More... | |
void | initialize (approximationt &approximation) |
void | get_values (approximationt &approximation) |
bool | is_in_conflict (approximationt &approximation) |
check if an under-approximation is part of the conflict More... | |
virtual void | check_SAT () |
virtual void | check_UNSAT () |
virtual void | post_process_arrays () |
generate array constraints More... | |
void | arrays_overapproximated () |
check whether counterexample is spurious More... | |
void | freeze_lazy_constraints () |
freeze symbols for incremental solving More... | |
virtual bvt | convert_mult (const exprt &expr) |
virtual bvt | convert_div (const div_exprt &expr) |
virtual bvt | convert_mod (const mod_exprt &expr) |
virtual bvt | convert_floatbv_op (const exprt &expr) |
virtual void | set_to (const exprt &expr, bool value) |
virtual void | set_assumptions (const bvt &_assumptions) |
![]() | |
void | encode (std::size_t object, bvt &bv) |
virtual bvt | convert_pointer_type (const exprt &expr) |
virtual void | add_addr (const exprt &expr, bvt &bv) |
bvt | convert_bitvector (const exprt &expr) override |
exprt | bv_get_rec (const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override |
bool | convert_address_of_rec (const exprt &expr, bvt &bv) |
void | offset_arithmetic (bvt &bv, const mp_integer &x) |
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const exprt &index) |
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const bvt &index_bv) |
void | do_postponed (const postponedt &postponed) |
![]() | |
void | conversion_failed (const exprt &expr, bvt &bv) |
bvt | conversion_failed (const exprt &expr) |
bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
virtual literalt | convert_bv_rel (const exprt &expr) |
virtual literalt | convert_typecast (const typecast_exprt &expr) |
conversion from bitvector types to boolean More... | |
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_overflow (const 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 exprt &expr) |
virtual literalt | convert_quantifier (const exprt &expr) |
virtual bvt | convert_index (const exprt &array, const mp_integer &index) |
index operator with constant index More... | |
virtual bvt | convert_index (const index_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) |
virtual bvt | convert_vector (const exprt &expr) |
virtual bvt | convert_complex (const exprt &expr) |
virtual bvt | convert_complex_real (const exprt &expr) |
virtual bvt | convert_complex_imag (const exprt &expr) |
virtual bvt | convert_lambda (const exprt &expr) |
virtual bvt | convert_array_of (const array_of_exprt &expr) |
virtual bvt | convert_union (const union_exprt &expr) |
virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
virtual bvt | convert_add_sub (const exprt &expr) |
virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
virtual bvt | convert_member (const member_exprt &expr) |
virtual bvt | convert_with (const exprt &expr) |
virtual bvt | convert_update (const exprt &expr) |
virtual bvt | convert_case (const exprt &expr) |
virtual bvt | convert_cond (const exprt &expr) |
virtual bvt | convert_shift (const binary_exprt &expr) |
virtual bvt | convert_bitwise (const exprt &expr) |
virtual bvt | convert_unary_minus (const unary_exprt &expr) |
virtual bvt | convert_abs (const exprt &expr) |
virtual bvt | convert_concatenation (const exprt &expr) |
virtual bvt | convert_replication (const replication_exprt &expr) |
virtual bvt | convert_bv_literals (const exprt &expr) |
virtual bvt | convert_constant (const constant_exprt &expr) |
virtual bvt | convert_extractbits (const extractbits_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 void | make_bv_expr (const typet &type, const bvt &bv, exprt &dest) |
virtual void | make_free_bv_expr (const typet &type, exprt &dest) |
void | convert_with (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_bv (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_array (const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_union (const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_struct (const struct_typet &type, const exprt &op1, const exprt &op2, 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 | post_process_quantifiers () |
void | build_offset_map (const struct_typet &src, offset_mapt &dest) |
![]() | |
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
adds array constraints (refine=true...lazily for the refinement loop) More... | |
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 | update_index_map (bool update_all) |
void | update_index_map (std::size_t i) |
merge the indices into the root More... | |
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 bool | get_bool (const exprt &expr, tvt &value) const |
get a boolean value from counter example if not valid More... | |
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 | |
void | display_index_set () |
display the current index set, for debugging More... | |
void | add_lemma (const exprt &lemma, bool add_to_index_set=true) |
add the given lemma to the solver More... | |
bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
add lemmas to the solver corresponding to the given equation More... | |
literalt | convert_rest (const exprt &expr) |
if the expression is a function application, we convert it using our own convert_function_application method More... | |
void | add_instantiations () |
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas. More... | |
bool | check_axioms () |
return true if the current model satisfies all the axioms More... | |
void | update_index_set (const exprt &formula) |
add to the index set all the indices that appear in the formula More... | |
void | update_index_set (const std::vector< exprt > &cur) |
add to the index set all the indices that appear in the formulas More... | |
void | initial_index_set (const string_constraintt &axiom) |
add to the index set all the indices that appear in the formula and the upper bound minus one More... | |
void | initial_index_set (const std::vector< string_constraintt > &string_axioms) |
add to the index set all the indices that appear in the formulas and the upper bound minus one More... | |
exprt | instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val) |
void | instantiate_not_contains (const string_not_contains_constraintt &axiom, std::list< exprt > &new_lemmas) |
exprt | compute_inverse_function (const exprt &qvar, const exprt &val, const exprt &f) |
std::map< exprt, int > | map_representation_of_sum (const exprt &f) const |
exprt | sum_over_map (std::map< exprt, int > &m, bool negated=false) const |
exprt | simplify_sum (const exprt &f) const |
exprt | get_array (const exprt &arr, const exprt &size) |
gets a model of an array and put it in a certain form More... | |
std::string | string_of_array (const exprt &arr, const exprt &size) const |
convert the content of a string to a more readable representation. More... | |
Private Attributes | |
unsigned | initial_loop_bound |
string_constraint_generatort | generator |
expr_sett | seen_instances |
std::vector< string_constraintt > | universal_axioms |
std::vector< string_not_contains_constraintt > | not_contains_axioms |
std::vector< exprt > | cur |
std::map< exprt, expr_sett > | current_index_set |
std::map< exprt, expr_sett > | index_set |
Definition at line 34 of file string_refinement.h.
|
protected |
Definition at line 54 of file string_refinement.h.
|
private |
Definition at line 66 of file string_refinement.h.
string_refinementt::string_refinementt | ( | const namespacet & | _ns, |
propt & | _prop, | ||
unsigned | refinement_bound | ||
) |
Definition at line 29 of file string_refinement.cpp.
|
private |
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas.
Definition at line 62 of file string_refinement.cpp.
References add_lemma(), current_index_set, messaget::debug(), messaget::eom(), from_expr(), instantiate(), and universal_axioms.
Referenced by dec_solve().
|
private |
add the given lemma to the solver
Definition at line 300 of file string_refinement.cpp.
References prop_conv_solvert::convert(), cur, messaget::debug(), messaget::eom(), from_expr(), exprt::is_true(), propt::l_set_to_true(), prop_conv_solvert::prop, and seen_instances.
Referenced by add_instantiations(), check_axioms(), and dec_solve().
|
privatevirtual |
add lemmas to the solver corresponding to the given equation
Reimplemented from boolbvt.
Definition at line 145 of file string_refinement.cpp.
References boolbvt::convert_bv(), messaget::debug(), messaget::eom(), prop_conv_solvert::equality_propagation, namespace_baset::follow(), prop_conv_solvert::freeze_all, from_expr(), generator, string_constraint_generatort::get_mode(), irept::id(), boolbvt::is_unbounded_array(), refined_string_typet::is_unrefined_string_type(), binary_relation_exprt::lhs(), boolbvt::map, decision_proceduret::ns, binary_relation_exprt::rhs(), prop_conv_solvert::set_frozen(), boolbv_mapt::set_literals(), set_mode(), string_constraint_generatort::set_string_symbol_equal_to_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
|
private |
return true if the current model satisfies all the axioms
Definition at line 401 of file string_refinement.cpp.
References add_lemma(), string_constraintt::body(), string_constraint_generatort::boolean_symbols, string_exprt::content(), messaget::debug(), messaget::eom(), from_expr(), from_integer(), generator, boolbvt::get(), get_array(), string_constraint_generatort::get_witness_of(), string_constraint_generatort::index_symbols, index_type(), string_exprt::length(), not_contains_axioms, decision_proceduret::ns, string_constraintt::premise(), replace_expr(), seen_instances, string_of_array(), string_constraint_generatort::symbol_to_string, string_constraintt::univ_var(), universal_axioms, and use_counter_example.
Referenced by dec_solve().
|
private |
f
corresponds to the expression $q + x$, compute_inverse_function(q,v,f)
returns an expression for $v - x$. Definition at line 642 of file string_refinement.cpp.
References messaget::debug(), messaget::eom(), map_representation_of_sum(), neg(), and sum_over_map().
Referenced by instantiate().
fills as many 0 as necessary in the bit vectors to have the right width
Definition at line 289 of file string_refinement.cpp.
References boolbvt::boolbv_width, const_literal(), prop_conv_solvert::convert(), and exprt::type().
|
protectedvirtual |
generate an expression, add lemmas stating that this expression corresponds to the result of the given function call, and convert this expression
Reimplemented from boolbvt.
Definition at line 134 of file string_refinement.cpp.
References string_constraint_generatort::add_axioms_for_function_application(), boolbvt::convert_bv(), messaget::debug(), messaget::eom(), from_expr(), and generator.
Referenced by convert_rest(), and convert_symbol().
if the expression is a function application, we convert it using our own convert_function_application method
Reimplemented from bv_pointerst.
Definition at line 92 of file string_refinement.cpp.
References convert_function_application(), bv_pointerst::convert_rest(), irept::id(), and to_function_application_expr().
if the expression as string type, look up for the string in the list of string symbols that we maintain, and convert it; otherwise use the method of the parent class
Reimplemented from boolbvt.
Definition at line 112 of file string_refinement.cpp.
References boolbvt::convert_bv(), convert_function_application(), boolbvt::convert_symbol(), dstringt::empty(), string_constraint_generatort::find_or_add_string_of_symbol(), generator, irept::get(), refined_string_typet::is_unrefined_string_type(), to_symbol_expr(), and exprt::type().
|
protectedvirtual |
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more indexes if needed.
Reimplemented from bv_refinementt.
Definition at line 204 of file string_refinement.cpp.
References add_instantiations(), add_lemma(), string_constraint_generatort::axioms, check_axioms(), cur, current_index_set, messaget::debug(), bv_refinementt::dec_solve(), display_index_set(), messaget::eom(), string_constraint_generatort::fresh_symbol(), generator, refined_string_typet::get_index_type(), irept::id(), index_type(), initial_index_set(), initial_loop_bound, instantiate_not_contains(), not_contains_axioms, string_not_contains_constraintt::s0(), to_refined_string_type(), to_string_constraint(), to_string_not_contains_constraint(), exprt::type(), universal_axioms, update_index_set(), and string_constraint_generatort::witness.
|
inlinevirtual |
Reimplemented from bv_refinementt.
Definition at line 46 of file string_refinement.h.
References is_positive(), prop_conv_solvert::prop, and propt::solver_text().
|
private |
display the current index set, for debugging
Definition at line 47 of file string_refinement.cpp.
References messaget::debug(), messaget::eom(), from_expr(), and index_set.
Referenced by dec_solve().
gets a model of an array and put it in a certain form
Definition at line 370 of file string_refinement.cpp.
References char_type(), messaget::debug(), messaget::eom(), from_expr(), from_integer(), irept::id(), index_type(), exprt::operands(), typet::subtype(), and exprt::type().
Referenced by check_axioms().
|
private |
add to the index set all the indices that appear in the formula and the upper bound minus one
Definition at line 722 of file string_refinement.cpp.
References string_constraintt::body(), cur, current_index_set, find_qvar(), forall_operands, from_integer(), irept::id(), index_set, exprt::op0(), exprt::op1(), replace_expr(), exprt::type(), string_constraintt::univ_var(), and string_constraintt::upper_bound().
Referenced by dec_solve(), and initial_index_set().
|
private |
add to the index set all the indices that appear in the formulas and the upper bound minus one
Definition at line 704 of file string_refinement.cpp.
References initial_index_set().
|
private |
str
, and an index expression val
. qvar
the universaly quantified variable of axiom
, by an index val
, in axiom
, so that the index used for str
equals val
. For instance, if axiom
corresponds to $ q. s[q+x]='a' && t[q]='b'$, instantiate(axom,s,v)
would return an expression for $s[v]='a' && t[v-x]='b'$. Definition at line 840 of file string_refinement.cpp.
References string_constraintt::body(), compute_inverse_function(), find_index(), find_qvar(), from_integer(), irept::is_nil(), string_constraintt::premise(), r, replace_expr(), exprt::type(), string_constraintt::univ_var(), and string_constraintt::univ_within_bounds().
Referenced by add_instantiations().
|
private |
Definition at line 862 of file string_refinement.cpp.
References string_exprt::content(), messaget::debug(), messaget::eom(), from_expr(), from_integer(), generator, string_constraint_generatort::get_witness_of(), index_set, string_not_contains_constraintt::premise(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), to_string_expr(), and exprt::type().
Referenced by dec_solve().
Referenced by decision_procedure_text().
|
private |
Definition at line 523 of file string_refinement.cpp.
References cur, irept::id(), exprt::op0(), and exprt::op1().
Referenced by compute_inverse_function(), and simplify_sum().
void string_refinementt::set_mode | ( | ) |
determine which language should be used
Definition at line 37 of file string_refinement.cpp.
References CPROVER_PREFIX, messaget::debug(), messaget::eom(), generator, namespacet::lookup(), symbolt::mode, decision_proceduret::ns, and string_constraint_generatort::set_mode().
Referenced by boolbv_set_equality_to_true().
Definition at line 629 of file string_refinement.cpp.
References boolbvt::map, map_representation_of_sum(), and sum_over_map().
Referenced by update_index_set().
|
private |
convert the content of a string to a more readable representation.
This should only be used for debbuging.
Definition at line 322 of file string_refinement.cpp.
References irept::id(), MAX_CONCRETE_STRING_SIZE, exprt::operands(), to_constant_expr(), and to_unsigned_integer().
Referenced by check_axioms().
|
private |
Definition at line 566 of file string_refinement.cpp.
References binary2integer(), from_integer(), boolbvt::get_value(), irept::id(), index_type(), irept::is_nil(), irept::is_not_nil(), and to_constant_expr().
Referenced by compute_inverse_function(), and simplify_sum().
|
private |
add to the index set all the indices that appear in the formula
Definition at line 765 of file string_refinement.cpp.
References cur, current_index_set, messaget::debug(), messaget::eom(), forall_operands, from_expr(), irept::id(), index_set, exprt::op0(), exprt::op1(), simplify_sum(), and exprt::type().
Referenced by dec_solve(), and update_index_set().
|
private |
add to the index set all the indices that appear in the formulas
Definition at line 713 of file string_refinement.cpp.
References update_index_set().
|
private |
Definition at line 80 of file string_refinement.h.
Referenced by add_lemma(), dec_solve(), initial_index_set(), map_representation_of_sum(), and update_index_set().
Definition at line 84 of file string_refinement.h.
Referenced by add_instantiations(), dec_solve(), initial_index_set(), and update_index_set().
|
private |
Definition at line 70 of file string_refinement.h.
Referenced by boolbv_set_equality_to_true(), check_axioms(), convert_function_application(), convert_symbol(), dec_solve(), instantiate_not_contains(), and set_mode().
Definition at line 85 of file string_refinement.h.
Referenced by display_index_set(), initial_index_set(), instantiate_not_contains(), and update_index_set().
|
private |
Definition at line 68 of file string_refinement.h.
Referenced by dec_solve().
|
private |
Definition at line 77 of file string_refinement.h.
Referenced by check_axioms(), and dec_solve().
|
private |
Definition at line 73 of file string_refinement.h.
Referenced by add_lemma(), and check_axioms().
|
private |
Definition at line 75 of file string_refinement.h.
Referenced by add_instantiations(), check_axioms(), and dec_solve().
bool string_refinementt::use_counter_example |
Definition at line 44 of file string_refinement.h.
Referenced by check_axioms().