Source file heuristics.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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Heuristics} *)

open Logtk
open Libzipperposition

module T = Term
module Lit = Literal

let depth_limit_ = ref None
let max_vars = ref 10
let no_max_vars = ref false

let enable_depth_limit i =
  if i <= 0 then invalid_arg "Heuristics.enable_depth_limit";
  depth_limit_ := Some i

let section = Util.Section.make ~parent:Const.section "heuristics"

let stat_depth_limit = Util.mk_stat "trivial.too_deep"
let stat_vars = Util.mk_stat "trivial.too_many_vars"

(** {2 Rules} *)

module type S = sig
  module Env : Env.S
  module C : module type of Env.C
  module PS : module type of Env.ProofState

  val register : unit -> unit
end

module Make(E : Env.S) = struct
  module Env = E
  module PS = Env.ProofState
  module C = Env.C
  module Ctx = Env.Ctx

  let _depth_types lits =
    Literals.Seq.terms lits
    |> Iter.map T.ty
    |> Iter.map (fun t -> InnerTerm.depth (t : Type.t :> InnerTerm.t))
    |> Iter.max ?lt:None
    |> CCOpt.map_or ~default:0 CCFun.id

  let is_too_deep c =
    match !depth_limit_ with
    | None -> false
    | Some d ->
      let lits = C.lits c in
      let depth = max (_depth_types lits) (Literals.depth lits) in
      if depth > d
      then (
        Ctx.lost_completeness();
        Util.incr_stat stat_depth_limit;
        Util.debugf ~section 5 "@[<2>clause dismissed (too deep at %d):@ @[%a@]@]"
          (fun k->k depth C.pp c);
        true
      ) else false

  let has_too_many_vars c =
    if !no_max_vars
    then false
    else (
      let lits = C.lits c in
      (* number of distinct term variables *)
      let n_vars =
        (Literals.vars lits
         |> List.filter (fun v -> not (Type.is_tType (HVar.ty v)))
         |> List.length)
      in
      if n_vars > !max_vars then (
        Ctx.lost_completeness();
        Util.incr_stat stat_vars;
        Util.debugf ~section 5 "@[<2>clause dismissed (%d vars is too much):@ @[%a@]@]"
          (fun k->k n_vars C.pp c);
        true
      ) else false
    )

  let register () =
    Util.debug ~section 2 "register heuristics...";
    Env.add_is_trivial is_too_deep;
    Env.add_is_trivial has_too_many_vars;
    ()
end

let extension =
  let action env =
    let module E = (val env : Env.S) in
    let module H = Make(E) in
    H.register ()
  in
  Extensions.(
    { default with name="heuristics"; env_actions=[action]; }
  )

let () =
  Params.add_opts
    [ "--depth-limit", Arg.Int enable_depth_limit, " set maximal term depth";
      "--max-vars", Arg.Set_int max_vars, " maximum number of variables per clause";
      "--no-max-vars", Arg.Set no_max_vars, " disable maximum number of variables per clause";
      "--enable-max-vars", Arg.Clear no_max_vars, "enable maximum number of variables per clause";
    ];
  Params.add_to_mode "ho-pragmatic" (fun () ->
      no_max_vars := true;
    );
  Params.add_to_mode "ho-competitive" (fun () ->
      no_max_vars := true;
    );
  Params.add_to_modes 
    [ "ho-complete-basic"
    ; "fo-complete-basic"
    ; "lambda-free-intensional"
    ; "lambda-free-extensional"
    ; "ho-comb-complete"
    ; "lambda-free-purify-intensional"
    ; "lambda-free-purify-extensional"] 
    (fun () ->
       no_max_vars := true;
    );
  ()