User Manual

context

   cd contrib
   ./get-antlr-3.4
   cd ..
   ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3
   make
   make check   [recommended]
   make install [optional]

   ./configure --prefix=~/install_targets/cvc4 ...
   make install

 cd contrib
 ./get-antlr-3.4

 ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

 ./configure --enable-64bit ...

 MACHINE_TYPE="x86" ./get-antlr3.4

 MACHINE_TYPE="x86_64" ./get-antlr3.4

 deb http://cvc4.cs.nyu.edu/debian/ unstable/

 ./configure --enable-language-bindings=java \
     JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include

$ cvc4
cvc4 1.0 assertions:off
CVC4>

CVC4> OPTION "incremental";
CVC4> OPTION "produce-models";
CVC4> TRANSFORM 25*25;
625
CVC4> x, y : INT;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = -1;
y : INT = 0;
CVC4> ASSERT x >= 0;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = 0;
y : INT = 1;
CVC4>

$ cvc4 -im
cvc4 1.0 assertions:off
CVC4> x, y : INT;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = -1;
y : INT = 0;
CVC4> ASSERT x >= 0;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = 0;
y : INT = 1;
CVC4>

CVC4> (declare-fun x () Int)
Parse Error: <shell>:1.7: In CVC4 presentation language mode, but SMT-LIB format detected.  Use --lang smt for SMT-LIB support.
CVC4>

$ cvc4 -v file.smt2
Invoking: (set-logic AUFLIRA)
Invoking: (set-info :smt-lib-version 2.000000)
Invoking: (set-info :category "crafted")
Invoking: (set-info :status unsat)
Invoking: (declare-fun x () Real)
etc...

$ cvc4 -vv file.smt2
Invoking: (set-logic AUFLIRA)
Invoking: (set-info :smt-lib-version 2.000000)
Invoking: (set-info :category "crafted")
Invoking: (set-info :status unsat)
Invoking: (declare-fun x () Real)
etc...
expanding definitions...
constraining subtypes...
applying substitutions...
simplifying assertions...
doing static learning...
etc...

CVC4> OPTION "verbosity" 2;

CVC4> (set-option :verbosity 2)

$ cvc4 --statistics foo.smt2
sat
sat::decisions, 0
sat::propagations, 3
sat::starts, 1
theory::uf::TheoryUF::functionTermsCount, 2
theory::uf::TheoryUF::mergesCount, 2
theory::uf::TheoryUF::termsCount, 6
theory<THEORY_UF>::propagations, 1 
driver::filename, foo.smt2
driver::sat/unsat, sat
driver::totalTime, 0.02015373
[many others]

(set-logic QF_UF)
(set-info :status sat)
(exit)

%%% This is a native language comment

[To do]

x, y : REAL;
QUERY (( x <= y ) AND ( y <= x )) => ( x = y );

x, y : INT;
QUERY ((2 * x + 4 * y <= 1) AND ( y >= x)) => (x <= 0);
z : REAL;
QUERY (2 * x + z <= 3.5) AND (z >= 1);

% User declarations of basic types:

MyBrandNewType: TYPE;

Apples, Oranges: TYPE;

I : TYPE;

%% Array types:

% Arrays with indices from I and values from REAL
Array1: TYPE = ARRAY I OF REAL;

% Arrays with integer indices and array values 
Array2: TYPE = ARRAY INT OF (ARRAY INT OF REAL);

% Arrays with integer pair indices and integer values
IntMatrix: TYPE = ARRAY [INT, INT] OF INT;

IntArray: TYPE = ARRAY INT OF INT;

% Tuple type declarations

RealPair: TYPE = [REAL, REAL]

MyTuple: TYPE = [ REAL, IntArray, [INT, INT] ];

MyType: TYPE;

% Record declaration

