(fun x _ m -> embed m x) m args
in
m, Terms.Node (Terms.Leaf (hash name):: args)
- ;;
+ let is_eq = function
+ | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
+ Some (ty,l,r)
+ | _ -> None
let saturate bo ty =
let vars, ty = embed [] ty in
let _, bo = embed vars bo in
~max_steps:max_int bag ~g_passives:[g_passives] ~passives
with
| P.Error s -> report_error s; 3
- | P.Unsatisfiable ((bag,_,l)::_) ->
+ | P.Unsatisfiable ((bag,_,_,l)::_) ->
success_msg bag l pp_unit_clause name; 0
| P.Unsatisfiable ([]) ->
report_error "Unsatisfiable but no solution output"; 3