simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

more doc

Browse source
This commit is contained in:
Simon Cruanes 2021-06-10 13:00:00 -04:00
parent e3a8422ab0
commit 12ba49ae5f
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/core/Sidekick_core.ml
View file

@ -51,6 +51,7 @@ module CC_view = struct
| Opaque t -> f_t t | Opaque t -> f_t t
end end
(** Main representation of Terms and Types *)
module type TERM = sig module type TERM = sig
module Fun : sig module Fun : sig
type t type t
@ -117,6 +118,12 @@ module type LIT = sig
val pp : t Fmt.printer val pp : t Fmt.printer
end end
(** Actions provided to the congruence closure.
The congruence closure must be able to propagate literals when
it detects that they are true or false; it must also
be able to create conflicts when the set of (dis)equalities
is inconsistent *)
module type CC_ACTIONS = sig module type CC_ACTIONS = sig
module T : TERM module T : TERM
module P : PROOF module P : PROOF