3 CVC's presentation language

CVC reads input in a presentation language. The input is a sequence of commands. Each command ends in a semi-colon.

CVC's presentation language is typed. In a typical example, constant symbols, function symbols, and predicate symbols are declared, with their types. Then some formulas are asserted. Finally, some queries are posed, to determine whether or not the asserted formulas logically imply some other formulas.

CVC detects two types types of errors processing input. Parse errors result when CVC's parser is unable to make sense of the input. Currently, parse errors appear with just the line number where they occurred. Type errors are reported in a somewhat more informative way.

Examples of valid input to CVC are given in green below.

3.1 Commands

This section describes the commands of CVC's presentation language.

3.1.1 Type declarations

New basic types can be declared in CVC using the following syntax:

t_1, ..., t_n : TYPE;

For example, the following two CVC commands declare a, b, and c to be new basic types.

a : TYPE;
b, c : TYPE;
3.1.2 Type definitions

New types may be defined in terms of old ones using the following syntax:

t : TYPE = t';

Here, it must be the case that given the previous definitions and declarations, t' is a well-formed type. t must be a new identifier. t becomes a name (or an abbreviation) for the type t'.

For example, the following defines rPair to be an abbreviation for the tuple type [ REAL, REAL ]:

rPair : TYPE = [ REAL, REAL];

Inductive datatypes and scalar types must be given a name using a type definition. They cannot appear anywhere else, in fact, except after the equality symbol in a type definition. They are the only types whose use is restricted in this way.

For example, the following defines msg_type to be the scalar type { PING, DATA, ACK }:

msg_type : TYPE = { PING, DATA, ACK };

The expression "{ PING, DATA, ACK }" cannot be used anywhere except as the right hand side to a type definition like this one.

3.1.3 Constant declarations

Constant, function, and predicate symbols, as they are used in first-order logic, are all referred to here as constants. Constants may be declared using the following syntax:

c_1, ..., c_n : t;

Here, c_1, ..., c_n are new identifiers, and t is an expression that is a well-formed type given the previous definitions and declarations.

For example, the following declarations declare c to be a triple, f to be a function from tuples to tuples, and p to be a predicate on REALs (see the documentation on types for more information on the syntax for types).

c : [ REAL, BOOLEAN, BOOLEAN ];
f : [ [REAL, REAL] -> [BOOLEAN, BOOLEAN] ];
p : [ REAL -> BOOLEAN ];

3.1.4 Constant definitions

Constants (see above) may be defined using the following syntax:

c : t = v;

Here, c is a new identifier. Also, given the previous definitions and declarations, v is an expression of type t.

For example, the following declares r to be a record with a "width" field, and then defines r_width to be "r.width".

