Skip to content

Commit

Permalink
Add a maybe_testing_function to builtin functions
Browse files Browse the repository at this point in the history
This is to know whether the result of a function can be used outside of
string operations.
  • Loading branch information
romainbrenguier committed Mar 24, 2018
1 parent 97ee2d6 commit 6609247
Showing 1 changed file with 23 additions and 0 deletions.
23 changes: 23 additions & 0 deletions src/solvers/refinement/string_builtin_function.h
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,14 @@ class string_builtin_functiont

exprt return_code;

/// Tells whether the builtin function can be a testing function, that is a
/// function that does not return a string, for instance like `equals`,
/// `indexOf` or `compare`.
virtual bool maybe_testing_function() const
{
return true;
}

private:
string_builtin_functiont() = default;

Expand Down Expand Up @@ -84,6 +92,11 @@ class string_transformation_builtin_functiont : public string_builtin_functiont

optionalt<exprt>
eval(const std::function<exprt(const exprt &)> &get_value) const override;

bool maybe_testing_function() const override
{
return false;
}
};

/// Adding a character at the end of a string
Expand Down Expand Up @@ -170,6 +183,11 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
UNREACHABLE;
};

bool maybe_testing_function() const override
{
return false;
}

protected:
explicit string_insertion_builtin_functiont(const exprt &return_code)
: string_builtin_functiont(return_code)
Expand Down Expand Up @@ -225,6 +243,11 @@ class string_creation_builtin_functiont : public string_builtin_functiont
{
return result;
}

bool maybe_testing_function() const override
{
return false;
}
};

/// String test
Expand Down

0 comments on commit 6609247

Please sign in to comment.