package mc2

You can search for identifiers within the package.

in-package search v0.2.0

A mcsat-based SMT solver in pure OCaml

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

v0.1.tar.gz

md5=92de696251ec76fbf3eba6ee917fd80f

sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0

doc/mc2.core/Mc2_core/Term/TC/index.html

Module `Term.TC`Source

Typeclass

Sourcetype t = tc

Source

val make : 
  ?init:
    (Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> unit) ->
  ?update_watches:
    (Mc2_core__.Solver_types.actions ->
      Mc2_core__.Solver_types.term ->
      watch:Mc2_core__.Solver_types.term ->
      Mc2_core__.Solver_types.watch_res) ->
  ?delete:(Mc2_core__.Solver_types.term -> unit) ->
  ?subterms:
    (Mc2_core__.Solver_types.term_view ->
      (Mc2_core__.Solver_types.term -> unit) ->
      unit) ->
  ?eval:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.eval_res) ->
  pp:Mc2_core__.Solver_types.term_view CCFormat.printer ->
  unit ->
  t

Make a new typeclass, directly

Lazy builder

Sourcetype lazy_tc

Sourceval lazy_from_val : t -> lazy_tc

Sourceval lazy_make : unit -> lazy_tc

Make a new typeclass, without providing the actual functions

Sourceval lazy_get : lazy_tc -> tc

Obtain the underlying typeclass; call only after lazy_complete