SMT Solvers Plug-in - Revision history

imported>Nicolas: /* Customizing the SMT-LIB translation settings */

2017-10-02T15:41:18Z

Customizing the SMT-LIB translation settings

← Older revision		Revision as of 15:41, 2 October 2017
Line 217:		Line 217:
	To display the SMT translation page, open the ''Preferences'' window: ''Window > Preferences'' and select the ''SMT'' node.		To display the SMT translation page, open the ''Preferences'' window: ''Window > Preferences'' and select the ''SMT'' node.

	[[Image:~~SMT_Pref~~.png\|450px]]		[[Image:SMT_TranslationConfig.png\|450px]]

	=== Setting the Temporary Directory Path ===		=== Setting the Temporary Directory Path ===

2017-10-02T15:40:44Z

Customizing the SMT-LIB translation settings

← Older revision		Revision as of 15:40, 2 October 2017
Line 217:		Line 217:
	To display the SMT translation page, open the ''Preferences'' window: ''Window > Preferences'' and select the ''SMT'' node.		To display the SMT translation page, open the ''Preferences'' window: ''Window > Preferences'' and select the ''SMT'' node.

	[[Image:~~SMT_TranslationConfig~~.png\|450px]]		[[Image:SMT_Pref.png\|450px]]

	=== Setting the Temporary Directory Path ===		=== Setting the Temporary Directory Path ===

2017-10-02T15:35:09Z

Customizing the SMT-LIB translation settings

← Older revision		Revision as of 15:35, 2 October 2017
Line 225:		Line 225:

	=== Setting the veriT Path ===		=== Setting the veriT Path ===
	Since version 0.8.0, the SMT solver veriT is bundled within the plug-in and its path used by default. However, you can change the path to another veriT binary if you want to use another version of it to produce SMT-LIB benchmarks.
	~~This information is required if you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks.~~
	~~To give a different path, click the corresponding ''Browse'' button, and select the veriT binary to use.~~

	Since version 1.3, this setting has disappeared, as the translation is always performed through PP.		Since version 1.3, this setting has disappeared, as the translation is always performed through PP.
			It was made to use veriT instead of ppTrans to translate Event-B sequents into SMT-LIB benchmarks.

	=== Setting the SMT auto tactic timeout ===		=== Setting the SMT auto tactic timeout ===

2017-10-02T15:31:54Z

Setting the Translation Directory Path

← Older revision		Revision as of 15:31, 2 October 2017
Line 219:		Line 219:
	[[Image:SMT_TranslationConfig.png\|450px]]		[[Image:SMT_TranslationConfig.png\|450px]]

	=== Setting the ~~Translation~~ Directory Path ===		=== Setting the Temporary Directory Path ===
	The plug-in needs to store some temporary files to interact with the external SMT Solver.<br>		The plug-in needs to store some temporary files to interact with the external SMT Solver.<br>
	By default, this is set to the system temporary directory path.<br/>		By default, this is set to the system temporary directory path.<br/>

2017-10-02T15:02:25Z

Installing additional SMT solvers

← Older revision		Revision as of 15:02, 2 October 2017
Line 95:		Line 95:
	* Alt-Ergo (INRIA Saclay)		* Alt-Ergo (INRIA Saclay)
	* CVC3 (New York and Iowa Universities)		* CVC3 (New York and Iowa Universities)
			* CVC4 (Stanford and Iowa Universities)
	* veriT (Loria Nancy and UFRN)		* veriT (Loria Nancy and UFRN)
	* Z3 (Microsoft Research)		* Z3 (Microsoft Research)

2017-09-29T08:40:14Z

Installing Z3

← Older revision		Revision as of 08:40, 29 September 2017
Line 122:		Line 122:

	=== Installing Z3 ===		=== Installing Z3 ===
	The Z3 solver can be downloaded from ~~http~~://~~z3.codeplex~~.com .		The Z3 solver can be downloaded from https://github.com/Z3Prover/z3/wiki .

	== Connect added solvers to the Rodin Platform ==		== Connect added solvers to the Rodin Platform ==

2017-09-07T17:28:22Z

Releases Notes: Add release notes for SMT 1.4

2016-01-15T09:42:34Z

Releases Notes: Version 1.3

← Older revision		Revision as of 09:42, 15 January 2016
Line 293:		Line 293:

	== Releases Notes ==		== Releases Notes ==

			'''Version 1.3.0'''
			* Add CVC4 and Z3, decreasing manual POs by 40% !
			* Simplify preferences:
			** always translate through PP
			** assume SMT-lib 2.0

	'''Version 1.2.0'''		'''Version 1.2.0'''

2016-01-14T16:13:25Z

Setting the veriT Path

← Older revision		Revision as of 16:13, 14 January 2016
Line 228:		Line 228:
	To give a different path, click the corresponding ''Browse'' button, and select the veriT binary to use.		To give a different path, click the corresponding ''Browse'' button, and select the veriT binary to use.

	Since version 1.3, this setting has disappeared, as the translation is always performed ~~thourgh~~ PP.		Since version 1.3, this setting has disappeared, as the translation is always performed through PP.

	=== Setting the SMT auto tactic timeout ===		=== Setting the SMT auto tactic timeout ===

2016-01-14T16:13:07Z

Setting the veriT Path

← Older revision		Revision as of 16:13, 14 January 2016
Line 227:		Line 227:
	This information is required if you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks.		This information is required if you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks.
	To give a different path, click the corresponding ''Browse'' button, and select the veriT binary to use.		To give a different path, click the corresponding ''Browse'' button, and select the veriT binary to use.

			Since version 1.3, this setting has disappeared, as the translation is always performed thourgh PP.

	=== Setting the SMT auto tactic timeout ===		=== Setting the SMT auto tactic timeout ===