Difference between revisions of "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);

% User declarations of basic types:

MyBrandNewType: TYPE;

Apples, Oranges: TYPE;

T1 : TYPE;

% Array types:

ArrayType1: TYPE = ARRAY T1 OF REAL;

ArrayType2: TYPE = ARRAY INT OF (ARRAY INT OF REAL);

ArrayType3: TYPE = ARRAY [INT, INT] OF INT;

% 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 | cons (head: INT, tail: IntList)
END;

% ASTs

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
           | cons_tl (first_t1: Tree, rest_t1: TreeList)
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;

 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

@@ Line 571: / Line 571: @@
   Apples, Oranges: TYPE;
-=== Function Types ===
-Function (<math>\to</math>) types are created by the mixfix type constructors
-<center>
-<math>
-\begin{array}{l}
-\_ \to \_ \\[1ex] (\ \_\ ,\ \_\ ) \to \_
-\\[1ex] (\ \_\ ,\ \_\ ,\ \_\ ) \to \_
-\\[1ex] \ldots
-\end{array}
-</math>
-</center>
-whose arguments can be instantiated by any first-order type.
- % Function type declarations
- UnaryFunType: TYPE = INT -> REAL;
- BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL;
- TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN;
-A function type of the form <math>(T_1, \ldots, T_n) \to T</math> with <math>n > 0</math> is interpreted as the set of all ''total'' functions from the Cartesian product <math>T_1 \times \cdots \times T_n</math> to <math>T</math>.
-The example above also shows how to introduce type names.
-A name like <code>UnaryFunType</code> above is just an abbreviation for the type <math>\mathrm{INT} \to \mathrm{REAL}</math> and can be used interchangeably with it.
-In general, any type defined by a type expression <code>E</code> can be given a name with the declaration:
- name : TYPE = E;
 === Structured Types ===
-All structured types are divided in following the families.
+CVC4's structured types are divided in the following families.
 ==== Array Types ====
@@ Line 731: / Line 699: @@
 ==== Tuple Types ====
+=== Function Types ===
+Function (<math>\to</math>) types are created by the mixfix type constructors
+<center>
+<math>
+\begin{array}{l}
+\_ \to \_ \\[1ex] (\ \_\ ,\ \_\ ) \to \_
+\\[1ex] (\ \_\ ,\ \_\ ,\ \_\ ) \to \_
+\\[1ex] \ldots
+\end{array}
+</math>
+</center>
+whose arguments can be instantiated by any first-order type.
+ % Function type declarations
+ UnaryFunType: TYPE = INT -> REAL;
+ BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL;
+ TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN;
+A function type of the form <math>(T_1, \ldots, T_n) \to T</math> with <math>n > 0</math> is interpreted as the set of all ''total'' functions from the Cartesian product <math>T_1 \times \cdots \times T_n</math> to <math>T</math>.
+The example above also shows how to introduce type names.
+A name like <code>UnaryFunType</code> above is just an abbreviation for the type <math>\mathrm{INT} \to \mathrm{REAL}</math> and can be used interchangeably with it.
+In general, any type defined by a type expression <code>E</code> can be given a name with the declaration:
+ name : TYPE = E;
 == Type Checking ==

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

Difference between revisions of "User Manual"

Revision as of 20:27, 25 October 2012

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

Tuple Types

Function Types

Type Checking

Terms and Formulas

Logical Symbols

User-defined Functions and Types

Arithmetic

Bit vectors

Arrays

Data types

Tuples and Records

Commands

QUERY

CHECKSAT

RESTART

Instantiation Patterns

Subtypes

Subtype Checking

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

Changing the output language

Proof support

Portfolio solving

Emacs support

Navigation menu

Search