;;
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_substitution ~formatter:f subst =
- (List.iter
- (fun (i, t) ->
- (Format.fprintf f "?%d -> " i;
- pp_foterm f t)
- )
- subst)
+ Format.fprintf f "@[<v 2>";
+ List.iter
+ (fun (i, t) ->
+ (Format.fprintf f "?%d -> " i;
+ pp_foterm f t;
+ Format.fprintf f "@;"))
+ subst;
+ Format.fprintf f "@]";
;;
let pp_proof bag ~formatter:f p =
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
+ Format.fprintf f "@[<hv>{";
+ pp_foterm f t;
+ Format.fprintf f "@;[%s] by %s@]"
+ (String.concat ", " (List.map string_of_int vars))
+ (match proof with
+ | Terms.Exact _ -> "axiom"
+ | Terms.Step (rule, id1, id2, _, p, _) ->
+ Printf.sprintf "%s %d with %d at %s"
+ (string_of_rule rule)
+ id1 id2 (String.concat
+ "," (List.map string_of_int p)))
| 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 =