Solver Plugin Model

This page is a discussion of the plugin model for solvers.

Application Domain

Currently Alloy can handle a number of SAT solvers. These SAT solvers are managed by Kodkod. The SATFactory class catalogs the different SAT solvers available provides static constants for each of them. A SATFactory can then create a SATSolver. The SATFactory can provide a solver (instance()). It can tell if it is incremental or prover.

The application project is aware of all possible SAT solvers. It has a class A4Options.SatSolver that also statics for each possible solver.

The application is also aware that some are provers and need extra options in the menu in doRefreshOption(). Currently the A4Options provide a union of all configuration information for all known SAT solvers. The application adjusts the user interface according to the selected solver.

The application also performs some actions to copy the native libraries to the file system.

The SatSolver describes the solver for the GUI. According to the selected solver, the menu items for the options are extended and certain options are managed differently.

In the A4Solution class, the the SatSolver definitions from the the A4Options class are translated by testing one by one and mapping the A4Options.SatSolver to a Kodkod SATFactory.

In the very near future, Alloy will be extended with SMT solvers that will need a different API from the current SATSolver API since it will have a much higher level interface that boolean expressions.

To be able to stop a solver, the actual solving is executed in a separate process.

    enum boolean { true, false }

    -- Core
    abstract sig SatSolver {
       id : String,
       external : String,    -- command line
       options  : seq String -- command line options
    }

    sig A4Options {
        solver : SatSolver,
        -- solver specific options
        skolemDepth : Int,
        unroll      : Int,
        intwidth    : Int
        -- ...
    }

    sig A4Solution {
        Solvers : SatSolver -> SATFactory
        solver  : Solver
    }


    -- Kodkod

    abstract sig SATFactory { 
        prover      : boolean,
        incremental : boolean,
        instance    : SATSolver,
        toString    : String -- name of the solver
    }
    abstract sig SATSolver { 
          // ...
    }
    abstract sig SATProver extends SATSolver { 
          // ...
    }

    sig Solver {
       solver : SATFactory
    }

Problem Description

Coupled

Knowledge of the available SAT solvers is currently hardcoded in all projects. This has the following disadvantages:

• Error prone – Changes in one project must be mirrored in other projects
• Complexity – A GUI needs to understand details of some solvers
• Adding Solver – Adding a solver is a lot of (error prone) work

SMT

Future SMT solvers will likely need a different API then the SATSolver API currently in place. Either Kodkod needs to be adjusted to handle SMT solvers or the SMT solver plugin needs access to either the Alloy AST or Kodkod AST.

Requirements to a Solution

• The Alloy application project must be cleaned of any native code or specific solver knowledge
• It must be possible to add a new SAT solver to Alloy without changing the application nor the core project.
• Plugins must be delivered as JARs
• It must be possible to use Maven Central to distribute plugins
• It must be possible to use a local directory in the user's Alloy home directory to add plugins
• JARs can be signed and Alloy must verify the signature if present
• Plugins must not have any external dependencies except the (currently not existing) Alloy API project.
• Transitive dependencies via Maven could be considered?
• External API must use the Java Community Process standards. Specifically:
  • JSON-B
  • JAXB
  • ...
• A Plugin JAR must be able to provide zero or more solvers
• A plugin must only provide solvers that actually can run on the platform
• Plugins must be the same for all platforms but only provide solvers on their supported platforms
• A plugin must be able to provide a configuration type for parameters
• Alloy must persist the configuration for a plugin
• Alloy must provide an automatic GUI for plugins for simple configuration data.
• Configuration must be a DTO/struct supporting fields with the following types:
  • boolean
  • int
  • double
  • String
  • enum
  • lists of the previous
• A plugin solver must be able to take over the whole solving process from the Alloy AST
• A plugin solver must provide an HTML description
• A plugin solver must have a unique id
• Plugins need metadata to verify that the version they were built against is compatible with the runtime of Alloy
• Alloy must verify that a plugin is compiled against a compatible version
• It must be possible to model the CNF writer and other built-in features as plugins.
• It must be possible for a solver to decide to run in a thread instead of a process
• It must be possible to add solvers as external system commands
• It must be possible to disable a plugin
• It must be possible to view a list of all installed plugins even if they do not contribute solvers
• Plugins must use the Java services loader model to register
• An example workspace should be provided on Github that can act as template for a new solver
• The solution must be prepared for other types of plugins, like parsers and visualizers.

Technical Solution

Strategy

Alloy in the current state is a classic application that has started small and grown over time. The code currently intertwines implementation fully with API. It will therefore first be necessary to extract an API. This API should at least be sufficient to do test cases and the application code.

Since any changes are done mostly in free time we should not go for a big bang approach. The current code works and has proven itself. Therefore, the new API should be implemented on the current code base as is without trying to improve the existing code. The new API should then first be used in extending the test cases to get experience. If this works, a new GUI project should be created that leverages the new API and takes advantage of it.

A new API should be completely defined with interfaces so that it will be easy to provide multiple implementations. This is mainly a boost for testing but it also provides significant benefits when different use cases arise. However, it mostly tends to simplify the code that uses the API since it cannot rely on implementation details.

Over time, the provider of the new API can then be migrated from the existing code base to newer implementations.