From f7fca5a294e821433c9999325eea14e23ea13664 Mon Sep 17 00:00:00 2001 From: BaierD Date: Mon, 21 Jul 2025 17:31:51 +0200 Subject: [PATCH 1/3] Add UnsatCore support and SL support to README --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 695a7f3c15..c1ac30a063 100644 --- a/README.md +++ b/README.md @@ -52,6 +52,7 @@ JavaSMT can express formulas in the following theories: - Array - Uninterpreted Function - String and RegEx + - Separation Logic (experimental) The concrete support for a certain theory depends on the underlying SMT solver. Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx. @@ -101,6 +102,7 @@ The following features are supported (depending on the used SMT solver): - Multiple independent contexts - Model generation - Interpolation, including tree and sequential structure + - Unsatisfiable core generation - Formula transformation using built-in tactics - Formula introspection using visitors From 638b9ec55f9dd7d073c7a436c77120a2c0144f04 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 30 Jul 2025 17:51:06 +0200 Subject: [PATCH 2/3] Extend README with info about examples and start with solver-independent feature info --- README.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/README.md b/README.md index c1ac30a063..39974120ae 100644 --- a/README.md +++ b/README.md @@ -180,6 +180,32 @@ try (SolverContext context = SolverContextFactory.createSolverContext( } } ``` +You can find several example implementations in the folder `org/sosy_lab/java_smt/example`. +These include examples for the usage of many of JavaSMTs solvers and features, for example: +- AllSatExample: showcasing the usage of the AllSat feature, returning all satisfiable + assignments for an input query. JavaSMT is capable of returning AllSat for many solvers even + without them directly supporting this feature. +- FormulaClassifier: showcases the usage of our formula visitor to classify the logic of an + input SMT file. +- Interpolation: presents how to utilize Craig-, sequential-, and tree-interpolation. +- OptimizationFormulaWeights: shows how the weighting of constraints can be optimized in + optimization solving, helping the solver in finding a result. +- OptimizationIntReal: presents optimization solving for integer and real logics. +- PrettyPrinter: showcases how to parse user-given SMT input into a pretty format. +- SimpleUserPropagator: shows an example of a user propagator, prohibiting variables and/or + expressions from being set to true. This can be used to guide an SMT solver in its + solving process. More examples can be found in the folder `nqueens_user_propagator`. +- SolverOverviewTable: prints out all available SMT solvers, including their theories and + features. This can be used to determine which solvers are available on any machine executing it. + +Furthermore, JavaSMT provides users with additional features available for many solvers: +- Debug-Mode: +- Synchronization: +- Statistics: +- Logging: +- Assumption solving: +- AllSat: +- Formula visitation: ## Authors From c4b5337eae24bd8c24a36b6f4364188350008a84 Mon Sep 17 00:00:00 2001 From: BaierD Date: Thu, 31 Jul 2025 12:28:41 +0200 Subject: [PATCH 3/3] Extend README with info about configurations and solver-independent feature info --- README.md | 40 +++++++++++++++++++++++++++++++++------- 1 file changed, 33 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 39974120ae..d49d6702d0 100644 --- a/README.md +++ b/README.md @@ -199,13 +199,39 @@ These include examples for the usage of many of JavaSMTs solvers and features, f features. This can be used to determine which solvers are available on any machine executing it. Furthermore, JavaSMT provides users with additional features available for many solvers: -- Debug-Mode: -- Synchronization: -- Statistics: -- Logging: -- Assumption solving: -- AllSat: -- Formula visitation: +- Debug-Mode: setting the option `useDebugMode=true`, in the configuration used to create a + `SolverContext`, applies additional checks to catch common usage errors. The checks + performed by this option are solver-sensitive and throw exceptions on operations that + are disallowed by a particular solver. For example, for most solvers, adding a constraint to a + `ProverEnvironment` may only be allowed iff the constraint has been built by the same + `SolverContext` that also created the used `ProverEnvironment`. Violating this rule while in + debug-mode with a solver that does not allow this throws a `IllegalArgumentException` with + information about the problem. +- Synchronization: setting the option `synchronize=true`, in the configuration used to create a + `SolverContext`, all solver actions are synchronized with the owning instance being the + `SolverContext`. This allows concurrent access, but strictly sequentializes all operations. +- Statistics: setting the option `collectStatistics=true`, in the configuration used to create a + `SolverContext`, counts all operations and interactions towards the SMT solver of this context. + These statistics can be access in the `SolverContext`. +- Logging: setting the option `useLogger=true`, in the configuration used to create a + `SolverContext`, logs all solver actions. Logging operations might slow down + usage of JavaSMT though. +- Assumption solving: in case an SMT solver does not support assumption solving natively, we + automatically add this feature seamlessly through a self-developed layer. No difference in usage + can be observed from a users' perspective. +- AllSat: in case an SMT solver does not support assumption solving natively, we + automatically add this feature seamlessly through a self-developed layer. No difference in usage + can be observed from a users' perspective. +- Formula visitation: we allow the inspection, traversal, and modification of formulas through + our formula-visitor, as long as the chosen SMT solver supports this feature. Users can utilize + many pre-built features based on this visitor like + `BooleanFormulaManager.toDisjunctionArgs()`, returning a set of formulas such that a + disjunction over them is equivalent to the input formula, or `FormulaManager. + extractVariablesAndUFs()`, which can be used to extract the names of all free variables and + UFs in a formula. The visitor-pattern can also be used with user-defined operations. + +Many more options are available to configure SMT solvers by setting them in the `Configuration` +given to an `SolverContext`, including SMT solvers native configuration options. ## Authors