.. _matlab_api_symbolic_chapter:

Symbolic Simulator Operations
==============================

In this section, we describe functions specific to Grackle.  These are
generally used to manipulate formulas or invoke constraint solvers.

.. _symbolic_config_fun:

symbolic\_config
----------------------

Provides the ability to view and update Grackle configuration options.

**Syntax**

::

   symbolic_config
   symbolic_config(option)
   x = symbolic_config(option, val)

**Description**

``symbolic_config`` allow users to view or update the current configuration
options.

-  When called with no arguments, ``symbolic_config`` will print the name of
   each variable along with the current value that it is set to.
-  When called with just the first argument ``name``, ``symbolic_config``
   will return the current value of the option.
-  When called with both arguments, ``symbolic_config`` will set the current
   value of the option.

See :ref:`config_chapter` for information about the different options.

symbolic\_config\_help
----------------------

Provides documentation about configuration options.

**Syntax**

::

    symbolic_config_help(name)

**Description**

``symbolic_config_help`` provides built-in documentation about the available
configuration variables.

-  When called with no arguments ``symbolic_config_help`` will print out
   documentation on *all* configuration variables in the system,
   including those which have no values by default (in particular, there
   may be more options printed here than are displayed by
   ``symbolic_config``).
-  When called with a string argument ``name``, ``symbolic_config_help`` will
   display documentation for the named configuration variable.

assert
------

**Syntax**

::

   assert(cond, msg)

**Description**

``assert`` adds the assertion that ``cond`` holds in the current
execution context. This assertion will be appended to the condition in
subsequent calls to ``check_sat``.  The optional ``msg`` argument will
be printed in the event the assertion fails.

In addition to adding ``cond`` to the current path condition,
``assert`` generates a proof obligation which states that the
condition holds in the current context.  These obligations may later
be examined or proved using the ``proof_obligations`` and
``prove_obligations`` procedures.


assume
---------

**Syntax**

::

   assume(cond)

``assume`` adds the assumption that ``cond`` holds in the current
execution context.  This assumption will be appended to the condition in
subsequent calls to ``check_sat``, as well as to the hypothesis set
of subsequent ``assert`` calls.

Unlike ``assert``, ``assume`` does not incur any proof obligation.
Instead the predicate is just silently assumed.  Thus, ``assume`` is
useful for stating preconditions of verifications, whereas ``assert``
is appropriate for safety conditions and postconditions.


.. _symbolic_fun:

symbolic
--------

Creates a fresh symbolic variable.

**Syntax**

::

 x = symbolic(name, dimensions…, class_name)

**Description**

``symbolic`` creates a new existentially quantified symbolic variable.
All arguments are optional.

-  If name ``name`` is provided, it must be a string that names a field
   used to return the value of struct when calling an SMT solver with
   functions such as ``check_sat``.
-  If ``dimensions`` are provided, they must contain non-negative
   integers providing the dimensions of the symbolic array to return. If
   a single dimension ``n`` is provided, the result is an ``n*n``
   matrix. Otherwise, the size of result has the same dimensions as the
   dimensions.

   Dimensions must be concrete values. For example, the following code
   will result in an error:

   .. raw:: html

      <pre><code>x = symbolic('x');
      a = symbolic('a', x);</code></pre>

-  ``class_name`` defines the type of created variables. It must be one
   of the following string constants:

   -  ``'integer'`` creates variables that are integers.
   -  ``'real'`` creates variables that are real numbers.
   -  ``'complex'`` creates variables that are complex numbers.
   -  ``'logical'`` creates variables that are Boolean logical
      variables.
   -  ``'intN'`` creates variables that are fixed width signed integers.
      *N* must be a positive integer, and the resulting variable's range
      is from -2N-1 to 2N-1-1.
   -  ``'uintN'`` creates variables that are fixed width integers. *N*
      must be a non-negative integer, and the resulting variable's range
      is from 0 to 2N-1.

   If only a single string is provided as an argument, it is interpreted
   as the class name, and the type is assumed to be ``'integer'``.

