Extend Solver Independent SMTLib2 Parser/Generator #436

baierd · 2025-02-17T17:17:21Z

This PR extends JavaSMT with an independent SMTLib2 parser/generator layer.
Every solver can use the layer to generate or parse SMTLib2, independent of their own implementation.
The parsing directly uses the API of the solver.
Generating tracks all API usage independently into SMTLib2.

Additionally, we offer a complete solver-independent layer, that is usable with no solver installed. This layer can generate SMTLib2, but also parse SMTLib2 to manipulate the given formula.

Ideally, we also want to support usage of the solvers binaries with SMTLib2 directly. This has been tested for Princess, but has not been implemented for all solvers. My suggestion would be to remove/extract it from this PR and work on it separately.

TODO:

Add a full visitor implementation for the solver-independent layer.
Transform the layer into a delegate.
Add appropriate options for the generator/parser.
Check if its possible to clean up the auto-generated files from ANTLR, or generate them when building the project (similar to the other auto-generated files).

DavidGalllob · 2025-04-03T12:40:48Z

A problem within JavaSMT is that it allows only one single assert in an smt2 String. This needs to be corrected to support all Strings. Momentarily the Generator can be used as a workaround as it builds Strings with only one assert statement.

…E CHANGED SOON! -added new test

… to Floating-Points as Strings

baierd · 2025-04-15T19:54:27Z

@DavidGalllob please do not force-push! Force-push rewrites the history and can lead to conflicts locally!

Also, please do not resolve threads opened by others, as it is hard to confirm that changes have resolved the issues when they are not shown anymore!

baierd

Please take a look at the marked code segments.

Additionally, please try to add some documentation in appropriate locations to make sure that your additions are maintainable in the future.

baierd · 2025-04-15T19:56:21Z

src/org/sosy_lab/java_smt/solvers/SolverLess/DummyType.java

