SVC checks the validity of formulas which are built up from expressions. These expressions use a lisp-like prefix notation. The correct syntax for a formula is specifed below.
formula : expr
expr : expr_ref
| ( constructed_expr )
| ( svc-expr-function )
expr_ref : expr_abv
| expr_num
expr_abv : $<identifier>
expr_num : $<num>
constructed_expr: ite
| equal
| expr_abv : constructed_expr
| [ type expr ]
| expr
| built-in-function
| interpreted-function
| uninterpreted-function
| constant
ite : ITE expr expr expr
equal : = expr expr
A formula is simply any expression. Boolean expressions are built using the ITE operator which takes three arguments. The first is a Boolean condition. The second is the value of the expression if the condition is true, and the last is the value of the expression if the condition is false. An "expression reference" (expr_ref) can be used to store an expression for future reference by prepending the reference and a colon. Referring to that reference later is the same as if you had entered the original expression again. Types and different kinds of functions and constants are described below.
svc-expr-function: SVC-SUBST expr expr expr
| SVC-FS expr
| SVC-SIG expr
| SVC-SIMP expr
| SVC-CHILD expr
| SVC-READFILE
These built-in functions perform a SVC-specific operations which return new expressions. SVC-SUBST substitutes the third expr for each instance of the second expr in the first expr. SVC-FS returns the splitter that SVC would choose from the given expr. SVC-SIG returns the signature of the given expr. SVC-SIMP returns the simplest equivalent expression. SVC-CHILD returns the nth child of the given expr. Finally, SVC-READFILE returns an expr which is the result of reading the given filename.
Types can be declared for variables and uninterpreted functions. In many cases, SVC can infer the types, but in some cases, such as with records and bit-vectors, it is necessary to explicitly specify the type.
type : UNKNOWN | BOOL | RAT | CONST
| ARRAY type type
| RECORD fieldtypes ENDRECORD
| BITVEC <num>
fieldtypes : distinct type
| distinct type fieldtypes
UNKNOWN is the same as not specifying a type. An unknown type may become known after type-inference is done. BOOL and RAT indicate Boolean and rational types respectively. The CONST type is for distinct constants only. ARRAY is a type-constructor which takes two additional types as parameters. The first is the type of the index into the array, and the second is the type of the objects in the array. A RECORD type consists of a list of fields. Each field contains a field name, specified using a distinct constant, and an associated type. The optional ENDRECORD token indicates that the record type is complete. The BITVEC type constructor is used for bit-vector types. It takes one argument which is the number of bits in the bit-vector (note that BITVEC <num> is represented internally by SVC as BARRAY <num> BIT and expressions printed by SVC will use this equivalent syntax).
A number of simple abbreviations are recognized by the parser. These are translated into the equivalent expressions using ites, equals, and Boolean constants.
built-in-function : not
| not-equal
| and
| or
| xor
| implies
| equiv
not : NOT expr
not-equal : /= expr
and : AND expr-list
or : OR expr-list
xor : XOR expr-list
implies : => expr expr
equiv : <=> expr expr
An expr-list is one or more white-space separated expressions.
In strict mode, interpreted functions are denoted by the use of braces (in non-strict mode, interpreted functions can be expressed using either normal parentheses or braces-the WWW interfaces use strict mode). SVC has been designed to facilitate the addition of new interpreted functions. This release supports unbounded arrays, arithmetic, inequalities, records, and bit-vectors.
interpreted-function : <identifier> expr-list
Note that interpreted functions are case-insensitive, whereas uninterpreted functions and variables are case-sensitive.
Unbounded arrays are implemented using read and write
expressions. Read expressions are donoted by the identifier
read. They interpret the first expression as a memory
store and the second expression as an address.
read : read expr expr write : write expr expr expr
Arithmetic operators recognized by SVC include addition, multiplication, and exponentiation. SVC is complete for linear arithmetic and is only able to solve extremely simple non-linear formulas. SVC only allows constant exponants and aborts if it encounters an unsolvable non-linear arithmetic equation.
add : + expr-list mult : * expr-list exp : ^ expr rational
The standard set of inequalities are recognized by SVC. SVC only supports linear inequalities.
ineq : < expr expr
: <= expr expr
: > expr expr
: >= expr expr
Note that inequalities are currently supported only for rational expressions (i.e. having type RAT).
Records can be used to group related variables into a single convenient structure. Records and record variables can be defined and updated, and specific fields can be selected from a record.
record : record fields
record-update : recupdate expr fields
record-select : recselect expr field
fields : field expr
| field expr fields
field : distinct
Note that the first argument to both recupdate and recselect is an expression which must be of type RECORD and which must include the field(s) referenced by the following arguments.
The following functions support bit-vectors in SVC.
bit-constant : bitconst bits
bit-select : bitsel expr msb lsb
bit-concatinate : bitcat expr-list
bit-negation : bitnot expr
bit-addition : bitplus plusterms
| bitplus plussize plusterms
bits : bit
| bit bits
bit : 0
| 1
msb : <integer>
lsb : <integer>
plusterms : plusterm
| plusterm plusterms
plusterm : expr
| <integer> expr
plussize : @<integer>
Note that all expressions which appear as arguments of these functions must be of type BITVEC. A bitconst expression simply defines a constant bit-vector whose bits are then given from most significant bit to least significant bit. A bitsel expression selects from its first argument the bit-range specified by its last two arguments. A bitcat expression concatenates the bit-vectors passed as arguments (again from most significant to least significant bits). A bitnot expression represents the bit-wise negation of its argument. A bitplus expression represents the bit-vector of size n whose value is the sum mod 2^n of the plusterms passed to it, where n is plussize (if specified) or the maximum length of the bit-vectors given in plusterms if plussize is not specified. The plusterms passed to a bitplus expression are a series of one or more bit-vector expressions with optional positive integer coefficients.
If a function is not recognized as built-in or interpreted, it will be parsed as an uninterpreted function. The expr-list is processed as an ordered list of function arguments. An uninterpreted-function with no expr-list is treated as a variable.
uninterpreted-function : <identifier> expr-list
| <identifier>
There are three types of constants: boolean, rational and distinct. Distinct constants are user-defined and have their own CONST type.
constant : FALSE
| TRUE
| rational
| distinct
rational : <integer>
| <integer> | <integer>
distinct : @<identifier>