Overview
=========================

Grackle is a tool for symbolic analyzing MATLAB and LLVM code.  This
allows one to analyze questions such as "Can I find inputs to a program
that lead to a particular result?", or "Are there inputs that could crash
the program?"

During symbolic simulation, the simulator executes the program, and generates
expressions describing the results of operations when those operations involve
symbolic values. These expressions can then be used to generate constraint
problems that are solved using automated decision procedures such as SAT and SMT
solvers (see :ref:`constraint_chapter` for details about the supported solvers).

To understand how Grackle works, we start with a simple example showing how the
symbolic simulator could be used to solve a linear integer relations:

::

    x = symbolic('x', 'integer');
    y = symbolic('y', 'integer');

    c1 = 3*x + 5*y < 11;
    c2 = 4*x + 3*y > 13;

    [r,s] = check_sat(c1 & c2)

When run though the simulator, the output it returns is:

::

    r =

         1

    s =

        x: 5
        y: -1

The example shows that ``r`` equals 1, indicating the problem is
satisfiable, and ``s`` is a struct containing the results of the
satisfiability query.

The simulator supports both straightline code and control flow
statements such as ``if``, ``switch``, and ``for`` statements. For
example, the following code is supported by the simulator:

::

    x      = symbolic('x', 'real');
    target = symbolic('target', 'real');
    diff = 3;

    if (x > target)
      y = x - diff;
    else
      y = x + diff;
    end

    [r,c] = check_sat(abs(x-target) > diff & abs(y-target) > abs(x-target))

In this case, the example is unsatisfiable, so the result from the
simulator is:

::

    r =

         0

    c =
         struct with no fields.

In addition to calling Yices directly, the simulator can generate files
for Yices and other SMT solvers that can be used offline for
verification (see functions :ref:`write_yices_fun` or :ref:`write_smtlib2_fun` for reference).