When passed to a solver with ``check_sat``, the variables created by
``symbolic`` are treated as existentially quantified variables, and the
solver will attempt to find an assignment under which the predicate
holds. If the variable has a name and the predicate holds, then
``check_sat`` will return the value found by the solver.

symbolic_array
----------------

**Syntax**

::

   x = symbolic_array(name, dimensions…, class_name)

**Description**

``symbolic_array`` creates a new existentially quantified symbolic array.
All arguments are optional.

-  If ``name`` is provided, must be a
   string that names a field used to return the value of struct when
   calling an SMT solver with functions such as ``check_sat``.
-  If ``dimensions`` are provided, they must must contain non-negative
   integers providing the dimensions of the symbolic array to return.
   If a single dimension ``n`` is provided, the result is an ``n*n``
   matrix.  Otherwise, the size of result has the same dimensions
   as the dimensions.

   Dimensions must be concrete values.

-  ``class_name`` defines the type of created variables.  It must be
   one of the following string constants:

   - ``'integer'`` creates an array of integers.
   - ``'real'`` creates an array of real numbers.
   - ``'complex'`` creates an array of complex numbers.
   - ``'logical'`` creates an array of boolean values.
   - ``'uintN'`` creates an array of unsigned machine integers of ``N`` bits.
   - ``'intN'`` creates an array of signed machine integers of ``N`` bits.

When passed to a solver with ``check_sat``, the variables created by
``symbolic_array`` are treated as existentially quantified array variables, and the
solver will attempt to find an assignment under which the predicate
holds.  If the variable has a name and the predicate holds, then
``check_sat`` will return the value found by the solver.

In contrast to ``symbolic``, the arrays created by ``symbolic_array``
are represented natively using the SMT theory of arrays.  This makes
indexing and updating by symbolic values much more efficient than
with the concrete arrays generated by ``symbolic``, but makes
aggregate operations difficult to support.

.. _latch_fun:

latch
------

**Syntax**

::

   x = latch(name, dimensions…, class_name)

**Description**

``latch`` creates a new value representing part of the state of a transition
system.  The arguments following the convention in :ref:`symbolic_fun` and are
all optional.

Expressions created from latch variables are only used to define transition
systems using the :ref:`write_aig` function and not be sent to ``check_sat``.
See :ref:`write_aig` for discssion about how to define the updated latch
variables.

symbolic_arrayfun
-----------------
**Syntax** ::

  [r1,…,rm] = symbolic_arrayfun(fHandle, a1,…,an)

**Description**

This operation applies a function, specified by the function handle ``fHandle``,
to each element of an array. The elements from arrays ``a1,…,an`` are passed as
input to ``fHandle`` and ``n`` is the number of parameters that the function
expects. Returns arrays ``r1,…,rm`` where ``m`` is the number of outputs from
``fHandle``.

This function is similiar to ``arrayfun``, but is geared towards symbolic
arrays.  The simulator will run the function identified by ``fHandle`` exactly
one time on symbolic inputs.  It then maps the function over the arguments.
The arguments must be builtin types supported by symbolic arrays, and the
return type must be as well.

externalize_array
-----------------
**Syntax**

::

   r = externalize_array( arr )

**Description**

Translate a symbolic array into a concrete array containing the same
values.  This operation breaks up a symbolic formula
describing an array into a collection of separate formulas, one for
each element of the array.  This may be useful because concrete arrays
support more kinds of operations than symbolic arrays.

``'integer'``, ``'real'`` and ``'complex'`` symbolic arrays will be
coerced into a concrete array of complex values.  ``'logical'``,
``'intN'``, and ``'uintN'`` symbolic arrays will be translated directly into
concrete arrays of the corresponding types.

The ``arr`` argument is required and must be a symbolic array.  The
return value will be an equivalent concrete array.

internalize_array
------------------
**Syntax**

