Make string_not_contains_constraintt a struct #3256
Conversation
romainbrenguier
requested review from
martin-cs and
peterschrammel
as code owners
romainbrenguier
force-pushed
the
refactor/string-not-constains-struct
branch
3 times, most recently
from
e87fae2 to
589dd9a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 589dd9a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90066851
| @@ -116,98 +116,46 @@ inline std::string to_string(const string_constraintt &expr) | |||
| } | |||
|
|
|||
| /// Constraints to encode non containement of strings. | |||
| class string_not_contains_constraintt : public exprt | |||
| /// string_not contains_constraintt are formula of the form: | |||
There was a problem hiding this comment.
⛏️ Typo: are formula -> are formulas (or formulae?)
Also typo in commit message: fields that have named -> fields that have names
| @@ -46,3 +46,43 @@ string_constraintt::string_constraintt( | |||
| "String constraints must have non-negative upper bound.\n" + | |||
| upper_bound.pretty()); | |||
| } | |||
|
|
|||
| /// Used for debug printing. | |||
| /// \param [in] expr: constraint to render | |||
romainbrenguier
force-pushed
the
refactor/string-not-constains-struct
branch
from
589dd9a to
a3318cd
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a3318cd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90278315
There was a problem hiding this comment.
I don't see anything intrinsically wrong with this patch but the general approach does not seem quite right to me. Maybe there are things that I don't see here. Personally I would lean towards having the expression as an exprt and the information about it that is used during solving as a class / struct. That way we distinguish between what you are reasoning about and the working information about it.
|
|
||
| // Create witness for axiom | ||
| symbol_tablet symtab; | ||
| const namespacet empty_ns(symtab); | ||
| string_constraint_generatort generator(ns); | ||
| std::map<string_not_contains_constraintt, symbol_exprt> witnesses; | ||
| std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses; | ||
| witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type()); | ||
|
|
||
| INFO("Original axiom:\n"); |
There was a problem hiding this comment.
Side remark (not for this PR): Calling debug output INFO is a bit confusing.
| @@ -116,98 +116,46 @@ inline std::string to_string(const string_constraintt &expr) | |||
| } | |||
|
|
|||
| /// Constraints to encode non containement of strings. | |||
| class string_not_contains_constraintt : public exprt | |||
| /// string_not contains_constraintt are formulas of the form: | |||
| /// forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y] | |||
There was a problem hiding this comment.
Can this be explained in terms of the members of the struct?
The |
In particular it does not inherit from exprt anymore. Not inheriting from exprt, allows the class to be more structured. We have fields that have names describing what they contain, instead of having to define accessor methods. This also prevent us from mistakenly passing a constraint to an exprt function, which wouldn't know how to deal with a string_not_contains_constraintt.
romainbrenguier
force-pushed
the
refactor/string-not-constains-struct
branch
from
a3318cd to
14057f5
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 14057f5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90384977
|
The `string_not_contains_constraintt` is the information that is only
used by the solver. The corresponding exprt that appears in the
(goto) program are function_application_exprts (for instance
"cprover_string_index_of_func")
Personally, I'd swap out the function application for a custom exprt,
or have the model implementation call something that resolved into a
custom exprt but it is up to you.
|
In particular it does not inherit from exprt anymore.
Not inheriting from exprt, allows the class to be more structured.
We have fields that have named describing what they contain, instead of
having to define accessor methods.
This also prevent us from mistakenly passing a constraint to an exprt
function, which wouldn't know how to deal with a
string_not_contains_constraintt.