Difference between revisions of "User Manual"

From CVC4
Jump to: navigation, search
(→‎The CVC4 library ("in-memory") interface)
(→‎Upgrading from CVC3 to CVC4)
Line 24: Line 24:
  
 
=Upgrading from CVC3 to CVC4=
 
=Upgrading from CVC3 to CVC4=
 +
 +
==Features not supported by CVC4 (yet)==
 +
 +
===Type Correctness Conditions (TCCs)===
 +
 +
Type Correctness Conditions (TCCs), and the checking of such, are not
 +
supported by CVC4 1.0.  Thus, a function defined only on integers can be
 +
applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain,
 +
but may produce strange results.  For example:
 +
 +
  f : INT -> INT;
 +
  ASSERT f(1/3) = 0;
 +
  ASSERT f(2/3) = 1;
 +
  CHECKSAT;
 +
  % sat
 +
  COUNTEREXAMPLE;
 +
  % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
 +
 +
CVC3 can be used to produce TCCs for this input (with the +dump-tcc option).
 +
The TCC can be checked by CVC3 or another solver.  (CVC3 can also check
 +
TCCs while solving with +tcc.)
 +
 
==If you were using the text interfaces of CVC3==
 
==If you were using the text interfaces of CVC3==
 +
 +
The native language of all solvers in the CVC family, referred to as the
 +
"presentation language," has undergone some revisions for CVC4.  The
 +
most notable is that CVC4 does _not_ add counterexample assertions to
 +
the current assertion set after a SAT/INVALID result.  For example:
 +
 +
  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
 +
 +
Here, CVC4 responds "invalid" to the second and third queries, because
 +
each has a counterexample (x=2 is a counterexample to the first, and
 +
x=1 is a counterexample to the second).  However, CVC3 will respond
 +
with "valid" to one of these two, as the first query (the CHECKSAT)
 +
had the side-effect of locking CVC3 into one of the two cases; the
 +
later queries are effectively querying the counterexample that was
 +
found by the first.  CVC4 removes this side-effect of the CHECKSAT and
 +
QUERY commands.
 +
 +
CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
 +
support decimals.
 +
 +
CVC4 does not have support for the IS_INTEGER predicate.
 +
 
==If you were using the library ("in-memory") interface 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 C===
 
===If you were using CVC3 from Java===
 
===If you were using CVC3 from Java===

Revision as of 14:05, 2 October 2012

This manual includes lots of information about how to use CVC4.

It is a work in-progress.

Obtaining CVC4

Obtaining binary packages

Obtaining sources

Building from source

Compiling the prerequisites

Choosing a configuration

Building

Installing

CVC4's native input language

CVC4 support for the SMT-LIB language

See SMT-LIBv2 Compliance.

The CVC4 library ("in-memory") interface

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)

Type Correctness Conditions (TCCs), and the checking of such, are not supported by CVC4 1.0. Thus, a function defined only on integers can be applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain, but may produce strange results. For example: 

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

CVC3 can be used to produce TCCs for this input (with the +dump-tcc option). The TCC can be checked by CVC3 or another solver. (CVC3 can also check TCCs while solving with +tcc.)

If you were using the text interfaces of CVC3

The native language of all solvers in the CVC family, referred to as the "presentation language," has undergone some revisions for CVC4. The most notable is that CVC4 does _not_ add counterexample assertions to the current assertion set after a SAT/INVALID result. For example: 

 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

Here, CVC4 responds "invalid" to the second and third queries, because each has a counterexample (x=2 is a counterexample to the first, and x=1 is a counterexample to the second). However, CVC3 will respond with "valid" to one of these two, as the first query (the CHECKSAT) had the side-effect of locking CVC3 into one of the two cases; the later queries are effectively querying the counterexample that was found by the first. CVC4 removes this side-effect of the CHECKSAT and QUERY commands.

CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not support decimals.

CVC4 does not have support for the IS_INTEGER predicate.

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

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=User_Manual&oldid=3546"