+public class DummyType {
+  /** This class ensures Type-safety for DummyFormulas. */
+  private int bitvectorLength;
+


This class is severely overloaded, hard to maintain, massively increases overhead and should be refactored into the appropriate type-classes!

Also, why not simply use the FormulaType class and its subclasses?

baierd · 2025-04-15T19:58:06Z

src/org/sosy_lab/java_smt/solvers/SolverLess/DummyType.java

+
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+
+@SuppressWarnings({"all", "overrides"})


Please never use the all suppression. Also, the warnings you got here were correct and told you problems that should be resolved! See the other comment in this class.

baierd · 2025-04-15T19:58:56Z

src/org/sosy_lab/java_smt/solvers/SolverLess/DummyFunction.java

+  private DummyType returnType;
+  private List<DummyType> argumentTypes;
+
+  public DummyFunction() {}


Why not use the constructor?

Making this class (and most others in solverless) immutable would reduce error-prone use of methods and known issues of mutability.

baierd · 2025-04-15T20:00:05Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SMTLIB2Formula.java

+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+
+@SuppressWarnings({"StringCaseLocaleUsage", "rawtypes", "Immutable"})


Same as for the type class of this package.

baierd · 2025-04-15T20:00:22Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SMTLIB2Formula.java

+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+
+@SuppressWarnings({"StringCaseLocaleUsage", "rawtypes", "Immutable"})
+public class SMTLIB2Formula


This class is severely overloaded, hard to maintain, massively increases overhead and should be refactored into the appropriate formula-classes!

baierd · 2025-04-15T20:01:59Z

src/org/sosy_lab/java_smt/solvers/SolverLess/DummyEnv.java

+
+package org.sosy_lab.java_smt.solvers.SolverLess;
+
+public class DummyEnv {}


Whats the purpose of this class?

baierd · 2025-04-15T20:02:13Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessFloatingPointFormulaManager.java

+import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager;
+
+@SuppressWarnings("StringSplitter")


Please address the warnings instead of suppressing them.

baierd · 2025-04-15T20:03:32Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessFormulaCreator.java

+
+  @Override
+  public <R> R visit(FormulaVisitor<R> visitor, Formula formula, SMTLIB2Formula f) {
+    return null;


Never return null!
Also, you are missing a core implementation here for the functionality of the independent SMTLib2 layer.

baierd · 2025-04-15T20:05:11Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessFloatingPointFormulaManager.java

+    if (pTargetType.isRationalType()) {
+      return new SMTLIB2Formula(new DummyType(DummyType.Type.RATIONAL));
+    }
+    return null;


Never return plain null for known reasons.
This looks like a switch-case expression.

baierd · 2025-04-15T20:05:24Z

src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessFloatingPointFormulaManager.java

+
+  @Override
+  protected SMTLIB2Formula remainder(SMTLIB2Formula pParam1, SMTLIB2Formula pParam2) {
+    return null;


Missing implementation?

Janelle King and others added 30 commits November 22, 2023 13:27

refactored ParserFormula

f7d8914

princess-all.jar with modified manifest added

7248ad9

refactored

a021e00

refactored

d877043

refactored

e33c7f0

first eval results

ef0e3a6

fixed bugs

d832fdb

Merge branch 'main' of github.com:KJanelle/java-smt into main

7298d8a

xml file

ec4f43e

fixed usage of Generator

2c3ae57

Merge branch 'main' of github.com:KJanelle/java-smt into main

7ce18dd

fixed usage of Generator

77d7a7c

fixed usage of Generator

b9ddfc9

fixed usage of Generator

0a4ca35

fixed usage of Generator

9f82157

evaluation tables

568d607

improved coverage of UnitTests

e8430eb

improved coverage of UnitTests Parser

de862c2

Added model tests

96da4b2

made keyword an ENUM

b1f260f

made methodToEvaluate in Generator "Optional"

4579f7f

Bugfix

8ef60d4

comments and test coverage

95af1b9

final refactoring

debbf48

deleted princess_all-2023-06.jar

fa5efe2

Readd missing checkstyle config and remove Princess binary

92d5d7a

Revert .idea and .gitignore to previous states

8e6673d

Fix idead Intellij JavaSMT setup (without local paths)

e2978b0

Merge branch 'solver-independent-smtlib2-parser-generator' into PR

c0e0ab3

Fixed merge issues.

3927dbe

DavidGalllob added 3 commits April 3, 2025 12:00

- modified gitignore to ignore scripts

48646f3

-fixed wrong Generating of some string functions.

a6bd296

-fixed tests

2ba04eb

DavidGalllob added 20 commits April 3, 2025 15:58

-changed solvers to native for benchmark

785ccd1

- Benchmark now only supports Z3

9167122

- Implemented support for Mathsat and Z3 in my Benchmark class

9d97dd2

- implemented support for BITWUZLA in Benchmark

f2d4b80

- refactored

bab58f1

- fixed wrong variable usage in benchmark class

01732d2

- updated unsupported Operation Exception in a visitor Method.

40bea36

- updated unsupported Operation Exception in a visitor Method.

0c1c6c6

-fixed tests

ed2208f

-refactorings

a909475

-added a test and changed Generator to use Set-logic all. THIS MUST B…

bf1cf27

…E CHANGED SOON! -added new test

- benchmark now compares the results.

4451895

- Implemented fp generating correctly and added new tests

d72a024

- fixed some intense bugs

0a8499b

-fixed wrong equation usage in fps

56baf31

-fixed a bug where wrong "" were set in regex

47801ba

-added new tests

5fe98a8

removed unsupported Test

9de0813

reformated

ce8e2b7

fixed tests

6b18557

DavidGalllob force-pushed the extend-solver-independent-smtlib2-parser-generator branch from 95f9851 to 6b18557 Compare April 13, 2025 09:43

DavidGalllob added 2 commits April 14, 2025 10:27

fixed a crucial implementation mistake, where all numbers were handed…

4bf4133

… to Floating-Points as Strings

fixed a crucial implementation mistake, where all numbers were handed…

4617374

… to Floating-Points as Strings

baierd commented Apr 15, 2025

View reviewed changes

baierd dismissed DavidGalllob’s stale review via 4617374 April 16, 2025 09:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extend Solver Independent SMTLib2 Parser/Generator #436

Extend Solver Independent SMTLib2 Parser/Generator #436

baierd commented Feb 17, 2025 •

edited by DavidGalllob

Loading

DavidGalllob commented Apr 3, 2025

baierd commented Apr 15, 2025

baierd left a comment

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025

baierd Apr 15, 2025


		import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;

		@SuppressWarnings({"all", "overrides"})


		package org.sosy_lab.java_smt.solvers.SolverLess;

		public class DummyEnv {}

Extend Solver Independent SMTLib2 Parser/Generator #436

Are you sure you want to change the base?

Extend Solver Independent SMTLib2 Parser/Generator #436

Conversation

baierd commented Feb 17, 2025 • edited by DavidGalllob Loading

DavidGalllob commented Apr 3, 2025

baierd commented Apr 15, 2025

baierd left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

baierd commented Feb 17, 2025 •

edited by DavidGalllob

Loading