Extend Solver Independent SMTLib2 Parser/Generator#436

Draft

baierd wants to merge 331 commits intomasterfrom

extend-solver-independent-smtlib2-parser-generator

This pull request is big! We're only showing the most recent 250 commits

Commits on Nov 22, 2023

refactored ParserFormula
Janelle King
committed
princess-all.jar with modified manifest added
Janelle King
committed

Commits on Nov 23, 2023

refactored
Janelle King
committed
refactored
Janelle King
committed
refactored
Janelle King
committed

Commits on Nov 24, 2023

first eval results
Your Name
committed

Commits on Nov 26, 2023

fixed bugs
Janelle King
committed
Merge branch 'main' of github.com:KJanelle/java-smt into main
Janelle King
committed

Commits on Nov 27, 2023

xml file
Your Name
committed
fixed usage of Generator
Janelle King
committed
Merge branch 'main' of github.com:KJanelle/java-smt into main
Janelle King
committed
fixed usage of Generator
Janelle King
committed
fixed usage of Generator
Janelle King
committed
fixed usage of Generator
Janelle King
committed
fixed usage of Generator
Janelle King
committed

Commits on Nov 28, 2023

evaluation tables
Your Name
committed

Commits on Nov 29, 2023

improved coverage of UnitTests
Janelle King
committed

Commits on Nov 30, 2023

improved coverage of UnitTests Parser
Janelle King
committed

Commits on Dec 18, 2023

Added model tests
Janelle King
committed
made keyword an ENUM
Janelle King
committed
made methodToEvaluate in Generator "Optional"
Janelle King
committed
Bugfix
Janelle King
committed
comments and test coverage
Janelle King
committed
final refactoring
Janelle King
committed
deleted princess_all-2023-06.jar
Janelle King
committed

Commits on Dec 19, 2023

Readd missing checkstyle config and remove Princess binary
BaierD
committed
Revert .idea and .gitignore to previous states
BaierD
committed
Fix idead Intellij JavaSMT setup (without local paths)
BaierD
committed

Commits on Jan 13, 2024

Commits on Apr 22, 2024

Commits on Apr 23, 2024

Commits on May 2, 2024

ParserGenerator: Add "set-logic" command only when the SMTLIB2 string is extracted, and not when the generator is initialized.
daniel-raffler
committed

Commits on Nov 3, 2024

[Unstable Floating Points not useable yet!]
DavidGalllob
committed

Commits on Nov 4, 2024

Commits on Nov 5, 2024

Commits on Nov 6, 2024

Merge branch 'solver-independent-smtlib2-parser-generator' into extend-solver-independent-smtlib2-parser-generator
BaierD
committed

Commits on Nov 12, 2024

Commits on Nov 13, 2024

-changed the Constructor of the Visitor.java class so that it now takes a FloatingPointFormulaManager
DavidGalllob
committed

Commits on Nov 19, 2024

-added parsing of Floating-Points which are in the Standard Format e.g. (_ FloatingPoint 11 23) in Visitor.java
DavidGalllob
committed

Commits on Nov 20, 2024

-Visitor.java should now be able to recognize all Floating Points definition variant, BUT Hexadecimal (incoming)
DavidGalllob
committed

Commits on Nov 21, 2024

-removed entire FloatingPoint implementation in smtlibv2.g4 file as it is redundant, because handling is done in Visitor.java without the new nodes.
DavidGalllob
committed

Commits on Nov 22, 2024

Commits on Nov 23, 2024

-added parsing of Strings in the Visitor.java class. (Not Tested yet)
DavidGalllob
committed

Commits on Nov 26, 2024

-introduced FloatingPoints and Strings as Sorts in the Generator.java
DavidGalllob
committed

Commits on Nov 27, 2024

Commits on Nov 28, 2024

Commits on Nov 29, 2024

-added basic FloatingPoint Operations in the FloatingPointGenerator class
DavidGalllob
committed

Commits on Nov 30, 2024

-added FloatingPoints and their operations to the Generator (NOT TESTED)
DavidGalllob
committed

Commits on Dec 2, 2024

-added missing StringOperations
DavidGalllob
committed

Commits on Dec 3, 2024

-added missing logging Operations to the AbstractFloatingPointFormulaManager
DavidGalllob
committed

Commits on Dec 5, 2024

Commits on Dec 6, 2024

-added Dummy classes for Solving (contains errors) unstable
DavidGalllob
committed

Commits on Dec 8, 2024

-added SolverLess FormulaManagers and dummytypes
DavidGalllob
committed

Commits on Dec 11, 2024

-added SolverLess FormulaManager (not working correctly yet)
DavidGalllob
committed

Commits on Dec 13, 2024

-added support for floatingPoints in the solverless Solver
DavidGalllob
committed

Commits on Dec 14, 2024

Commits on Dec 15, 2024

-changed formula creation and recognization in Formulacreator
DavidGalllob
committed

Commits on Jan 2, 2025

-added UF Manager in Solverless Solver
DavidGalllob
committed

Commits on Jan 6, 2025

-added correct creation of nested arrays in the Solverless Solver
DavidGalllob
committed

Commits on Jan 7, 2025

Commits on Jan 11, 2025

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

Commits on Jan 14, 2025

Commits on Jan 16, 2025

-added FloatingPointTests
DavidGalllob
committed

Commits on Jan 18, 2025

Created a test environment where a String will be put directly to Z3 and once parsed and regeneratated and then given to Z3 as part of an evaluation.
DavidGalllob
committed

Commits on Jan 21, 2025

fixed a problem where "makeString" would not work because they weren't added to the variables Hashmap in the Visitor.java
DavidGalllob
committed

Commits on Jan 25, 2025

-added basic functions for UFManager
DavidGalllob
committed

Commits on Jan 26, 2025

-added support for Bitvectors in UFs
DavidGalllob
committed

Commits on Jan 27, 2025

-added full Support for Uninterpreted Functions in Solverless Solver
DavidGalllob
committed

Commits on Feb 3, 2025

bugfixes
DavidGalllob
committed

Commits on Feb 11, 2025

Commits on Feb 12, 2025

-Refactorings
DavidGalllob
committed

Commits on Feb 19, 2025

Bring ivysettings in line with main branch
BaierD
committed

Commits on Feb 20, 2025

Commits on Feb 21, 2025

-fixed all Warnings
DavidGalllob
committed

Commits on Feb 22, 2025

Commits on Feb 25, 2025

Commits on Feb 26, 2025

Format source code (including code by Janelle)
BaierD
committed
Switch ArrayList to List types in return types
BaierD
committed

Commits on Feb 27, 2025

Commits on Feb 28, 2025

Commits on Mar 1, 2025

Commits on Mar 2, 2025

Commits on Mar 4, 2025

-restored all failing tests
DavidGalllob
committed

Commits on Mar 5, 2025

Commits on Mar 6, 2025

Commits on Mar 7, 2025

Commits on Mar 16, 2025

Commits on Mar 19, 2025

Commits on Mar 21, 2025

Commits on Mar 26, 2025

Commits on Mar 31, 2025

Commits on Apr 1, 2025

Commits on Apr 3, 2025

Commits on Apr 5, 2025

Commits on Apr 7, 2025

- Implemented fp generating correctly and added new tests
DavidGalllob
committed

Commits on Apr 11, 2025

Commits on Apr 14, 2025