SMLP 1.1.1

Notable Changes:

• Support for installing SMLP via pip on Linux and MacOS. The package is called smlptech and available on PyPI: https://pypi.org/project/smlptech/
  • utils/poly: Prepare mac support by @fbrausse in #54
  • smlp pip package build and test by @mdmitry1 in #53
  • Changed wheel name to smlptech by @mdmitry1 in #74
  • Note that the MacOS version currently cannot be built out-of-the-box from the master branch, we're working on integrating it.
• The pip package installs the command smlp providing the full functionality of this version of SMLP
  • Use relative imports everywhere in src/smlp_py and conditionally in run_smlp.py by @fbrausse in #56
  • Move poly from smlp to smlp.core by @fbrausse in #60
• A great tutorial containing applications and examples on how to use SMLP for a variety of concrete problems, kindly contributed by @mdmitry1:
  • SMLP tutorial by @mdmitry1 in #49
• Various fixes:
  • regression tests: use relative -solver_path to mathsat by @fbrausse in #63
  • Fixing bug in loading saved models (Fixes issue #69) by @zurabksmlp in #71

Full Changelog: v1.0.1...v1.1.1

SMLP 1.0.2

• Added wheel support for Linux
  Installation:

pip3.11 install https://github.com/SMLP-Systems/smlp/raw/refs/heads/master/dist/smlp-0.1.0-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl

• Added full screen support Docker container server
  Installation:

docker pull mdmitry1/python311-dev:latest

SMLP 1.0.1

What's Changed

• Added Docker support for Intel, AMD and Mac series M CPU's
• Added pip install support for Linux

SMLP 1.0.0

What's Changed

• Incorporate changes from cav2024 branch in #8
• Bug fix for polynomial terms in #43, #45
• Cleanups (#42, #44, #45)

Full Changelog: poly-v0.10.1-r1...v1.0.0

v0.10.1-r1

poly-v0.10.1-r1

mrmr features

poly-v0.10.1

• fix problem related to missing bounds

poly-v0.10.0

• document python module build
• generate setup.py by meson
• make mpfr dependency respect the "static" option
• py: support domain as container, domain-component as pair; add set_loglvl() and simplify opt
• fix infix parser for numeric constant at end of the input
• require -R for Pareto search
• py: allow instantiation of pre_problem and domain
• simplify creation of expr2
• restore support for gcc-11 and clang >= 11
• include libiv sources + update build instrs
• -O now does not affect alpha, beta or eta
• add missing include/smlp
• fix fallback def of isatty()
• print backtrace on USR1
• add (yet unused) gearopt iterable
• default symbol visibility and -rdynamic

poly-v0.9.0

• fix computation of final bounds for optimum
• catch more cases worth logging
• move bop/uop to expr2; add infix support for "^"
• move more ad-hoc unrolled functions to API: and, or, not, div_cnst
• begin parsing cvc5/cvc4/z3 inexact or algebraic assignments in models
• add reals and algebraics
• introduce A values to cnst2
• parameterize how literals are unrolled
• prepare to librarify
• add initial version of Pareto
• cleanup
• first version Python API
• add some local things to .gitignore
• move init.py + separate -static* flags for exe & lib
• add version + fix boost dep for static build

poly-v0.8.0

• override Z3's buggy SIGINT handler (after 100ms)
• add -T LO:INC:HI option format
• rename -O OUT-BNDS to -O OBJ-BNDS for uniformity
• disentangle critical points and fallback solver from ival solver
• obtaining all solutions to a problem is now handled in a lazy manner
• splitting intervals no longer skips space between midpoint and next double
• critical points solver only handles linear derivatives
• add option -o OBJ-SPEC supporting arbitrary expressions or the expression
  'Pareto(E1,E2,...)' containing such expressions (Pareto optimization is not
  implemented, yet)
• minor improvements/fixes:
  • simplifier deals with double-neg and unnecessary conj/disj
  • logging
  • fix handling option -c auto
  • report and error on surplus unused arguments
  • empty sequence of solvers
  • ext-solver outputs time to solve
  • print the named outputs (if any)
  • sequence of variables in models is sorted now
  • optimize_EA properly forwards strictness info to obj-range
  • check that none of the objectives is constant on the domain

poly-v0.7.0

• moved old options -1 and -c to -C gen-obj and -C clamp
• introduced structured and colored log output for clarity:
  • verbosity controlled by new option -v
  • log levels are: none, error, warn, info, note, debug; default: note
  • color controlled by repurposed option -c
  • solvers are more verbose in what they are doing
• support reading options from envvar SMLP_OPTS (if set); parsing the envvar
  string is done by the shell (envvar SHELL if set, 'sh' otherwise), as if
  SMLP was invoked by

    ${SHELL} -c 'exec "$0" ${SMLP_OPTS} "$@"' smlp arguments...