20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H 30 #define MAX_CONCRETE_STRING_SIZE 500 32 #define MAX_NB_REFINEMENT 100 80 std::vector<exprt>
cur;
109 std::list<exprt> &new_lemmas);
unsigned initial_loop_bound
Generates string constraints to link results from string functions with their arguments.
std::map< exprt, int > map_representation_of_sum(const exprt &f) const
application of (mathematical) function
virtual const std::string solver_text()=0
bool boolbv_set_equality_to_true(const equal_exprt &expr)
add lemmas to the solver corresponding to the given equation
void add_instantiations()
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas.
void set_mode()
determine which language should be used
exprt get_array(const exprt &arr, const exprt &size)
gets a model of an array and put it in a certain form
std::set< exprt > expr_sett
Defines string constraints.
literalt convert_rest(const exprt &expr)
if the expression is a function application, we convert it using our own convert_function_application...
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)
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
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)
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 expressions for the string solver.
std::map< exprt, expr_sett > current_index_set
Base class for all expressions.
void display_index_set()
display the current index set, for debugging
decision_proceduret::resultt dec_solve()
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more inde...
static exprt is_positive(const exprt &x)
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)
std::vector< string_not_contains_constraintt > not_contains_axioms
std::map< exprt, expr_sett > index_set
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
std::vector< literalt > bvt
virtual std::string decision_procedure_text() 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...