View source for SMT-LIB Compliance

From CVC4

You do not have permission to edit this page, for the following reason:

The action you have requested is limited to users in the group: Users.

You can view and copy the source of this page.

CVC4 is mostly SMT-LIB-conforming with ''--lang smt''.  With the ''--smtlib'' command line option, though, you get additional strictness and standards conformance.

There are areas where we don't support full functionality, or where we are not compliant:

* We do not yet support the ''to_real'' or ''to_int'' functions, nor the ''is_int'' predicate, from [http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2 the ''Reals_Ints'' theory].
* We do not yet support unsat core extraction (the ''get-unsat-core'' command)
* We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)

Also:

* We do not yet support Boolean terms, e.g., function symbols that take Boolean arguments or arrays of Boolean.<br/>'''This limitation should be fixed by the 1.0 release.'''
* We do not yet support abstract values.  An array can itself be printed as a term, and even a function can be printed (as a ''lambda'').<br/>'''We plan to support abstract values when running in --smtlib compliance mode, by the 1.0 release.'''

Return to SMT-LIB Compliance.

Retrieved from "http://cvc4.cs.stanford.edu/wiki/SMT-LIB_Compliance"

View source for SMT-LIB Compliance

Navigation menu

Views

Personal tools

CVC4

For CVC4 Developers

Cascade

Meta

Wiki

Search

Tools