::

   r = internalize_array( arr, class_name )

**Description**

Translate a concrete array into a symbolic array containing the same values.
This translation constructs an explicit array literal in the SMT theory
of arrays using the element values of the concrete array ``arr``.

The ``arr`` argument is required and must be an array of numeric or
logical values.  Cell arrays, struct arrays and function handles are
not allowed.

The ``class_name`` argument is optional.  If not provided, complex
arrays will be translated to complex, logical, intN and uintN arrays
will be translated to corresponding symbolic arrays.  However, if
``class_name`` is provided it must be one of the following string values;
the input array will be coerced into a symbolic array of the named type.

- ``'integer'``
- ``'real'``
- ``'complex'``
- ``'logical'``
- ``'intN'``
- ``'uintN'``

If ``class_name`` is not provided, the ``arr`` must be a concrete
array of appropriate type.  However, if ``class_name`` is provided,
``arr`` may be any array (concrete or symbolic) whose values can be
coerced into the requested type.

.. _forall_fun:

forall
------

**Syntax**

::

   p = forall(name, dimensions…, class_name, pred)

**Description**

``forall`` allows one to write predicates that contain a universally quantified
variable. The arguments ``name``, ``dimensions``, and ``class_name`` are all
interpreted as in :ref:`symbolic_fun` and are all optional. The last argument is
required, and is expected to be a Matlab function that is passed a single
symbolic value, and is expected to return a logical value.

Within the predicate, the symbolic value is treated as a free variable in calls
to ``check_sat`` or other functions that build formal models such as
``write_smtlib2``. This is to allow one to check satisfiability to determine if a
path is feasible.

Outside the predicate, the free variable cannot be directly referenced, and it
is an error to assign the symbolic variable to global variables.

The forall predicates introduced by this function are only supported in specific
solvers.  ``abc`` and ``yices`` support the **exists-forall** fragment, which allows
universally quantified predicates, but does not allow existential predicates to
be nested inside universal predicates.   ``z3`` supports nesting via heuristics
but may fail to decide if an expression is true or false.

exists
------

**Syntax**

::

   p = exists(name, dimensions…, class_name, pred)

**Description**

``exists`` is the dual of ``forall``, and allows one to write predicates over a
existentially quantified variable. The arguments ``name``, ``dimensions``, and
``class_name`` are all interpreted as in :ref:`symbolic_fun` and are all
optional. The last argument is required, and is expected to be a Matlab function
that is passed a single symbolic value, and is expected to return a logical
value.

Within the predicate, the symbolic value is treated as a free variable in calls
to ``check_sat`` or other functions that build formal models such as
``write_smtlib2``. This is to allow one to check satisfiability to determine if a
path is feasible.

Outside the predicate, the free variable cannot be directly referenced, and it
is an error to assign the symbolic variable to global variables.

Support for existential predicates varies depending on the solver.  See the
discussion in :ref:`forall_fun` for more information.

path\_condition
-------------------------

**Syntax**

::

   p = path_condition

**Description**

``path_condition`` returns the path condition of the
currently-active simulation path.  This includes all symbolic branch
conditions in the current path, as well as any symbolic assertions
made along this execution.


.. _math_check_sat:

check\_sat
----------

**Syntax**

::

   [sat,subst,bounds] = check_sat(condition)

**Description**

``check_sat`` invokes the currently-configured default solver to check
the satisfiability of the given condition in the current execution
context.  The first return value is an integer indicating if the given
condition is satisfiable: ``sat`` is ``0`` when the condition is
unsatisfiable, and is ``1`` if satisfiable.  If the problem is
satisfiable and the solver produces models, ``subst`` will be a struct
with fields containing an assignment for symbolic values created
previously by the symbolic simulator that are involved in the given
condition. If ``sat`` is ``0`` then ``subst`` is an empty struct.
Note: the path condition of the current execution path is
automatically included in the satisfiability predicate passed to the
solver.

