From 40e124931cd6b5efc33db907272cf4b1174da0ed Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 26 Sep 2022 21:00:09 -0400 Subject: [PATCH] doc: update readme --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 08dddc8b..1869a654 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Sidekick [![Build](https://github.com/c-cube/sidekick/actions/workflows/main.yml/badge.svg)](https://github.com/c-cube/sidekick/actions/workflows/main.yml) -Sidekick is an OCaml library with a functor to create SMT solvers following +Sidekick is an OCaml library for creating SMT solvers following the CDCL(T) approach (so called "lazy SMT"). See [below](#short-summary) for a more detailed explanation. @@ -35,11 +35,11 @@ arithmetic, algebraic datatypes, and others. Sidekick is a CDCL(T) solver implemented in pure [OCaml](https://ocaml.org/) and with a strong focus on modularity and reusability of components. -Almost everything in the code is _functorized_ and generic over the concrete -representation of terms, formulas, etc. -The goal is for users to be able to implement their own theories and combine -them with the pre-existing ones in a bespoke solver, something that is typically -a lot of work in the C/C++ solvers. +It _used to_ provide a functorized interface, but it now comes with its own +representation of terms, in a simple version of the Calculus of Constructions. +Users can extend that term representation by adding new custom _constants_ +to model their domain theories. Most of the constants defined in sidekick are +defined exactly as outside constants would be. Sidekick comes in several components (as in, opam packages):