sop-satisfier: Check satisfiability of expressions on natural numbers

[ bsd2, library, solver, symbolic-arithmetic ] [ Propose Tags ] [ Report a vulnerability ]

Expression satisfier on natural numbers. . It can reason about expressions contatining addition and multiplication. It also provides limited support of exponentiations and subtraction.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.3.4.5
Change log CHANGELOG.md
Dependencies base (>=4.13 && <5), containers (>=0.6.2.1 && <0.8), transformers (>=0.5 && <0.7) [details]
Tested with ghc ==8.8.4, ghc ==8.10.7, ghc ==9.0.2, ghc ==9.2.8, ghc ==9.4.8, ghc ==9.6.6, ghc ==9.8.4, ghc ==9.10.1, ghc ==9.12.1
License BSD-2-Clause
Author Aleksandr Pokatilov <pokatilov0802@gmail.com>
Maintainer QBayLogic B.V. <devops@qbaylogic.com>
Category Solver, Symbolic Arithmetic
Source repo head: git clone https://github.com/clash-lang/sop-satisfier
Uploaded by ChristiaanBaaij at 2025-06-07T14:40:00Z
Distributions
Downloads 0 total (0 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2025-06-07 [all 1 reports]

Readme for sop-satisfier-0.3.4.5

[back to package description]

SoP Satisfier

Kind of SMT solver with only Non-linear Natural Arithmetic.

Library with an SMTlib like interface to declare and assert SoP (kind of) expressions.

Interface:

  • declare - to declare expression to the state
  • assert - to assert that expression holds in the state
  • unify - to get a list of expressions that need to hold for the given expression to hold (only equalities are supported)
  • range - to get a range (a pair of minimum and maximum possible values) of expression