Some solvers (in particular, dReal) return only approximately satisfying
solutions on ``sat`` answers. Such "satisfying" assignments must be used
with care! In this case, the third argument will be bound to a structure
that maps each symbolic value in the model to a bounding box around the
solution. For a real or complex symbolic value, the structure will
contain the following fields: ``real_low``, ``real_high``, ``imag_low``
and ``imag_high``. Some fields may be missing, which should be
interpreted as no bound in the associated direction (i.e., bounded by
``+inf`` or ``-inf``). Currently, only dReal uses this third argument;
other solvers return only an empty struct.

For example, on the following code:

::

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

    [sat,subst] = check_sat(x(1) + x(2) > y)

The value ``sat`` will be ``1``, and ``subst`` will be a record with two
elements such as

::

    subst =

        x: [1, 2]
        y: 0

This function is non-deterministic when the function has multiple
satisfying assignments.

When calling dReal, the bounding boxes may be used as follows:

::

    symbolic_config('default_solver','dreal');
    x = symbolic('x', 'real');

    [sat,subst,bounds] = check_sat( x^2 < x );

The values of the substitution and bounding boxes appears as

::

    subst =
        x: 2.6621e-04

    bounds.x{1} =
        real_low: 0
        real_high: 5.3243e-04
        imag_low: 0
        imag_high: 0


reset\_cache
--------------------------
**Syntax** ::

  reset_cache


``reset_cache`` clears the current formula cache and sets up a new
one, provided caching is currently enabled.  If caching is not
currently enabled, this function has no effect.


proof\_obligations
----------------------
**Syntax** ::

  ps = proof_obligations

``proof_obligations`` simply returns an array of logical values
representing the currently outstanding proof obligations.  Each
element of the array represents a separate proof obligation.  They are
provided in "negated goal" form, such that the proof is completed iff
the given predicate is unsatisfiable.

Calls to ``assert`` and the use of partial operations generate
proof obligations.


prove\_obligations
------------------------------
**Syntax** ::

  remaining = prove_obligations

``prove_obligations`` passes each of the currently outstanding proof
obligations to the default solver.  Any obligations which are proved
are removed from the list.  Any obligations which are disproved are
printed together with their counterexamples.

Afterward, a short summary message is printed which indicates: how many
total proofs were attempted; how many were successfully proved; how
many were falsified with a counterexample; and how many were inconclusive.

The return value indicates the number of proof obligations that remain
after all proof attempts are complete.  This count includes both proof
obligations that were falsified and those which were inconclusive.
In particular, if ``remaining`` is 0, all proof attempts were successful.

Calls to ``assert`` and the use of partial operations generate
proof obligations.

.. _write_aig:

write\_aig
--------------

**Syntax**

::

   write_aig(filename, output)
   write_aig(filename, output, latches)

**Description**

This command writes out a combinational or sequential circuit in the bit level
`AIG format`_.  Combinational circuits are specified by defining the filename
and output values.  The output values are parsed by collecting the symbolic
expressions in ``output``.  These values must be either ``logical`` values,
fixed precision ``int`` or ``uint`` values, or ``cell arrays`` containing only
``logical``, or ``int`` or ``uint`` values.

To define sequential circuit, you should first define latch variables created by
the :ref:`latch_fun` function for representing the sequential input latches.
There should be one `output` value for each input latch.

.. _AIG format: http://fmv.jku.at/aiger/


write\_dimacs
--------------

**Syntax**

::

   write_dimacs(filename, pred)

**Description**

This writes out the predicate in the DIMACS format used by SAT competitions.
The predicate ``pred`` must be formed only from logical and fixed precision
``int`` and ``uint`` operations.  The DIMACS format only support Boolean values,
and does not support any SMT theories.

.. _write_smtlib2_fun:

write\_smtlib2
--------------

**Syntax**

::

   write_smtlib2(filename, condition)

**Description**

``write_smtlib2`` generates an SMTLIB version 2 file with the given
filename that contains a theorem containing the given condition. The
file will contain free variables for each symbolic variable referred to
in the condition.

