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>