Symbolic Simulator Operations¶

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 Simulator Configuration Options 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¶

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:

  x = symbolic('x');
  a = symbolic('a', x);

• 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¶

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 symbolic and are all optional.

Expressions created from latch variables are only used to define transition systems using the write_aig function and not be sent to check_sat. See 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¶

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 symbolic 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 symbolic 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 forall 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.

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¶

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 latch function for representing the sequential input latches. There should be one output value for each input latch.

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¶

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¶

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¶

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 ith 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 symbolic. 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 symbolic 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.