.. _write_yices_fun:

write\_yices
------------

**Syntax**

::

   write_yices(filename, condition)

**Description**

``write_yices`` generates an Yices file with the given filename that
contains a theorem containing the given condition. The file will contain
free variables for each symbolic variable referenced in the condition.

find\_mus
---------

**Syntax**

::

   mus = find_mus(fixedPredicate, clauses)

**Description**

Given a fixed predicate and a vector of clauses such that
``fixedPredicate & all( clauses )`` is unsatisfiable, find a minimal
unsatisfiable subset of the clauses.

The return value of this function is a vector of concrete boolean values
of the same length as the clause vector. The clauses that are in the
found unsatisfiable subset will be marked with a 1; clauses not in the
subset will be marked with a 0.

This function is only available when Grackle is run with the "online"
backend command-line flag.

find\_all\_mus
--------------

**Syntax**

::

   mus = find_all_mus(fixedPredicate, clauses, maxCores)

**Description**

Given a fixed predicate and a vector of clauses such that
``fixedPredicate & all( clauses )`` is unsatisfiable, find all minimal unsatisfiable
subsets of the clauses, up to the bound ``maxCores``. The return value is a
matrix of Boolean values, where each row in the matrix identifies an MUS,
just as with ``find_mus``.

This function is much like ``find_mus``, except that multiple minimal
unsatisfiable subsets are found. If run with only two arguments, *all*
MUSs will be computed and returned. If run with three arguments, then at
most ``maxCores`` MUSs will be computed.

NOTE: there may be exponentially many MUSs, so take care when asking for
all of them.

This function is only available when Grackle is run with the "online"
backend command-line flag.

.. _symbolic_fork_fun:

symbolic\_fork
--------------------

**Syntax**

::

   p = symbolic_fork

**Description**

The ``symbolic_fork`` operation creates a separate execution thread that will bypass
the post-dominator-based merging strategy in addition to the current execution
path, which will continue executing as before once the separate execution path
terminates.

The caller can use the return value to determine whether it is in the new
path or the original path.  ``symbolic_fork`` returns ``true``
to the separate execution path, and ``false`` to the original thread.

``symbolic_fork`` cannot currently be used when running ``grackle`` interactively.

Note: the way ``symbolic_fork`` is implemented causes the ``true`` branch
to be executed *all the way to program exit* before returning to
execute the ``false`` branch.  Any changes to MATLAB global variables
made on the ``true`` branch, as well as any execution result, are
discarded before resuming the ``false`` branch.
However, configuration changes made via ``symbolic_config`` and any
external side-effects (such as writing files) are retained.  The
``exit`` function may be called to immediately end a forked child;
this will only exit from the fork, and not exit the entire interpreter
(unless there is only one remaining forked child).


formula\_stats
--------------------

**Syntax**

::

   formula_stats(formula)
   formula_stats(formula, ':file', filename)

**Description**

This prints statistics about the formula to the screen or to a file if the
``:file`` option is provided.  The statistics include the number of
subexpressions in the overall formula, the theories present in the formula,
the number of subexpressions per theory, and how many subexpressions each
line contributed to the formula.

print\_formula
--------------

**Syntax**

::

   print_formula(formula)

**Description**

This will print the entire formula for a given expression to the console.  This
allows one to inspect how terms are represented internally by the simulator.

symbolic\_solvers
-----------------

**Syntax**

::

   r = symbolic_solvers

**Description**

This returns a cell array containing the names of the supported solvers.  This can
be used to check whether a given solver is available.

symbolic\_fn
-----------------

**Syntax**

::

   f = symbolic_fn(name, param_types, nargout, fun);

**Description**

This function symbolically executes the function ``fun`` on symbolic inputs whose
types are determined from ``param_types``.

The ``name`` parameter should be the name of the function.

The ``fun`` parameter should be either a function handle or an anonymous function.

