SMT 1.4 Performance Results - Revision history

imported>Nicolas: /* Results for every prover */

2017-09-11T15:57:24Z

Results for every prover

← Older revision		Revision as of 15:57, 11 September 2017
Line 18:		Line 18:
	[[File:SMT_1.4_Perf_Remaining_POs.png]]		[[File:SMT_1.4_Perf_Remaining_POs.png]]

	== ~~Results for every prover~~ ==		== Global results ==
	Now considering the whole benchmark for every upgraded prover:		Now considering the whole benchmark for every upgraded prover:

imported>Nicolas at 15:54, 11 September 2017

2017-09-11T15:54:51Z

← Older revision		Revision as of 15:54, 11 September 2017
Line 1:		Line 1:
			== Upgraded Provers ==

	In SMT plug-in 1.4.0, the following bundled provers have been upgraded:		In SMT plug-in 1.4.0, the following bundled provers have been upgraded:
	* veriT (v2012 to v2016)		* veriT (v2012 to v2016)
Line 7:		Line 9:
	This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.		This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.

			== Results overview ==
	The following picture shows the discharged POs for each project of the performance benchmark:		The following picture shows the discharged POs for each project of the performance benchmark:

Line 15:		Line 18:
	[[File:SMT_1.4_Perf_Remaining_POs.png]]		[[File:SMT_1.4_Perf_Remaining_POs.png]]

	Now considering the whole benchmark for every prover:		== Results for every prover ==
			Now considering the whole benchmark for every upgraded prover:

	[[File:SMT_1.4_Perf_Total_Remaining_POs.png]]		[[File:SMT_1.4_Perf_Total_Remaining_POs.png]]

			Integrating the performances of the other provers:

			[[File:SMT_1.4_Perf_Total_Remaining_POs_All_Provers.png]]

	== Conclusion ==		== Conclusion ==
Line 27:		Line 35:
	'''CVC4''' has also greatly improved since its latest release: -22.4% of remaining POs.		'''CVC4''' has also greatly improved since its latest release: -22.4% of remaining POs.

	'''Z3''' has ~~globally~~ improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, Z3 remains the SMT prover with the best results.		'''Z3''' has slightly improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, Z3 remains the SMT prover with the best results.

			With '''all SMT''' provers combined (including '''CVC3'''), this is a 3.4% improvement on the remaining proof obligations.

	~~Overall~~, ~~with all SMT~~ provers ~~combined~~, ~~this~~ is a 3.4% ~~improvement on the remaining proof obligations~~. In a context where every percent is valuable, it is a sensible enhancement.		Adding '''AtelierB''', we see that the provers complement one another, and '''the overall improvement is 3.5%'''.
			In a context where every percent is valuable, it is a sensible enhancement.

	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:User documentation]]		[[Category:User documentation]]

imported>Nicolas: /* Conclusion */

2017-09-11T14:57:51Z

Conclusion

← Older revision		Revision as of 14:57, 11 September 2017
Line 23:		Line 23:
	The upgraded provers have individually improved their rate of automatically discharged proof obligations.		The upgraded provers have individually improved their rate of automatically discharged proof obligations.

	In particular, veriT has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.		In particular, '''veriT''' has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.

	CVC4 has also greatly improved since its latest release: -22.4% of remaining POs.		'''CVC4''' has also greatly improved since its latest release: -22.4% of remaining POs.

	Z3 has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, z3 remains the SMT prover with the best results.		'''Z3''' has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, Z3 remains the SMT prover with the best results.

	Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.		Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.

imported>Nicolas at 14:55, 11 September 2017

2017-09-11T14:55:22Z

← Older revision		Revision as of 14:55, 11 September 2017
Line 1:		Line 1:
	In SMT plug-in 1.4.0, the following bundled provers have been upgraded:		In SMT plug-in 1.4.0, the following bundled provers have been upgraded:
	* veriT (v2016)		* veriT (v2012 to v2016)
	* CVC4 (v1.4)		* CVC4 (v1.4 to v1.5)
	* Z3 (v4.5)		* Z3 (v4.4.1 to v4.5.0)
	Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3.		Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3.

Line 18:		Line 18:

	[[File:SMT_1.4_Perf_Total_Remaining_POs.png]]		[[File:SMT_1.4_Perf_Total_Remaining_POs.png]]

			== Conclusion ==

			The upgraded provers have individually improved their rate of automatically discharged proof obligations.

			In particular, veriT has greatly improved since the last integrated version: -46.1% of remaining POs; this can be explained by the quite old previous version that was shipped and the good work that has been done since on the prover.

			CVC4 has also greatly improved since its latest release: -22.4% of remaining POs.

			Z3 has globally improved (-1.1% of remaining POs), although a few regressions can be noticed among the previously discharged POs; however, z3 remains the SMT prover with the best results.

			Overall, with all SMT provers combined, this is a 3.4% improvement on the remaining proof obligations. In a context where every percent is valuable, it is a sensible enhancement.

	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:User documentation]]		[[Category:User documentation]]

imported>Nicolas at 17:26, 7 September 2017

2017-09-07T17:26:20Z

← Older revision		Revision as of 17:26, 7 September 2017
Line 15:		Line 15:
	[[File:SMT_1.4_Perf_Remaining_POs.png]]		[[File:SMT_1.4_Perf_Remaining_POs.png]]

			Now considering the whole benchmark for every prover:

			[[File:SMT_1.4_Perf_Total_Remaining_POs.png]]

	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:User documentation]]		[[Category:User documentation]]

imported>Nicolas: add images

2017-09-07T09:48:09Z

add images

← Older revision		Revision as of 09:48, 7 September 2017
Line 3:		Line 3:
	* CVC4 (v1.4)		* CVC4 (v1.4)
	* Z3 (v4.5)		* Z3 (v4.5)
			Note: CVC3 is still bundled but remains in the same version (v2.4.1) as in SMT 1.3.

	This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.		This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.
	~~The following picture shows the discharged POs:~~

	[[File:~~discharged~~.png]]		The following picture shows the discharged POs for each project of the performance benchmark:

			[[File:SMT_1.4_Perf_Discharged_POs.png]]

	This next image focuses on the remaining POs:		This next image focuses on the remaining POs:

	[[File:~~remaining~~.png]]		[[File:SMT_1.4_Perf_Remaining_POs.png]]


	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:User documentation]]		[[Category:User documentation]]

imported>Nicolas: Created page with "In SMT plug-in 1.4.0, the following bundled provers have been upgraded: * veriT (v2016) * CVC4 (v1.4) * Z3 (v4.5) This has led to globally improve the rate of automatically d..."

2017-09-07T09:38:26Z

Created page with "In SMT plug-in 1.4.0, the following bundled provers have been upgraded: * veriT (v2016) * CVC4 (v1.4) * Z3 (v4.5) This has led to globally improve the rate of automatically d..."

New page

In SMT plug-in 1.4.0, the following bundled provers have been upgraded:
* veriT (v2016)
* CVC4 (v1.4)
* Z3 (v4.5)

This has led to globally improve the rate of automatically discharged proof obligations (PO), thus reducing the remaining POs to prove manually.
The following picture shows the discharged POs:

[[File:discharged.png]]

This next image focuses on the remaining POs:

[[File:remaining.png]]

[[Category:Plugin]]
[[Category:User documentation]]