0.4.4

What's Changed

• more flexible context extension with open expression builders
• special *NoFlat builders for and/or operations

0.4.3

What's Changed

• Change the way of native libraries storing

0.4.2

What's Changed

• Cvc5 solver support for ksmt
• Internalizer optimization
• Downgrade z3 version to 4.11.2

0.4.1

What's Changed

• Z3: upgrade version to 4.12.1 and add support for macOS with aarch64
• Bitwuzla array lambdas
• Portfolio solver
• Multi indexed arrays

0.4.0

Changes

• Evaluator for Fp expressions
• Yices SMT solver
• Simplifying context
• Better Bitwuzla solver support
• Custom expression documentation

0.3.2

Changes

• Bv and fp optimization
• Better expression interning
• KInterpretedValue base class for all inderpreted constants (replacement for KInterpretedConstant marker interface)
• Small changes in KTransformer.transformApp argument types

0.3.1

Bitwuzla

1. Fix fp support on windows (rebuild native lib)
2. Fix Bv values internalization/conversion on windows
3. Fix fma internalization

Z3

1. Construct Fp values from biased exponent since unbiased exponent is sometimes incorrect in Z3
2. Z3 array lambda converter

Core

1. Fp constructors with biased exponent
2. Support uninterpreted sorts in model
3. Fix expression substitution and evaluation in quantifiers
4. Staged ite expression simplification which is required for function app evaluation in a case of recursievly defined functions.
5. Simplify select from array lambda
6. Fix simplification of Bv shifts

Other

1. Check expression ownership context in all API's
2. Check that variables in function interpretations always match declaration arguments

Release 0.3.0

Changes

• Better const creation API in #36
• Parser API in #38
• Roadmap in #39
• Expression checked cast utility in #41
• Expr sort and decl API rework in #43
• Expr simplifier in #45
• Expression printer in #48
• Solver configuration api in #34

Full Changelog: 0.2.1...0.3.0

Release 0.2.1

• Support FP theory in Bitwuzla
• Usage documentation and examples

0.2.0

Run solvers in a separate process