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

feat: expose printers

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 19:46:58 -06:00 • committed by Guillaume Bury
parent 6dbaa2d335
commit d089db3e4d
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/core/Msat.ml
View file

@ -53,6 +53,17 @@ type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof)
type negated = Solver_intf.negated = Negated | Same_sign type negated = Solver_intf.negated = Negated | Same_sign
(** Print {!negated} values *)
let pp_negated out = function
| Negated -> Format.fprintf out "negated"
| Same_sign -> Format.fprintf out "same-sign"
(** Print {!lbool} values *)
let pp_lbool out = function
| L_true -> Format.fprintf out "true"
| L_false -> Format.fprintf out "false"
| L_undefined -> Format.fprintf out "undefined"
module Make_mcsat = Solver.Make_mcsat module Make_mcsat = Solver.Make_mcsat
module Make_cdcl_t = Solver.Make_cdcl_t module Make_cdcl_t = Solver.Make_cdcl_t
module Make_pure_sat = Solver.Make_pure_sat module Make_pure_sat = Solver.Make_pure_sat