SMT-LIB Compliance - Revision history

Mdeters at 17:47, 27 September 2014

2014-09-27T17:47:16Z

2013-05-29T16:58:44Z

2013-05-29T16:58:19Z

2013-04-02T19:46:08Z

2012-12-03T19:31:37Z

2012-10-09T20:53:29Z

2012-10-09T20:17:03Z

2012-10-09T20:16:53Z

2012-10-09T20:14:51Z

2012-10-09T20:13:14Z

@@ Line 3: / Line 3: @@
 There are areas where we don't support full functionality, or where we are not compliant:
 * We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
-** '''Update!''' work is ongoing (Summer/Fall 2013)
+* We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5
 Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input.  That is, it is a bit lenient in accepting non-conforming input.

@@ Line 4: / Line 4: @@
 * We do not yet support unsat core extraction (the ''get-unsat-core'' command)
-** this support will be coming Summer/Fall 2013
+** '''Update!''' this support will be coming Summer/Fall 2013
 * We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
-** work is ongoing (Summer/Fall 2013)
+** '''Update!''' work is ongoing (Summer/Fall 2013)
 Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input.  That is, it is a bit lenient in accepting non-conforming input.

@@ Line 3: / Line 3: @@
 There are areas where we don't support full functionality, or where we are not compliant:
 * 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, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input.  That is, it is a bit lenient in accepting non-conforming input.

← Older revision		Revision as of 19:46, 2 April 2013
Line 1:		Line 1:
−	CVC4 is mostly SMT-LIB-conforming with ''--lang smt''. With the ''--smtlib'' command line option, though, you get additional strictness and standards conformance.	+	CVC4 is mostly SMT-LIB-conforming with ''--lang smt''. With the ''--smtlib-strict'' 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:		There are areas where we don't support full functionality, or where we are not compliant:

@@ Line 7: / Line 7: @@
 * We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
-Also:
+Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input.  That is, it is a bit lenient in accepting non-conforming input.
-−
-* 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.'''
-−
-Please note that CVC4 is not intended as a compliance-checker for SMT-LIB input.  That is, it is a bit lenient in accepting non-conforming input.

← Older revision		Revision as of 20:53, 9 October 2012
Line 11:		Line 11:
	* 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 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.'''		* 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.'''
		+
		+	Please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input.

@@ Line 9: / Line 9: @@
 Also:
-* We do not yet support Boolean terms, e.g., function symbols that take Boolean arguments or arrays of Boolean.  '''This limitation should be fixed by the 1.0 release.'''
+* We do not yet support Boolean terms, e.g., function symbols that take Boolean arguments or arrays of Boolean.
-* 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'').  '''We plan to support abstract values when running in --smtlib compliance mode, by the 1.0 release.'''
+<br/>'''This limitation should be fixed by the 1.0 release.'''

← Older revision		Revision as of 20:14, 9 October 2012
Line 1:		Line 1:
−	~~Mostly compliant~~ with --lang smt~~, but you get extra strict/conformance things with~~ the --smtlib command line option.	+	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:		There are areas where we don't support full functionality, or where we are not compliant:

← Older revision	Revision as of 20:13, 9 October 2012
(No difference)