The initial_index_set function was not taking into account if
expressions.
We now recursively add the components of the if expression.
The function was also performing an unecessary look-up for a quantified
variable.

…nter-examples

[TG-2459] Only add counter examples when index set is exhausted

This dependency was introduced by moving language.h to langapi.
The dependency will be removed by the work in 1869 / 1935.

An SMT2 frontend plus solver binary

Fix for cbmc running out of memory while printing traces using json_ui / target: develop

This key will be used for uploading doxygen html documentation.

To keep it as fast/current as possible we will use rsync that to upload
only changes and delete what is no longer part of documentation.

And publish documentation in case of successful build.

This provides an interface satisfiable by both goto_modelt and lazy_goto_modelt.
It exposes the symbol table and function map, but with the caution that get_goto_function
may produce functions on demand, and thereby have side-effects on either of them.

This enables it to be used interchangeably with goto_modelt, with the first user
being bmct (specificially the symex-and-solve process)

…phase

This allows lazy_goto_modelt to be passed in instead of a goto_modelt's functions
map as was used previously.

…documentation

Public CPROVER documentation [TG-2181]

Changes since the assume-false-if-no-match mode was introduced had broken it, so this also adds unit tests to
ensure that the assume-false mode continues to work in future.

String constraints for insert are permisive with index that are negative
or exceed the length of the string so the eval method should do the
same, and in particular should not make an invariant fail.

It was previously not clear what could happen when the argument of
substring were out of bounds. This is now clearly specified and avoids
getting formulas with array accesses at negative indexes in particular.

This function behaves slightly differently from StringBuilder.insert
since it never raise an exception.
This tests the cases where the index exceeds the limits.

What was happening for start and end index out of bound wasn't clear and
could lead to empty index set because the strings where sometimes
indexed at negative indices.
The behavior is now similar to substring: the actual start index is
`start_index' = max(0, start_index)` (where start_index is the argument value) and the
actual end index is `max(min(end_index, s2.length), start_index')`.

The previous version was not handling correcly the case where end_index
was smaller than start_index.

This test the CProverString.append function when start_index and
end_index arguments are proivided.

added support for rotation operators

…string-insert-eval

Fix StringBuilder.insert and String.substring [TG-2459]

…virtual-functions

Remove virtual functions: simplify and fix no-fallback-function mode

Detects when an overflow happens in the sum of two integers.
This will be used in buitin functions for dealing with the overflow case.

This function is adding assumptions on the values of integers which may
lead to contradiction. It is better to deal with overflows at the level
of the specification of the builtin functions instead.

The obtained expression can be exponentially smaller, because sparse
array representation avoids repetitions.

In the case of index_expressions this can use exponentialy less
memory.

This ensures that arrays from the underlying solver are interpreted in a
consistent manner in the solver (always using interval_sparse_arrayt).

This makes sure the way we interpret arrays is consistent even in
debugging functions.

This will allow to remove fill_in_array_expr which duplicates what
concretize does.

This is now unecessary as get_array takes care of the concretization
using sparse arrays.
This allows use to delete concretize_arrays_in_expression which is now
unused.
Equivalent behavior to this function can be obtained using sparse arrays.

We should use sparse arrays as in the solver.

…rmance

Improve performance replace_symbolt/rename_symbolt

…arrays-in-get

[TG-2721] Use sparse arrays in string_refinementt::get

Replaces the string literal "array-list".

It was not possible to declare such a constructor before because the
array_list_exprt class did not exist.