package theo

  1. Overview
  2. Docs
A BDD library with theory support

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

  1. J
    Jérôme Vouillon

Maintainers

  1. J
    Jérôme Vouillon

Sources

theo-0.1.0.tbz
sha256=bdaa3e26ec5ab84a6a378693cdc4d5ca3470b52c9a36715e7ccb6543100281ed
sha512=9d3ac06b7dc9f154ac987cc376af5725bdbce326f245d5036ff54412eeae9edbca7cbeec60dbec3451122396a74699c9befcd238b47d4492334b86730e178e76

doc/CHANGES.html

Changelog

0.1.0 (2026-07-16)

Initial release.

  • Core BDD engine with hash-consing and canonical negative-edge form
  • Boolean operations: AND, OR, NOT, IMPLIES, EQUIV, XOR, and exists/forall quantifiers
  • Pluggable theory support over linear orders and equality (booleans, strings, integers, semantic versions), with a Combine functor to mix theories
  • restrict operation for partial evaluation, and constraint introspection via pattern matching
  • Irredundant sum-of-products (Minato-Morreale) computation
  • Property-based test suite