RecordType: TYPE = [# id: REAL, age: INT, info: MyType #];

% simple enumeration type

% implicitly defined are the testers: is_red, is_yellow and is_blue
% (similarly for the other data types)

DATATYPE
  PrimaryColor = red | yellow | blue
END;

% infinite set of pairwise distinct values ..., v(-1), v(0), v(1), ...

DATATYPE
  Id = v (id: INT)
END;

% ML-style integer lists

DATATYPE
  IntList = nil | ins (head: INT, tail: IntList)
END;

% AST for lamba calculus

DATATYPE
  Term = var (index: INT)
       | apply (arg_1: Term, arg_2: Term)
       | lambda (arg: INT, body: Term)
END;

% Trees

DATATYPE
  Tree = tree (value: REAL, children: TreeList),
  TreeList = nil_tl
           | ins_tl (first_t1: Tree, rest_t1: TreeList)
END;

% Parametric pairs
DATATYPE [X, Y]
  Pair[X, Y] = pair (first: X, second: Y)
END;

% Parametric lists

DATATYPE [X]
  List[X] = nil | cons (head: X, tail: List[X])
END;

% Parametric trees using the list type above

DATATYPE [X]
  Tree[X] = node (value: X, children: List[Tree[X]]),
END;

DATATYPE
 IntStream = s (first:INT, rest: IntStream)
END;

DATATYPE
 RationalTree = node1 (child: RationalTree)
              | node2 (left_child: RationalTree, right_child:RationalTree)
END;

DATATYPE
  T1 =  c1 (s1: T2),
  T2 =  c2 (s2: T1)
END;

% Function type declarations

UnaryFunType: TYPE = INT -> REAL;

BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL;

TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN;

name : TYPE = E;

DATATYPE [X]
  List[X] = nil | cons (head: X, tail: List[X])
END;

ASSERT y = cons(1, nil::List[REAL]);

DATATYPE [X, Y]
  Union[X, Y] = left(val_l: X) | right(val_r: Y)
END;

ASSERT y = left::Union[BOOLEAN, REAL](TRUE);

% integer constants

a, b, c: INT;

% real constants

x, y, z: REAL;

% unary function

f1: REAL -> REAL;

% binary function

f2: (REAL, INT) -> REAL;

% unary function with a tuple argument

f3: [INT, REAL] -> BOOLEAN;

% binary predicate

p: (INT, REAL) -> BOOLEAN;

% Propositional "variables"

P, Q; BOOLEAN;

c: INT;

i: INT = 5 + 3*c;  % i is effectively a shorthand for 5 + 3*c

j: REAL = 3/4;

t: [REAL, INT] = (2/3, -4);

r: [# key: INT, value: REAL #] = (# key := 4, value := (c + 1)/2 #);

f: BOOLEAN = FORALL (x:INT): x <= 0 OR x > c ;

% Global declaration of x as a unary function symbol

x: REAL -> REAL;

% Local declarations of x as variable (hiding the global one)

f: REAL -> REAL = LAMBDA (x: REAL): 2*x + 3;

p: (INT, INT) -> BOOLEAN = LAMBDA (x,i: INT): i*x - 1 > 0;

g: (REAL, INT) -> [REAL, INT] = LAMBDA (x: REAL, i:INT): (x + 1, i - 3);

t: REAL =
  LET x1 = 42,
      g = LAMBDA(x:INT): x + 1,
      x2 = 2*x1 + 7/2
  IN
     (LET x3 = g(x1) IN x3 + x2) / x1;

A, B: TYPE;

q: BOOLEAN = FORALL (x,y: A, i,j,k: B): 
               i = j AND i /= k => EXISTS (z: A): x /= z OR z /= y;

A: TYPE;
i, j: INT;

% The first occurrence of i and of j in f are constant symbols,
% the others are variables.

f: BOOLEAN =  i = j AND FORALL (i,j: A): i = j OR i /= j;

A: TYPE;
b, c: A;
p, q: A -> BOOLEAN;
r: (A, A) -> BOOLEAN;

ASSERT FORALL (x0, x1, x2: A):
         PATTERN (r(x0, x1), r(x1, x2)): 
         (r(x0, x1) AND r(x1, x2)) => r(x0, x2) ;

ASSERT FORALL (x: A):
         PATTERN (r(x, b)): 
         PATTERN (r(x, c)): 
         p(x) => q(x) ;

ASSERT EXISTS (y: A):
         FORALL (x: A):
           PATTERN (r(x, y), p(y)): 
           r(x, y) => q(x) ;

% Conditional term
x, y, z, w: REAL;

t: REAL = 
  IF x > 0 THEN y
  ELSIF x >= 1 THEN z
  ELSIF x > 2 THEN w
  ELSE 2/3 ENDIF;

A: TYPE = ARRAY INT OF REAL;
a: A;
i: INT = 4;

% selection:

elem: REAL = a[i];

% update

a1: A = a WITH [10] := 1/2;

% sequential update 
% (syntactic sugar for (a WITH [10] := 2/3) WITH [42] := 3/2)

a2: A = a WITH [10] := 2/3, [42] := 3/2;

% Record construction and field selection
Item: TYPE = [# key: INT, weight: REAL #];

x: Item = (# key := 23, weight := 43/10 #);
k: INT = x.key;
v: REAL = x.weight;

% Tuple construction and projection
y: [REAL, INT, REAL] = ( 4/5, 9, 11/9 );
first_elem: REAL = y.0;
third_elem: REAL = y.2;

% Record updates

Item: TYPE = [# key: INT, weight: REAL #];

x:  Item = (# key := 23, weight := 43/10 #);

x1: Item = x WITH .weight := 48;

% Tuple updates

Tup: TYPE = [REAL,INT,REAL];
y:  Tup = ( 4/5, 9, 11/9 );
y1: Tup = y WITH .1 := 3; 

Updates to a nested component can be combined in a single WITH operator:

Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #];
State: TYPE = [# pc: INT, cache: Cache #];

s0: State;
s1: State = s0 WITH .cache[10].data := 2/3;

% Record updates

Item: TYPE = [# key: INT, weight: REAL #];

x:  Item = (# key := 23, weight := 43/10 #);

x1: Item = (# key := x.key,  weight := 48 #);

% Tuple updates

Tup: TYPE = [REAL,INT,REAL];
y:  Tup = ( 4/5, 9, 11/9 );
y1: Tup = ( y.0, 3, y.1 );

PUSH;
QUERY <formula>;
POP;

QUERY <formula>;

CVC4> invalid

RESTART <formula2>;

PUSH;
QUERY <formula>;
POP;
ASSERT <formula2>;
QUERY <formula>;

 f : INT -> INT;
 ASSERT f(1/3) = 0;
 ASSERT f(2/3) = 1;
 CHECKSAT;
 % sat
 COUNTEREXAMPLE;
 % f : (INT) -> INT = LAMBDA(x1:INT) : 0;

 x, y : INT;
 ASSERT x = 1 OR x = 2;
 ASSERT y = 1 OR y = 2;
 ASSERT x /= y;
 CHECKSAT;
 % sat
 QUERY x = 1;
 % invalid
 QUERY x = 2;
 % invalid

Solver's last result	Exit code	Notes
sat or invalid	10
unsat or valid	20
unknown	0	could be for any reason: time limit exceeded, no memory, incompleteness..
no result	0	no query or check-sat command issued
parse errors	0 (in interactive mode) 1 (otherwise)	see below
other errors	1 (usually)	see below

User Manual

Contents

What is CVC4?

Obtaining and compiling CVC4

Obtaining binary packages

Obtaining source packages

Source repository

Building from source

Quick-start instructions

Common make Options

Common configure Options

Build dependencies

Installing libantlr3c: ANTLR parser generator C support library

MacPorts

Installing the Boost C++ base libraries

Optional requirements

Building with CUDD (optional)

Language bindings

Building CVC4 from a repository checkout

Examples and tutorials are not built or installed

Appendix: Build architecture

Using the CVC4 binary

Verbosity

Getting statistics

Exit status

CVC4's native input language

Type System

Basic Types

The BOOLEAN Type

The REAL Type

The INT Type

Bit Vector Types

User-defined Basic Types

Structured Types

Array Types

Tuple Types

Record Types

Inductive Data Types

Non-Parametric Data Types

Parametric Data Types

Restriction to Inductive Types

Function Types

Type Checking

Type Ascription

Terms and Formulas

Global symbol definitions

Local symbol definitions

Built-in theories and their symbols

Logical Symbols

User-defined Functions and Types

Arithmetic

Bit vectors

Arrays

Data types

Tuples and Records

Commands

QUERY

CHECKSAT

RESTART

COUNTERMODEL

COUNTEREXAMPLE

POPTO

Instantiation Patterns

CVC4's support for the SMT-LIB language

SMT-LIB compliance

The CVC4 library interface (API)

Using CVC4 in a C++ project

Using CVC4 from Java

The compatibility interface

Upgrading from CVC3 to CVC4

Features not supported by CVC4 (yet)

Type Correctness Conditions (TCCs)

If you were using the text interfaces of CVC3

If you were using the library ("in-memory") interface of CVC3

If you were using CVC3 from C

If you were using CVC3 from Java

Useful command-line options

Statistics

Time and resource limits

Dumping API calls or preprocessed output