Source file ProverSearch.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
open Tactical
open Strategy
let configure (console : #Tactical.feedback) strategy =
let { tactical ; selection ; arguments } = strategy in
let verdict () =
try
tactical#reset ;
Strategy.set_args tactical arguments ;
tactical#select console selection
with Not_found | Exit -> Not_applicable
in
match Lang.local ~pool:console#pool verdict () with
| Applicable process when not console#has_error ->
let script = ProofScript.jtactic tactical selection in
Some (script , process)
| _ -> None
let fork tree anchor strategy =
let console = new ProofScript.console
~pool:(ProofEngine.pool tree)
~title:strategy.tactical#title in
try
let context = ProofEngine.node_context anchor in
match WpContext.on_context context (configure console) strategy with
| None -> None
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
with
| Exit | Not_found | Invalid_argument _ ->
console#set_error "Can not configure strategy" ; None
| e ->
console#set_error "Exception <%s>" (Printexc.to_string e) ;
raise e
let rec lookup tree anchor k hs =
let n = Array.length hs in
if n=0 then None,0,[| |] else
match fork tree anchor hs.(k) with
| Some fork -> Some fork,k,hs
| None ->
if k = 0 then
lookup tree anchor 0 (Array.sub hs 1 (n-1))
else
let slice = Array.sub hs 0 (n-1) in
if k < n-1 then
( Array.blit hs (succ k) slice k (n-k-1) ;
lookup tree anchor k slice )
else
lookup tree anchor 0 hs
let index tree ~anchor ~index =
if index < 0 then None else
let _,hs = ProofEngine.get_strategies anchor in
if index < Array.length hs then
fork tree anchor hs.(index)
else None
let first tree ?anchor strategies =
let node = ProofEngine.anchor tree ?node:anchor () in
let fork,index,space = lookup tree node 0 strategies in
ProofEngine.set_strategies node ~index space ; fork
let search tree ?anchor ?sequent heuristics =
let pool = new Strategy.pool in
let anchor = ProofEngine.anchor tree ?node:anchor () in
let sequent =
match sequent with
| Some s -> s
| None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
let lookup h = try h#search pool#add sequent with Not_found -> () in
Conditions.index sequent ;
WpContext.on_context
(ProofEngine.node_context anchor)
(List.iter lookup) heuristics ;
first tree ~anchor pool#sort
let backtrack tree ?anchor ?(loop=false) ?(width = max_int) () =
let node = ProofEngine.anchor tree ?node:anchor () in
let k,hs = ProofEngine.get_strategies node in
let n = Array.length hs in
if 1<n && (loop || succ k < (min n width)) then
let k = if succ k < n then succ k else 0 in
let fork,index,hs = lookup tree node k hs in
ProofEngine.set_strategies node ~index hs ; fork
else None