package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

(* 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-complete-basic" (fun () ->
      no_max_vars := true
    );
  Params.add_to_mode "ho-pragmatic" (fun () ->
      no_max_vars := false;
      max_vars    := 10;
    );
  Params.add_to_mode "ho-competitive" (fun () ->
      no_max_vars := false;
      max_vars    := 10;
    );
  Params.add_to_mode "fo-complete-basic" (fun () ->
      no_max_vars := true
    );
  ()
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct