SMT Solvers Plug-in Developer Support

For user support, see SMT Solvers Plug-in

Installation from the sources

You will need to:

• Install the Eclipse Platform.
• Install the Subclipse plug-in to use SVN in Eclipse.
• Download Rodin sources into Eclipse.
• Download SMT plug-in sources into Eclipse.
  • Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.
• Install the SMT solvers you want to use.

Installing the Eclipse Platform

Download Eclipse Classic (SDK) (around 170 MB) at http://www.eclipse.org/downloads/ . Install it [1].

Installing the Subclipse plug-in

Launch Eclipse and go to Help > Install New Software....

Click the Add button and type:

http://subclipse.tigris.org/update_1.6.x

Name it (ex: SUBCLIPSE 1.6).

Then select the same items as in the following image:

Under Linux, in order to use JNI, you'll need to install the following packages:

   * libsvn-java
   * subversion
   * libsvn1

and to link the installation directory in eclipse.ini, by adding:

-Djava.library.path=/usr/lib/jni

then restart Eclipse and select JavaHL in Window > Preferences > Team > SVN.

Downloading the Rodin Sources

Open the SVN Repository Exploring perspective.

Right-clic in the SVN Repositories view, then New > Repository Location. Enter the following URL : https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp

Select all projects in trunk > RodinCore then right-clic and Checkout....

Check out into the workspace as projects must be selected. Then click Finish.

The download might be long (might take around 15min), do not interrupt.

Warning:

Once all the sources are downloaded, get back to the Java perspective. org.eventb.core.seqprover and org.eventb.core.seqprover.tests projects might need to be recompiled: select the former and press F5.

Downloading the SMT Plug-in Sources

Do the same as to dowload Rodin sources, with projects in trunk > exploratory > fages:

• org.eventb.smt.core
• org.eventb.smt.core.tests
• org.eventb.smt.help
• org.eventb.smt.ui
• org.eventb.smt.ui.tests

Configuration

You'll need to:

• Launch the Rodin platform as to set the default Run Configuration.
• Add the SMT plug-ins to this configuration.
• Set the SMT solvers you want to use within Rodin.

Launching the Rodin Platform

Once we have downloaded the Rodin sources, and built it within Eclipse, we can launch the Rodin platform.

Enter the org.rodinp.platform project and right-clic Rodin.product file then choose Run As... > Eclipse Application.

The Rodin platform is launched and ready.

Adding the SMT plug-ins to the Run Configuration

Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: Run > Run Configurations....

Select the Rodin.product configuration, and go to the Plug-ins tab. Check all the SMT Plug-ins except org.eventb.smt.core.tests and org.eventb.smt.ui.tests.

Now, you can launch the Rodin platform extended with the SMT plug-in.

SMT solvers settings

See SMT_Solvers_Plug-in#SMT_solvers_settings.