Extend Solver Independent SMTLib2 Parser/Generator #436

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

TODO: Description

…rator

…r and logEqualBV to Generator

- minor bugfixes

…SMTLIb2 Strings when generating them

-FloatingPoints can now log values.

…and once parsed and regeneratated and then given to Z3 as part of an evaluation.

…t added to the variables Hashmap in the Visitor.java

-bugfix where all String tests would evaluate negative in Parser Test

-introduced new Type, which holds all important information for handling formulaTypes

… generate them...

-deleted many methods that had no usages

baierd

@DavidGalllob
I found some points to address.
Also, please run ant all-checks and fix all issues found.
The checks tell you several problems still present.

src/org/sosy_lab/java_smt/api/FloatingPointRoundingMode.java

src/org/sosy_lab/java_smt/basicimpl/BinaryModel.java

baierd · 2025-02-17T17:32:28Z

src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java

@@ -482,15 +483,17 @@ public int getLength(BitvectorFormula pNumber) {
  public final BooleanFormula distinct(List<BitvectorFormula> pBits) throws GeneratorException {
    // optimization
    if (pBits.size() <= 1) {
+      BooleanFormula nativeTrue = bmgr.makeTrue();


Since the results for true and false are immutable and static, you most likely don't need the changes in this class.

Ich habe in dieser Klasse überhaupt keine Änderungen vorgenommen. Soll ich dennoch dieses Anliegen beheben?

baierd · 2025-02-19T14:53:24Z

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -135,6 +172,9 @@ protected TFormulaInfo makeNumberImpl(

  protected static boolean isNegativeZero(Double pN) {
    Preconditions.checkNotNull(pN);
+    if(Generator.isLoggingEnabled()){
+      throw new GeneratorException("Logging isNegativeZero ist not supported yet");


Neg zero is quite important for FP. You should try to include it.

Das Problem ist, dass SMT-LIB nur isZero unterstützt. Es gibt keine eigene Funktion für isNegativeZero, deshalb wird hier diese Exception geworfen. Ich kann gerne isZero verwenden, was jedoch nicht äquivalent ist.

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

src/org/sosy_lab/java_smt/basicimpl/FloatingPointGenerator.java

src/org/sosy_lab/java_smt/basicimpl/FunctionEnvironment.java

src/org/sosy_lab/java_smt/basicimpl/StringGenerator.java

Janelle added 30 commits August 20, 2023 15:19

added BooleanLogger

feb46c3

connected BooleanLogger to Main.java

b2a4ea7

changed BooleanLogger to Generator, added StringBuilder

133d125

Added Generator to SolverContextFactory as cmdline option

c267bf4

Updated Generator.logNot

1cb653f

Introduced new Structure for Logging in Generator

25a7899

Cleaned up Code

b84c06f

Moved logging of constraints from solver to prover

6c064b4

Fixed double entries of "declare-const"

f97b344

Added Boolean Equivalence and And

7f2ceec

Added more Boolean Operator Functions

6fbd040

Added logMakeTrue and logMakeFalse

425b8b7

Added logOr for Collections

c793057

Added logOr for Collections

7f4cf43

Added makeNumber, makeVariable, add and equals for Numerals

325a713

New class RecursiveString instead of Triple for in-place-evaluation

d97e384

added log functions for make functions for numbers

cf64938

fixed types of declare-const

9656d5c

added logSum to Generator

c3d6b2e

added logSubtract, logDivide, logModulo, logModularCongruence to Gene…

b462f58

…rator

added logMultiply and logDistinct to Generator

b6a06be

fixed logMakeVariable, finished Integer theory, added logMakeBitVecto…

ffcac71

…r and logEqualBV to Generator

fixed logMakeBitVector

423b5a1

fixed BVEquals, refactored Generator, added more BV functions

d6a4d8e

added several Bitvector functions

8f11c85

finished Bitvector functions

cefbf20

fixed logBVEqual and logBVDistinct in BitvectorGenerator

6ba0db1

added ArrayGenerator

0d0112d

added UFGenerator

143aa5d

fixed bugs for BitVec and UF

3d2cf82

DavidGalllob and others added 24 commits December 8, 2024 17:10

-added SolverLess FormulaManagers and dummytypes

2c017fd

-added SolverLess FormulaManager (not working correctly yet)

13ad326

-added support for floatingPoints in the solverless Solver

4d7fb87

-Fixed bugs where Arrays and Integers couldn't be created correctly

896dc9b

- Bitvectors now can be parsed without a Solver.

f9a3d3a

-changed formula creation and recognization in Formulacreator

b16cf18

-added UF Manager in Solverless Solver

5e0c515

- minor bugfixes

-added correct creation of nested arrays in the Solverless Solver

df52e4e

Clean up registering of SMTLIB2 Int or Real number in the generator

a529138

Add precondition and some simplifications to recursive evaluation of …

c03a3f5

…SMTLIb2 Strings when generating them

Call solvers only once when logging SMTLib2 generation independently

bd7cdd6

Solverless Sovler now works with all types (nearly correctly) except UFs

1924ffb

Refactored Solverless Package name and created evaluation tests.

479a14d

-added small tests

f424513

-added FloatingPointTests

f74c2cd

-FloatingPoints can now log values.

Created a test environment where a String will be put directly to Z3 …

6cb380a

…and once parsed and regeneratated and then given to Z3 as part of an evaluation.

fixed a problem where "makeString" would not work because they weren'…

3f627ef

…t added to the variables Hashmap in the Visitor.java

-added basic functions for UFManager

948eacd

-bugfix where all String tests would evaluate negative in Parser Test

-added support for Bitvectors in UFs

8c45e8c

-added full Support for Uninterpreted Functions in Solverless Solver

9f1b5cd

-introduced new Type, which holds all important information for handling formulaTypes

bugfixes

6f72c82

-Solverless now can work with Floating Point formulas but still can't…

0e12e7d

… generate them...

-Solveless now can correctly Generate FloatingPoints

e4e981d

-Refactorings

1da6680

-deleted many methods that had no usages

baierd assigned DavidGalllob Feb 17, 2025

Bring ivysettings in line with main branch

7cd9f6f

baierd commented Feb 19, 2025

View reviewed changes

DavidGalllob added 3 commits February 20, 2025 14:35

Refactorings.

a44c8ec

minor refactorings

c28fd49

minor refactorings

bc9e8bc

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

baierd left a comment

baierd Feb 17, 2025

DavidGalllob Feb 20, 2025

baierd Feb 19, 2025

DavidGalllob Feb 20, 2025

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

baierd left a comment

Choose a reason for hiding this comment

baierd Feb 17, 2025

Choose a reason for hiding this comment

DavidGalllob Feb 20, 2025

Choose a reason for hiding this comment

baierd Feb 19, 2025

Choose a reason for hiding this comment

DavidGalllob Feb 20, 2025

Choose a reason for hiding this comment