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
use std::collections::VecDeque;
use crate::{DefaultDerivationHeuristic,DerivationHeuristic,DerivationTree,DerivationTerm};
/// Responsible for exploring the search space of assignments for a
/// given term.
pub struct Derivation<F,T,H = DefaultDerivationHeuristic<T>>
where F:Copy+Fn(usize,&[usize],&DerivationTree<T>)->Option<bool>,
T:DerivationTerm,
H:DerivationHeuristic<T>
{
tree: DerivationTree<T>,
/// Worklist of items remaining to be explored. The first field
/// of each element identifies a term within the derivation tree,
/// whilst the second field identifies the current assignment used
/// to derive that term.
worklist: VecDeque<(usize,Vec<usize>)>,
/// Heuristic responsible for deriving individual terms.
heuristic: H,
/// Function for determining when a terminal and/or goal state is
/// reached.
query: F
}
impl<F,T,H> Derivation<F,T,H>
where F:Copy+Fn(usize,&[usize],&DerivationTree<T>)->Option<bool>,
T:DerivationTerm,
H:Default+DerivationHeuristic<T>
{
pub fn new(mut term: T, query: F) -> Self {
let n = term.domain();
// Construct initial assignment
let mut assignments = vec![0; n];
// Prevent unused variables from taking part
for i in 0..n {
if term.num_uses(i) == 0 {
// Since this is not a free variable within the term,
// there is no point exploring possible assignments
// for it. Therefore, we just give the maximum
// possible assignment as an indicator.
assignments[i] = usize::MAX;
}
}
// Construct proof
let tree = DerivationTree::new(term);
// Construct worklist
let worklist = vec![(0,assignments)];
// Construct heuristic
let heuristic = H::default();
// Begin!
Derivation{tree, heuristic, query, worklist: worklist.into()}
}
}
impl<F,T,H> Derivation<F,T,H>
where F:Copy+Fn(usize,&[usize],&DerivationTree<T>)->Option<bool>,
T:DerivationTerm,
H:DerivationHeuristic<T>
{
/// Return current size of the search. Observe that, when this is
/// zero, the search is complete.
pub fn size(&self) -> usize {
self.worklist.len()
}
/// Continue searching along the current branch. This assumes
/// there is at least one item remaining in the worklist. We
/// apply the query function to check whether a terminal node is
/// reached (and, if so, whether we found what we're looking for).
/// If so, that is returned. Otherwise, we continue derivationting.
pub fn split(&mut self) -> Option<usize>
where F:Copy+Fn(usize,&[usize],&DerivationTree<T>)->Option<bool> {
// Pull off the next term
let (next,assignments) = self.worklist.pop_front().unwrap();
// Run the derivation functions
match (self.query)(next,&assignments,&self.tree) {
Some(true) => {
Some(next)
}
Some(false) => {
// Indicates a terminal node which doesn't match the
// query. Therefore, it is simply dropped.
None
},
None => {
// Continue derivationting!
todo!()
}
}
}
}
impl<F,T,H> Iterator for Derivation<F,T,H>
where F:Copy+Fn(usize,&[usize],&DerivationTree<T>)->Option<bool>,
T:DerivationTerm,
H:DerivationHeuristic<T>
{
type Item = (T,Vec<usize>);
fn next(&mut self) -> Option<Self::Item> {
todo!()
// loop {
// match self.internal_next_for(usize::MAX) {
// BoundedOption::Some(_,item) => { return Some(item);}
// BoundedOption::None(_) => {return None;}
// BoundedOption::OutOfResource => {}
// }
// }
}
}