4 open source projects by Gbury

An ocaml implementation of variants of the simplex and branch&bound algorithms for satisfiability.

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

A small library to output memory graph for ocaml values

A modular sat/smt solver with proof output.