r : [# width : REAL, height : REAL #];
r_width : REAL = r.width;

3.1.5 ASSERT

A formula can be added to the current logical context using the following syntax:

ASSERT F;

F must be a well-formed expression (given previous definitions and declarations) of type BOOLEAN.

For example, the following is a valid assertion (given suitable declarations or definitions of x, y, and z).

ASSERT x + 2 * y = z;

It can be useful to assert some formulas, and then issue several QUERY commands. CVC may be able to process something like

ASSERT F_1;
QUERY F_2;
QUERY F_3;

faster than

QUERY F_1 => F_2;
QUERY F_1 => F_3;

("=>" is the syntax for "implies") because work performed to handle the assertion of F_1 will not be duplicated in the former case, but may be duplicated in the latter. This remark does not apply when using Chaff, where at most one query can be performed in a single execution of CVC.

3.1.6 QUERY

CVC can be queried to determine whether or not a formula is logically implied by the formulas (if there are any) in the current logical context using the following syntax:

QUERY F;

F must be a well-formed expression (given previous definitions and declarations) of type BOOLEAN. CVC will output "Valid." if F is valid in the current logical context and "Invalid." otherwise (ASSERT adds formulas to the current logical context). If CVC reports that the formula is invalid, it will remain in the logical context where the invalidity was detected. In general, this context may contain formulas that were not in the logical context when the query command was issued. This is because CVC's propositional SAT solver dynamically adds formulas to the context. The current context can be printed using WHERE.

Currently, if CVC is in SAT mode only one QUERY command can be processed in a given execution of CVC.

3.1.7 TRANSFORM

Any expression can be simplified with respect to the current logical context (see ASSERT and QUERY) using the following syntax:

TRANSFORM E;

Given previous definitions and declarations, E should be a well-formed expression (a type, term, or formula). The simplification does not necessarily reduce expressions to a canonical form. Both the simplified expression and its classifier (its type or TYPE, depending on whether it has a type or is a type) will be printed.
3.1.8 PRINT

An expression can be printed without simplification using the following syntax:

PRINT E;

Given previous definitions and declarations, E should be a well-formed expression (a type, term, or formula). Both E and its classifier (its type or TYPE, depending on whether it has a type or is a type) will be printed. What is printed may be slightly different from E. This is because CVC employs a straightforward pre-processing translation from its presentation to a simpler internal language.
3.1.9 ECHO

CVC can be told to print a string to stdout using the following syntax:

ECHO S;

S should be a string literal like "alfalfa sprouts and lima beans" (including the quotation marks). For example:

ECHO "Hello, world!";
3.1.10 INCLUDE

CVC may be directed to process another file using the INCLUDE command. The name of the file is given in double quotation marks. For example:

INCLUDE "processor_def.cvc";
INCLUDE "queries.cvc";

3.1.11 WHERE

This command prints the formulas in the current logical context (see ASSERT and QUERY). The syntax is just

WHERE;

Note that at any given point, the logical context can be different, depending on whether or not CVC is in SAT mode. This command is most useful when CVC has reported a formula that has been queried with a QUERY command is invalid. In that case, WHERE will print the assumptions under which CVC believes the negation of the formula is satisfied.

In SAT mode, many new constants are added. These new constants may appear in the formulas printed by WHERE. To print the declarations of those constants, set the TRACE option "Vars" before calling WHERE. For example:

TRACE "Vars";
WHERE;

In some cases, constructs may appear in the formulas produced by WHERE which currently are not valid input to CVC. These constructs are introduced by the decision procedures (particularly, the decision procedure for arrays) as they run. Explaining these constructs is currently beyond the scope of this documentation.

WHERE also prints the scope level of the current scope (see PUSH, etc. below for an explanation of scopes).

3.1.12 TRACE

Various options for tracing the execution of CVC may be turned on and off using the TRACE command. With no arguments, TRACE prints a list of those options. With the name of an option (in double quotation marks), it toggles the option. ALL and NONE are special options that turn on and off, respectively, all the options. TRACE will probably not be used by typical users of CVC.

3.1.13 DUMP_PROOF and DUMP_SIG

If a CVC reports that a queried (with QUERY) formula is valid, this command will dump a proof of that formula. For DUMP_PROOF to be available, CVC must not be in SAT mode, and CVC must have been invoked with the command-line option +proofs.

DUMP_PROOF may be called like this:

DUMP_PROOF;

or like this:

DUMP_PROOF "F";

where F is the name of a file to which the proof should be written. In the former case, the proof will be written to stdout.

The proof produced will generally depend on the assertions (added with ASSERT) in the current logical context, and on the declarations of types and constants. Those declarations are dumped separately using the DUMP_SIG command, which may also be called with the name of a file to use or with no arguments.

See the section on checking proofs with flea for information on how to check the proofs produced by DUMP_PROOF.

3.1.14 DUMP_ASSUMPTIONS

DUMP_ASSUMPTIONS is available under the same conditions as DUMP_PROOF, and may be called in the same way. It dumps all the assumptions that were relevant to the validity of a queried (with QUERY) formula which CVC reports to be valid.

3.1.15 PUSH, POP, POPTO, RESET, and CONTEXT

More than one logical context (see ASSERT and QUERY) can exist at the same time. To switch contexts, the CONTEXT command is used:

CONTEXT "C";

where C is the name of the context. If the context does not exist yet, it is created before CVC switches to it. There is a default context, which CVC is in when it starts. This default context is called "default". Assertions (made with ASSERT) are always added to the current context only. Queries (with QUERY) are always relative to the current context. Definitions and declarations of types and constants, on the other hand, are global across all contexts.

With no arguments, CONTEXT prints the name of the current context.

Within each context, CVC maintains a stack of scopes. To push n scopes (where n is a natural number) use this syntax:

PUSH n;

This pops n scopes:

POP n;

The index of a scope in the stack is that scope's scope level. The first scope in the stack has scope level 1. To pop all scopes after scope level n, use this syntax

POPTO n;

PUSH, POP, and POPTO can be called with no arguments, in which case a default argument of 1 is supplied. CVC is always in a scope, so it is not allowed to pop the first scope (which is the one with scope level 1). RESET is just a synonym for POPTO with no arguments.

WHERE prints the scope level of the current scope.

If CVC reports that a queried (with QUERY) formula is invalid, it will remain in the scope where the invalidity was detected.