package encoding

  1. Overview
  2. Docs
Smt encoding library

Install

Dune Dependency

Authors

Maintainers

Sources

v0.0.4.tar.gz
md5=79eace174880a378ca634f3b6d6dca2b
sha512=c244e75b833cd5eae204749e6049003fb0ede5f202cd18219de8d3a771fc40475b2cc865e9b49f7694696c67389e5b5fe7d5bee415f5e6439ee7ff960ff3c9e0

CHANGES.md.html

v0.0.4

  • Adds Arthur's clz and ctz implementations for i64s

  • Completes missing eval_numeric operations

  • Adds more tests to increase code coverage

  • Adds extend_ixx to lexer

  • Adds colibri2 mappings

  • Fixes hash-consing in 72eeb6f

  • Rename declare-fun to let-const

  • Rotate_left and rotate_right operators

  • Print floats in OCaml syntax (Closes #49)

v0.0.3

  • Improve bitv creation interface

  • Add naive hash-consing of expressions

  • Add Ceil and Floor FPA operators

  • Start migrating inline tests to standard tests

  • No simplifier on batch solver

v0.0.2

  • Support for bv8

  • Refactor optimizer interface

  • Fixes batch solver in e061344

  • Adds default simplifier in z3 leading to great performance gains

  • Adds logic configuration option to mk_solver

  • Fixes pp function in 11476fb

  • Adds ematching and timeout parameters

  • Improves documentation

  • Relax ocaml compiler constraint to >= 4.14.0

v0.0.1

Initial release