A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
-
Updated
May 13, 2026 - SMT
#
congruence-closure
Here are 6 public repositories matching this topic...
My first SMT solver (only QF_UF)
satisfiability-modulo-theories logic-programming cnf learning-by-doing sat-solver smt-solver dpll tseitin-transformation cdcl logical-reasoning congruence-closure backjumping cdcl-t sat-solving qf-uf diy-smt
-
Updated
Jul 8, 2020 - Haskell
Production-ready decision procedure solver implementing congruence closure for satisfiability checking in the union of first-order theories (Equality, Lists, Arrays). Based on Bradley & Manna algorithms with 571 passing tests.
java lists equality arrays smt-solver formal-verification automated-reasoning satisfiability congruence-closure theory-solver decision-procedures bradley-manna university-verona
-
Updated
Jan 31, 2026 - Java
This project is focused on implementing and visualizing the Congruence Closure (CC) Algorithm in a step-by-step manner . The primary objective is to develop an interactive and educational tool that simplifies understanding of the algorithm’s mechanics.
-
Updated
Dec 23, 2024 - Python
Lazy DPLL(T) SMT solver in pure Standard ML over the vendored sml-sat DPLL core: EUF (congruence closure) + LRA (Fourier-Motzkin). Dual-compiler MLton + Poly/ML.
theorem-proving sml standard-ml mlton smt smt-solver polyml congruence-closure dpll-t fourier-motzkin
-
Updated
Jun 22, 2026 - Standard ML
Improve this page
Add a description, image, and links to the congruence-closure topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the congruence-closure topic, visit your repo's landing page and select "manage topics."