Skip to content

Commit efb0db5

Browse files
wadoonwadoon
committed
Preps for #3597.
1 parent e2137bc commit efb0db5

File tree

2 files changed

+233
-108
lines changed

2 files changed

+233
-108
lines changed

‎docs/devel/AddingSMTSolvers.md‎

Lines changed: 116 additions & 108 deletions
Original file line numberDiff line numberDiff line change
@@ -1,115 +1,123 @@
1+
---
2+
history:
3+
- Appelhagen
4+
- Pfeifer
5+
- Weigl (2025)
6+
date: 2025-12-01
7+
---
8+
19
# Adding a new SMT Solver
210

3-
Solver properties files allow developers to
11+
With [pull request 3597](https://github.com/keyproject/key/pull/3597), we switched to a JSON-based configuration format. The previously format was `properties`-based.
412

5-
- Add support for an SMT solver currently not used by KeY (as long as it accepts SMT-LIB as input). In this case,
6-
it will likely be necessary to also implement a new subclass of de.uka.ilkd.key.smt.communication.AbstractSolverSocket
7-
to handle the solver output unless an existing solver socket suffices.
8-
- Add a new variant of an SMT solver, for example "Z3, but only with quantifier-free formulas" or "CVC5, but ignoring all formulas with casts".
9-
- Add a new variant of an SMT solver with specific options / a specific preamble (e.g., Z3 with "(set-option :produce-proofs true)").
13+
KeY allows you to add SMT (configuration) using a JSON-like files. This interface enables you to
14+
- add support for an SMT solver, with of SMT-LIB as input.
15+
- add a new variant of an SMT solver, for example *Z3, but only with quantifier-free formulas* or *CVC5, but ignoring all formulas with casts*.
16+
- add a new variant of an SMT solver with specific options or a specific preamble (e.g., Z3 with `(set-option :produce-proofs true)`).
1017

1118
This can all be done without writing a lot of own code (except for the solver socket).
1219

1320

14-
To add a solver, specify a properties (*.props*) file following the example below or the already existing properties files in the project.
15-
Afterwards, put the properties file in a *...\resources\de\uka\ilkd\key\smt\solvertypes* directory in one of the subprojects of KeY.
16-
For the solver to be usable, add the file's name to a *solvers.txt* which also should be located in the same directory as the .props file.
17-
18-
If you choose to add the properties file to the specific directory *key.core\src\main\resources\de\uka\ilkd\key\smt\solvertypes*,
19-
it will be included in an automatically (via gradle task) created *solvers.txt* file in that same directory.
20-
21-
## Specifiable properties
22-
23-
The solver's name.
24-
Should be unique amongst all used solvers, otherwise it is given a unique name throughout the solver loading process.
25-
If no name is given, the solver will be called "SMT Solver" or a unique version of that (depending on the other solvers' names).
26-
```properties
27-
name=Z3
28-
```
29-
30-
Arbitrary information about the specified solver.
31-
```properties
32-
info=Some text.
33-
```
34-
35-
The default cmd command used to start the solver process. Empty String by default, if the property is not specified.
36-
The current command can later be changed by the user in the settings.
37-
```properties
38-
command=startSolver
39-
```
40-
41-
The cmd parameters appended to the command when starting the solver program, e.g. "-in" and "-smt2".
42-
If the property is not specified, the params are an empty String by default. They can later be changed by the user in the settings.
43-
```properties
44-
params=--params
45-
```
46-
47-
The version parameter appended to the command while starting the solver program in order to get its version.
48-
If the property is not specified, it is an empty String "". Note that this cannot be changed later by the user.
49-
```properties
50-
version=--version
51-
```
52-
53-
The minimum supported version of this solver. By default, this is an empty String.
54-
Note that different versions are compared to this minimum version lexicographically - if that comparison is not possible, you may have to override the SolverTypeImplementation class.
55-
```properties
56-
minVersion=0.0.0
57-
```
58-
59-
The delimiters used by the solver program in its stdout messages. Default value is the array {"\n", "\r"}.
60-
```properties
61-
delimiters=delimiter1, delimiter2\
62-
delimiter3, delimiter4,\
63-
delimiter5
64-
```
65-
66-
The default solver process timeout (in seconds) as a long value.
67-
If the property is not set or <= -1, it is -1 by default, meaning that the general SMT timeout is used.
68-
The current timeout can later be changed by the user in the settings.
69-
```properties
70-
timeout=60
71-
```
72-
73-
The fully qualified class name of the SolverSocket class used by the solver at hand.
74-
SolverSockets are responsible for the interpretation of messages sent by the solver process, so you may need to implement a new one if the added solver so requires.
75-
See the *key.core\src\main\java\\de\uka\ilkd\key\smt\communication* package for currently available SolverSockets and adding new ones.
76-
Currently possible values for SOCKET_CLASS
77-
```properties
78-
socketClass=de.uka.ilkd.key.smt.communication.Z3Socket
79-
```
80-
81-
The fully qualified class name of the SMTTranslator class used by the solver at hand.
82-
Currently possible values for TRANSLATOR_CLASS (see the *key.core\src\main\java\\de\uka\ilkd\key\smt* package):
83-
SmtLib2Translator (legacy solvers), ModularSMTLib2Translator
84-
```properties
85-
translatorClass=de.uka.ilkd.key.smt.TRANSLATOR_CLASS
86-
```
87-
88-
The SMTHandlers used by this solver.
89-
If the property is not specified, it is an empty list by default which leads to all handlers being used.
90-
Note that this property currently only takes effect if the ModularSMTLib2Translator class is used.
91-
The handlers' names are expected to be fully qualified. Currently possible values of HANDLER_CLASS are for example:
92-
BooleanConnectiveHandler, CastHandler, CastingFunctionsHandler, DefinedSymbolsHandler, FieldConstantHandler, InstanceOfHandler, ...
93-
```properties
94-
handlers=de.uka.ilkd.key.smt.newsmt2.HANDLER_CLASS,\
95-
...
96-
```
97-
98-
The handler options (a list of arbitrary Strings) for the SMTHandlers used by the SMTTranslator.
99-
If the property is not specified, it is an empty list by default leading to default behavior of the SMTHandlers.
100-
All the used handlers handle the options on their own.
101-
```properties
102-
handlerOptions=option1,\
103-
...
104-
```
105-
106-
The path of the preamble file. By default, the *key.core\src\main\resources\de\uka\ilkd\key\smt\newsmt2\preamble.smt2* file is used as a preamble.
107-
If you want to use another, more solver-specific preamble, the file should be put in the same directory as the .props file for the solver.
108-
```properties
109-
preamble = specialPreamble.smt2
110-
```
111-
112-
If this is true, the solver is only usable in experimental mode. Generally, those are the solvers that still use the SmtLib2Translator instead of the ModularSMTLib2Translator. The property is false by default, if not specified.
113-
```properties
114-
legacy=true/false
115-
```
21+
!!! note
22+
If the SMT solver drops out of the traditional communication scheme (SMT-LIB on stdin and stdou), an integration requires an implementation via the interface of [`AbstractSolverSocket`](https://javadoc.io/doc/org.key-project/key.core/latest/de/uka/ilkd/key/smt/communication/AbstractSolverSocket.html).
23+
24+
To add a solver, you specify its properties in a JSON file, following the [schema](smt-solvers.schema.json). The SMT solver definitions are loaded from various places (in order of loading):
25+
26+
1. All resources in the classpath under the name `de/uka/ilkd/key/smt/solvertypes/smt-solvers.json`.
27+
3. The KeY user configuration folder: `~/.key/smt-solvers.json`
28+
2. Path given by a system property : `-P key.smt_solvers=<path>`
29+
1. The current working directory: `./smt-solvers.json`
30+
31+
Each file can add or substitute previous entry with the same name. Removal is currently not possible, but the substituation with an empty definition.
32+
33+
Use (4) to define SMT solvers for single project, more complex projects or scripting should rather use (3), and (2) is for user-specific but project-wide installation.
34+
35+
## The schema
36+
37+
!!! info
38+
A JSON schema file is available here: [smt-solvers.schema.json](smt-solvers.schema.json).
39+
40+
* `string name = "Z3"`
41+
42+
The solver's name.
43+
44+
Should be unique amongst all used solvers, otherwise it is given a unique name throughout the solver loading process.
45+
46+
If no name is given, the solver will be called "SMT Solver" or a unique version of that (depending on the other solvers' names).
47+
48+
* `string info;`
49+
50+
Arbitrary information about the specified solver.
51+
52+
* `string command`
53+
54+
The default cmd command used to start the solver process. Empty String by default, if the property is not specified.
55+
56+
The current command can later be changed by the user in the settings.
57+
58+
* `string params`
59+
The cmd parameters appended to the command when starting the solver program, e.g. "-in" and "-smt2".
60+
If the property is not specified, the params are an empty String by default. They can later be changed by the user in the settings.
61+
62+
* `string version = "";`
63+
64+
The version parameter appended to the command while starting the solver program in order to get its version.
65+
66+
If the property is not specified, it is an empty String. Note that this cannot be changed later by the user.
67+
68+
* `string minVersion = "";`
69+
70+
The minimum supported version of this solver. By default, this is an empty String.
71+
72+
Note that different versions are compared to this minimum version lexicographically - if that comparison is not possible, you may have to override the `SolverTypeImplementation` class.
73+
74+
* `array[string] delimiters = ['\n','\r'];`
75+
76+
The delimiters used by the solver program in its stdout messages. Default value is the array `["\n", "\r"]`.
77+
78+
* `int timeout = -1;`
79+
80+
The default solver process timeout (in seconds) as a integer value.
81+
82+
If the property is not set or non-positive, no timeout is forced.
83+
84+
The current timeout can later be changed by the user in the settings.
85+
86+
* `string socketClass="de.uka.ilkd.key.smt.communication.Z3Socket";`
87+
88+
The fully qualified class name of the SolverSocket class used by the solver at hand.
89+
SolverSockets are responsible for the interpretation of messages sent by the solver process, so you may need to implement a new one if the added solver so requires.
90+
See the *key.core\src\main\java\\de\uka\ilkd\key\smt\communication* package for currently available SolverSockets and adding new ones.
91+
Currently possible values for SOCKET_CLASS
92+
93+
* `string translatorClass = "de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator";`
94+
95+
The fully qualified class name of the SMTTranslator class used by the solver at hand.
96+
Currently possible values are subclasses of [SMTTranslator](https://javadoc.io/doc/org.key-project/key.core/latest/de/uka/ilkd/key/smt/SMTTranslator.html).
97+
98+
* `array[string] handlers = [];`
99+
100+
The SMTHandlers used by this solver.
101+
102+
If the property is not specified, it is an empty list by default which leads to all handlers being used.
103+
104+
Note, that this property currently only takes effect if the `ModularSMTLib2Translator` class is used.
105+
The handlers' names are expected to be fully qualified. Currently possible values of can be found in the [javadoc as subclasses of `SMTHandler`](https://javadoc.io/doc/org.key-project/key.core/latest/de/uka/ilkd/key/smt/newsmt2/SMTHandler.html).
106+
107+
* `array[string] handlerOptions = [];`
108+
109+
The handler options (a list of arbitrary strings) for the `SMTHandlers` used by the `SMTTranslator`.
110+
111+
If the property is not specified, it is an empty list by default leading to default behavior of the SMTHandlers.
112+
113+
All the used handlers handle the options on their own.
114+
115+
??? warn
116+
weigl: Completely unclear how to find such handlers. Or define new ones
117+
118+
119+
* `string preamble = "key.core\src\main\resources\de\uka\ilkd\key\smt\newsmt2\preamble.smt2"`
120+
121+
A string describing a resource. Traditional, the preamble is loaded from the classpath, by default, resource is used `de/uka/ilkd/key/smt/newsmt2/preamble.smt2`.
122+
123+
If the string starts with either `file:` or `http:` (e.g., `file://mypreamble.smt2` or `http://example.com/preamble.smt2`), the resource is loaded from the file system or URL instead.

‎docs/devel/smt-solvers.schema.json‎

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
{
2+
"$schema": "https://json-schema.org/draft/2020-12/schema",
3+
"$id": "https://keyproject.github.io/key-docs/devel/smt-solvers.schema.json",
4+
"title": "SMT Solvers",
5+
"description": "Schema for SMT solvers configuration used by the KeY project.",
6+
"type": "object",
7+
"additionalProperties": false,
8+
"patternProperties": {
9+
"^[ a-zA-Z0-9._-]+$": {
10+
"$ref": "#/definitions/solver"
11+
}
12+
},
13+
"$defs": {
14+
"solver": {
15+
"type": "object",
16+
"description": "Configuration for a single SMT solver.",
17+
"properties": {
18+
"experimental": {
19+
"type": "boolean",
20+
"description": "Marks solver as experimental."
21+
},
22+
"params": {
23+
"type": "string",
24+
"description": "Command-line parameters passed to the solver."
25+
},
26+
"timeout": {
27+
"type": "integer",
28+
"description": "Timeout in seconds; -1 means no timeout."
29+
},
30+
"name": {
31+
"type": "string",
32+
"description": "Should be unique amongst all used solvers, otherwise it is given a unique name throughout the solver loading process. If no name is given, the solver will be called "SMT Solver" or a unique version of that (depending on the other solvers' names)."
33+
},
34+
"info": {
35+
"type": "string",
36+
"description": "Additional information or description for the solver."
37+
},
38+
"command": {
39+
"type": "string",
40+
"description": "Executable name or path for the solver."
41+
},
42+
"version": {
43+
"type": "string",
44+
"description": "Argument passed to the solver to obtain its version string."
45+
},
46+
"minVersion": {
47+
"type": "string",
48+
"description": "Minimum acceptable version string or date for the solver."
49+
},
50+
"socketClass": {
51+
"type": "string",
52+
"description": "Fully-qualified Java class name for the socket implementation."
53+
},
54+
"translatorClass": {
55+
"type": "string",
56+
"description": "Fully-qualified Java class name for the translator implementation."
57+
},
58+
"handlerOptions": {
59+
"type": "array",
60+
"description": "Options controlling handler behaviour.",
61+
"items": {
62+
"type": "string"
63+
},
64+
"uniqueItems": true,
65+
"minItems": 0
66+
},
67+
"delimiters": {
68+
"type": "array",
69+
"description": "List of line delimiters used to parse solver output.",
70+
"items": {
71+
"type": "string"
72+
},
73+
"minItems": 1,
74+
"uniqueItems": true
75+
},
76+
"handlers": {
77+
"type": "array",
78+
"description": "Ordered list of fully-qualified Java handler class names used to translate or postprocess SMT terms.",
79+
"items": {
80+
"type": "string"
81+
},
82+
"minItems": 1,
83+
"uniqueItems": false
84+
},
85+
"preamble": {
86+
"type": "string",
87+
"description": "Resource path, file path, or URL of the SMT preamble to be used with the solver."
88+
}
89+
90+
},
91+
"required": [
92+
"name",
93+
"command"
94+
],
95+
"additionalProperties": false
96+
}
97+
},
98+
"examples": [
99+
{
100+
"Z3": {
101+
"params": "-in -smt2",
102+
"timeout": -1,
103+
"name": "Z3",
104+
"info": "Z3 solver by Microsoft.",
105+
"command": "z3",
106+
"version": "--version",
107+
"handlers": [
108+
"de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler",
109+
"de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler"
110+
],
111+
"handlerOptions": [
112+
"getUnsatCore"
113+
]
114+
}
115+
}
116+
]
117+
}

0 commit comments

Comments
 (0)