32 use_counter_example(false),
33 initial_loop_bound(refinement_bound)
39 debug() <<
"initializing mode" <<
eom;
42 debug() <<
"mode detected as " << mode <<
eom;
51 const exprt &s=i.first;
54 for(
auto j : i.second)
64 debug() <<
"string_constraint_generatort::add_instantiations: " 65 <<
"going through the current index set:" <<
eom;
68 const exprt &s=i.first;
71 for(
const auto &j : i.second)
75 for(
const auto &j : i.second)
94 if(expr.
id()==ID_function_application)
115 const irep_idt &identifier=expr.
get(ID_identifier);
116 assert(!identifier.
empty());
136 debug() <<
"string_refinementt::convert_function_application " 138 exprt f=generator.add_axioms_for_function_application(expr);
139 return convert_bv(f);
157 if(expr.
lhs().
id()==ID_symbol &&
166 if(expr.
rhs().
id()==ID_typecast)
171 debug() <<
"(sr) detected casted string" <<
eom;
207 if(axiom.
id()==ID_string_constraint)
212 else if(axiom.
id()==ID_string_not_contains_constraint)
242 debug() <<
"check_SAT: got SAT but the model is not correct" <<
eom;
246 debug() <<
"check_SAT: the model is correct" <<
eom;
247 return D_SATISFIABLE;
262 debug() <<
"current index set is empty" <<
eom;
263 return D_SATISFIABLE;
267 debug()<<
"instantiating NOT_CONTAINS constraints" <<
eom;
270 debug()<<
"constraint " << i <<
eom;
271 std::list<exprt> lemmas;
273 for(
const exprt &lemma : lemmas)
281 debug() <<
"string_refinementt::dec_solve reached the maximum number" 282 <<
"of steps allowed" <<
eom;
307 debug() <<
"string_refinementt::add_lemma : tautology" <<
eom;
315 cur.push_back(lemma);
325 if(size.
id()!=ID_constant)
326 return "string of unknown size";
332 return "very long string";
336 std::ostringstream buf;
340 if(val.
id()==
"array-list")
342 for(
size_t i=0; i<val.
operands().size()/2; i++)
353 buf << static_cast<char>(c);
360 return "unable to get array-list";
376 if(val.
id()==
"array-list")
381 for(
size_t i=0; i<val.
operands().size()/2; i++)
393 debug() <<
"unable to get array-list value of " 403 debug() <<
"string_refinementt::check_axioms: ===============" 404 <<
"===========================================" <<
eom;
405 debug() <<
"string_refinementt::check_axioms: build the" 406 <<
" interpretation from the model of the prop_solver" <<
eom;
415 exprt len=
get(elength);
419 fmodel[econtent]=arr;
428 debug() <<
"" << it.get_identifier() <<
" := " 435 debug() <<
"" << it.get_identifier() <<
" := " 441 std::map<size_t, exprt> violated;
444 <<
" universal axioms" <<
eom;
460 case decision_proceduret::D_SATISFIABLE:
466 case decision_proceduret::D_UNSATISFIABLE:
469 throw "failure in checking axiom";
474 bool violated_not_contains=
false;
476 <<
" not_contains axioms" <<
eom;
483 exprt val=
get(witness);
484 violated_not_contains=
true;
487 if(violated.empty() && !violated_not_contains)
489 debug() <<
"no violated property" <<
eom;
494 debug() << violated.size() <<
" string axioms can be violated" <<
eom;
499 for(
const auto &v : violated)
501 const exprt &val=v.second;
511 debug() <<
"instance already seen" <<
eom;
524 const exprt &f)
const 527 std::map<exprt, int> elems;
529 std::list<std::pair<exprt, bool> > to_process;
530 to_process.push_back(std::make_pair(f,
true));
532 while(!to_process.empty())
535 bool positive=to_process.back().second;
536 to_process.pop_back();
537 if(
cur.id()==ID_plus)
539 to_process.push_back(std::make_pair(
cur.op1(), positive));
540 to_process.push_back(std::make_pair(
cur.op0(), positive));
542 else if(
cur.id()==ID_minus)
544 to_process.push_back(std::make_pair(
cur.op1(), !positive));
545 to_process.push_back(std::make_pair(
cur.op0(), positive));
547 else if(
cur.id()==ID_unary_minus)
549 to_process.push_back(std::make_pair(
cur.op0(), !positive));
567 std::map<exprt, int> &m,
bool negated)
const 577 for(
const auto &term : m)
580 const exprt &t=term.first;
581 int second=negated?(-term.second):term.second;
582 if(t.
id()==ID_constant)
608 for(
int i=0; i<second; i++)
613 for(
int i=0; i>second; i--)
645 exprt positive, negative;
655 auto it=elems.find(qvar);
656 assert(it!=elems.end());
657 if(it->second==1 || it->second==-1)
663 assert(it->second==0);
664 debug() <<
"in string_refinementt::compute_inverse_function:" 665 <<
" warning: occurrences of qvar canceled out " <<
eom;
705 const std::vector<string_constraintt> &string_axioms)
707 for(
const auto &axiom : string_axioms)
715 for(
const auto &axiom :
cur)
725 std::list<exprt> to_process;
726 to_process.push_back(axiom.
body());
728 while(!to_process.empty())
731 to_process.pop_back();
732 if(
cur.id()==ID_index)
759 to_process.push_back(*it);
767 std::list<exprt> to_process;
768 to_process.push_back(formula);
770 while(!to_process.empty())
773 to_process.pop_back();
774 if(
cur.id()==ID_index)
778 assert(s.
type().
id()==ID_array);
780 if(
index_set[s].insert(simplified).second)
790 to_process.push_back(*it);
808 if(expr.
id()==ID_index)
829 catch (
exprt i) {
return i; }
873 for(
auto it0 : index_set0)
874 for(
auto it1 : index_set1)
889 new_lemmas.push_back(lemma);
909 new_lemmas.push_back(witness_bounds);
The type of an expression.
virtual decision_proceduret::resultt dec_solve()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
unsigned initial_loop_bound
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
A generic base class for relations, i.e., binary predicates.
std::list< symbol_exprt > boolean_symbols
std::map< exprt, int > map_representation_of_sum(const exprt &f) const
application of (mathematical) function
virtual literalt convert(const exprt &expr) override
bool equality_propagation
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
string_exprt & to_string_expr(exprt &expr)
exprt find_index(const exprt &expr, const exprt &str)
find an index used in the expression for str, for instance with arguments (str[k] == 'a') and str...
irep_idt mode
Language mode.
literalt convert_rest(const exprt &expr) override
boolbv_widtht boolbv_width
const string_not_contains_constraintt & to_string_not_contains_constraint(const exprt &expr)
bool is_unbounded_array(const typet &type) const override
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool boolbv_set_equality_to_true(const equal_exprt &expr)
add lemmas to the solver corresponding to the given equation
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const symbol_exprt & univ_var() const
virtual void set_frozen(literalt a) override
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
exprt univ_within_bounds() const
void add_instantiations()
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas.
static mstreamt & eom(mstreamt &m)
const exprt & upper_bound() const
virtual bvt convert_symbol(const exprt &expr)
void set_mode()
determine which language should be used
void l_set_to_true(literalt a)
void set_mode(irep_idt _mode)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
find_index_visitort(const exprt &str)
std::map< irep_idt, string_exprt > symbol_to_string
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void visit(class expr_visitort &visitor)
An expression denoting infinity.
The boolean constant true.
exprt get_array(const exprt &arr, const exprt &size)
gets a model of an array and put it in a certain form
static bool is_unrefined_string_type(const typet &type)
std::set< exprt > expr_sett
const exprt & length() const
virtual const bvt & convert_bv(const exprt &expr)
const refined_string_typet & to_refined_string_type(const typet &type)
literalt convert_rest(const exprt &expr)
if the expression is a function application, we convert it using our own convert_function_application...
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
static bool find_qvar(const exprt index, const symbol_exprt &qvar)
looks for the symbol and return true if it is found
const irep_idt & get(const irep_namet &name) const
string_exprt find_or_add_string_of_symbol(const symbol_exprt &sym)
if a symbol represent a string is present in the symbol_to_string table, returns the corresponding st...
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
exprt simplify_sum(const exprt &f) const
string_refinementt(const namespacet &_ns, propt &_prop, unsigned refinement_bound)
std::list< exprt > axioms
bool check_axioms()
return true if the current model satisfies all the axioms
void update_index_set(const exprt &formula)
add to the index set all the indices that appear in the formula
#define forall_operands(it, expr)
array constructor from single element
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 give...
exprt compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
const typet & get_index_type() const
bitvector_typet index_type()
const exprt & premise() const
The unary minus expression.
std::string string_of_array(const exprt &arr, const exprt &size) const
convert the content of a string to a more readable representation.
string_constraint_generatort generator
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 ...
String support via creating string constraints and progressively instantiating the universal constrai...
literalt const_literal(bool value)
mp_integer get_value(const bvt &bv)
void set_string_symbol_equal_to_expr(const symbol_exprt &sym, const exprt &str)
add a correspondence to make sure the symbol points to the same string as the second argument ...
exprt get(const exprt &expr) const override
std::map< exprt, expr_sett > current_index_set
#define MAX_CONCRETE_STRING_SIZE
Base class for all expressions.
void display_index_set()
display the current index set, for debugging
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
decision_proceduret::resultt dec_solve()
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more inde...
const exprt & content() const
Operator to update elements in structs and arrays.
void operator()(const exprt &expr)
std::list< symbol_exprt > index_symbols
exprt sum_over_map(std::map< exprt, int > &m, bool negated=false) const
void instantiate_not_contains(const string_not_contains_constraintt &axiom, std::list< exprt > &new_lemmas)
void operator()(const exprt &expr)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Expression to hold a symbol (variable)
std::vector< string_not_contains_constraintt > not_contains_axioms
std::map< exprt, expr_sett > index_set
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const typet & subtype() const
const string_constraintt & to_string_constraint(const exprt &expr)
std::map< string_not_contains_constraintt, symbol_exprt > witness
const exprt & premise() const
std::vector< string_constraintt > universal_axioms
void add_lemma(const exprt &lemma, bool add_to_index_set=true)
add the given lemma to the solver
bitvector_typet char_type()
std::vector< literalt > bvt
const exprt & body() const
const string_exprt & s0() const
const string_exprt & s1() const
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 mainta...
find_qvar_visitort(const exprt &qvar)