;;
let string_of_rule = function
- | Terms.SuperpositionRight -> "SupR"
- | Terms.SuperpositionLeft -> "SupL"
- | Terms.Demodulation -> "Demod"
+ | Terms.Superposition -> "Super"
+ | Terms.Demodulation -> "Demod"
;;
let string_of_direction = function
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
- Format.fprintf f "Id : %d, " id ;
+ Format.fprintf f "Id : %3d, " id ;
match l with
| Terms.Predicate t ->
pp_foterm f t
| Terms.Equation (lhs, rhs, ty, comp) ->
- Format.fprintf f "{";
+ Format.fprintf f "@[<hv>{";
pp_foterm f ty;
- Format.fprintf f "}: ";
+ Format.fprintf f "}:@;@[<hv>";
pp_foterm f lhs;
- Format.fprintf f " %s " (string_of_comparison comp);
+ Format.fprintf f "@;%s@;" (string_of_comparison comp);
pp_foterm f rhs;
- Format.fprintf f " [%s] by %s"
+ Format.fprintf f "@]@;[%s] by %s@]"
(String.concat ", " (List.map string_of_int vars))
(match proof with
| Terms.Exact _ -> "axiom"
(string_of_rule rule)
id1 id2 (String.concat
"," (List.map string_of_int p)))
-
;;
let pp_bag ~formatter:f bag =