Extend Solver Independent SMTLib2 Parser/Generator#436

Draft

baierd wants to merge 220 commits intomasterfrom extend-solver-independent-smtlib2-parser-generator

+38,034-357

Commits on Aug 20, 2023

added BooleanLogger
Janelle
committed

Commits on Aug 23, 2023

connected BooleanLogger to Main.java
Janelle King
committed

Commits on Aug 28, 2023

changed BooleanLogger to Generator, added StringBuilder
Janelle King
committed

Commits on Sep 2, 2023

Added Generator to SolverContextFactory as cmdline option
Janelle King
committed

Commits on Sep 3, 2023

Updated Generator.logNot
Janelle King
committed

Commits on Sep 4, 2023

Introduced new Structure for Logging in Generator
Janelle King
committed

Commits on Sep 5, 2023

Cleaned up Code
Janelle King
committed
Moved logging of constraints from solver to prover
Janelle King
committed
Fixed double entries of "declare-const"
Janelle King
committed

Commits on Sep 14, 2023

Added Boolean Equivalence and And
Janelle King
committed
Added more Boolean Operator Functions
Janelle King
committed
Added logMakeTrue and logMakeFalse
Janelle King
committed

Commits on Sep 15, 2023

Added logOr for Collections
Janelle King
committed
Added logOr for Collections
Janelle King
committed
Added makeNumber, makeVariable, add and equals for Numerals
Janelle King
committed

Commits on Sep 23, 2023

New class RecursiveString instead of Triple for in-place-evaluation
Janelle King
committed
added log functions for make functions for numbers
Janelle King
committed

Commits on Sep 28, 2023

fixed types of declare-const
Janelle King
committed

Commits on Sep 30, 2023

added logSum to Generator
Janelle King
committed

Commits on Oct 6, 2023

added logSubtract, logDivide, logModulo, logModularCongruence to Generator
Janelle King
committed

Commits on Oct 7, 2023

added logMultiply and logDistinct to Generator
Janelle King
committed
fixed logMakeVariable, finished Integer theory, added logMakeBitVector and logEqualBV to Generator
Janelle King
committed

Commits on Oct 9, 2023

fixed logMakeBitVector
Janelle King
committed

Commits on Oct 11, 2023

fixed BVEquals, refactored Generator, added more BV functions
Janelle King
committed
added several Bitvector functions
Janelle King
committed
finished Bitvector functions
Janelle King
committed

Commits on Oct 13, 2023

fixed logBVEqual and logBVDistinct in BitvectorGenerator
Janelle King
committed
added ArrayGenerator
Janelle King
committed

Commits on Oct 16, 2023

added UFGenerator
Janelle King
committed
fixed bugs for BitVec and UF
Janelle King
committed

Commits on Oct 20, 2023

Backup Parser
Janelle King
committed

Commits on Oct 21, 2023

working draft parser
Janelle King
committed
added parser operations for Int and Bool
Janelle King
committed

Commits on Oct 22, 2023

finished Boolean Parser
Janelle King
committed
fixed and finished Numeral Parser
Janelle King
committed

Commits on Oct 23, 2023

added and finished BitVector Parser
Janelle King
committed
fixed BitVector Parser
Janelle King
committed
added Array Parser
Janelle King
committed

Commits on Oct 24, 2023

finished Array Parser, updated operands structure
Janelle King
committed
added and finished UF Parser
Janelle King
committed

Commits on Oct 28, 2023

fixed bugs in array and bitvector
Janelle King
committed

Commits on Oct 29, 2023

added define-fun to parser
Janelle King
committed

Commits on Nov 1, 2023

Backup
Janelle King
committed
Fixed Generator Modifier
Janelle King
committed
Added UnitTest for BooleanGenerator
Janelle King
committed

Commits on Nov 2, 2023

Fixed addConstraint
Janelle King
committed

Commits on Nov 3, 2023

Laptopwechsel
Janelle
committed
Fixed nested AND for Booleans, added NumeralGeneratorTest
Janelle King
committed
added more NumeralGeneratorTests
Janelle King
committed

Commits on Nov 4, 2023

Finished NumeralGenerator test
Janelle King
committed

Commits on Nov 5, 2023

Added BitVecGenerator test
Janelle King
committed
Changed Constructors of Models, Provers and SolverContexts to accept FormulaManagers instead of FormulaCreators
Janelle King
committed

Commits on Nov 6, 2023

Backup Model
Janelle King
committed
Fixed UFGenerator
Janelle King
committed

Commits on Nov 7, 2023

Fixed Modelparsing
Janelle King
committed

Commits on Nov 10, 2023

Backup to transfer to other Laptop
Janelle King
committed
connected Parser with SolverFactory and Prover
Janelle King
committed

Commits on Nov 12, 2023

Backup fixes in Generator
Janelle King
committed

Commits on Nov 13, 2023

Created Exceptions
Janelle King
committed
Finished BitvectorGeneratorTest
Janelle King
committed
added "let" expressions to Parser
Janelle King
committed
added ArrayGeneratorTest
Janelle King
committed

Commits on Nov 14, 2023

added UFGeneratorTest
Janelle King
committed
finished UFGeneratorTest
Janelle King
committed
added BooleanParserTest
Janelle King
committed
fixed Arrays - again
Janelle King
committed

Commits on Nov 15, 2023

finished ArrayParserTest
Janelle King
committed

Commits on Nov 17, 2023

fixed SpotBugs bugs
Janelle King
committed

Commits on Nov 18, 2023

Refactoring, tested with Arrays
Janelle King
committed
Backup ivy configs
Janelle King
committed
Backup ivy configs without cs
Janelle King
committed

Commits on Nov 20, 2023

Clean up Antlr4 dependency and add to classpath/Intellij config
BaierD
committed
Format project and add serial implementation in needed classes
BaierD
committed
for pull
Janelle King
committed
for pull
Janelle King
committed
for pull
Janelle King
committed

Commits on Nov 21, 2023

refactoring
Janelle King
committed
Fix publish scripts for Princess fat jar
BaierD
committed
Add UnnecessaryParentheses suppression to SMTLIB2 parser
BaierD
committed
added princess dependency
Janelle King
committed
Process
Janelle King
committed

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