The ``param_types`` parameter should be a cell array where element ``param_types{i}``
describes the type of the `i`\ th parameter.

The ``nargout`` parameter indicates the number of outputs that ``fun`` is
expected to return.

Currently, the simulator only allows input parameters to be the primitive types
supported by :ref:`symbolic_fun`.  To specify a primitive type, the type parameter
should be a singleton struct containing the fields:

* A required ``type`` field which is a string that names one of the symbolic
  types supported by the :ref:`symbolic_fun` function.

* An optional ``dims`` field, which defines should be an array of integers
  defining the dimensions.

  * If the ``dims`` field is empty for a given argument position, then it will
    be treated as denoting a singleton value.
  * If the ``dims`` field contains a single value `n`, then it will treat the
    input as a `n` by `n` matrix.
  * If the ``dim`` field contains two or more arguments, then it will treat
    those as the dimensions to an multi-dimensional array or vector.

``symbolic_fn`` returns a handle to a new function, which given arguments
with the correct types, will symbolically denote the result of applying the
input function ``fun`` to those arguments.  Semantically, the function ``r``
returned by ``symbolic_fn`` is equivalent to the input function on inputs
with the specified types.  However calls to ``r`` will not actually evaluate the
function, but instead generate a symbolic expression denoting the result.

The primary reason to use this function is to allow functions that are called
repeatedly in loop bodies to avoid the overhead of executing the loop body
at each iteration.  These functions will be used during SMTLIB and Yices
output generation as well, potentially allowing much smaller output files
and more efficient solving.

**Example**

This code generates a symbolic function that expects a single integer
argument, and a `9x4` array of real values:

::

    params{1}.type = 'integer';
    params{2}.type = 'real';
    params{2}.dims = [9 4];
    f = symbolic_fn(params, @fun);

grackle_simplify_ite
--------------------

**Syntax**

::
   [q] = grackle_simplify_ite(p)

**Description**

This simplifies the logical expression ``p`` by a set of rewrite rules that
distribute over if-then-else expressions.  These rewrite rules are not enabled
by default as they can lead to an exponential increase in the size of the terms.
However, for certain problems, we have found dramatic speedup.  These rules can
be effective if, for example, there are array access with symbolic indices that
cover a small fraction of the array.

convex_opt
--------------------

**Syntax**

::

    [feasible subst] = convex_opt(objectiveFunction, constraints)

**Description**

This performs a gradient descent optimization to find the assignments
for all relevant symbolic values to minimize ``objectiveFunction`` subject to
the ``constraints``.  The ``objectiveFunction`` must be a real value while the
constraints are a single dimension array of reals that implicitly should be
less than or equal to zero.

For example, to find the minimum point on a parabola centered at the origin but
constrained to have ``x + y >= 7`` and ``x >= 1`` one would submit:

::

    x = symbolic('x','real');
    y = symbolic('y','real');
    obj = x^2;
    constrs = [ 7 - x - y, 1 - x];
    [s model] = convex_opt(obj,constrs)

This yields an approximation that minimizes for the value of ``x^2``, modulo
constraints, such as:

::

    model =
        x: 1.0000
        y: 7.1832

Notice both the correctness and termination will suffer if non-convex objectives
or constraints are passed to ``convex_opt``.

WARNING: The convex optimization implementation is currently in an alpha state
and should not be used without steps to verify any result.

exit
-------------

**Syntax**

::

   exit
   exit(exit_code)

**Description**

This exits the symbolic simulator.  By default, the simulator will return exit
code 0.  A different exit code can be returned by providing the exit code to
``exit``, which must be an integer between 0 and 255.

Note: ``exit`` will only exit from the current execution.  By default,
there is only one execution; however, each invocation of the
``symbolic_fork`` command creates two separate executions.  If ``exit`` is
used to end an execution, but additional executions remain to be
executed, then the provided exit code is discarded.  Only the exit
code used to exit from the final remaining execution will eventually
be returned as the exit code from the Grackle executable.