package mc2
A mcsat-based SMT solver in pure OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
doc/src/mc2.core/Reason.ml.html
Source file Reason.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29open Solver_types type t = reason let pp out = function | n, _ when n < 0 -> Format.fprintf out "%%" | n, Decision -> Format.fprintf out "@@%d" n | n, Bcp c -> Format.fprintf out "#%d@<1>←%s%d" n (Premise.prefix c.c_premise) c.c_name | n, Bcp_lazy c -> if Lazy.is_val c then ( let lazy c = c in Format.fprintf out "#%d@<1>←%s%d" n (Premise.prefix c.c_premise) c.c_name ) else Format.fprintf out "#%d@<1>←<lazy>" n | n, Eval _ -> Format.fprintf out "$%d" n let pp_opt out = function | n, _ when n < 0 -> Format.fprintf out "%%" | n, None -> Format.fprintf out "%d" n | n, Some r -> pp out (n,r)