Skip to content

Commit edac756

Browse files
hzhangxyzCopilot
hzhangxyz
and
Copilot
committed
Add search class into the core library.
Co-authored-by: Copilot <[email protected]>
1 parent 5783fcb commit edac756

File tree

11 files changed

+403
-258
lines changed

11 files changed

+403
-258
lines changed

‎examples/main.cc‎

Lines changed: 28 additions & 109 deletions
Original file line numberDiff line numberDiff line change
@@ -2,134 +2,53 @@
22
#include <cstring>
33
#include <functional>
44
#include <iostream>
5-
#include <map>
6-
#include <set>
75

86
#include <ds/ds.hh>
7+
#include <ds/search.hh>
98
#include <ds/utility.hh>
109

11-
struct PointerLess {
12-
template<typename T>
13-
bool operator()(const T& lhs, const T& rhs) const {
14-
if (lhs->data_size() < rhs->data_size()) {
15-
return true;
16-
}
17-
if (lhs->data_size() > rhs->data_size()) {
18-
return false;
19-
}
20-
ds::length_t data_size = lhs->data_size();
21-
const std::byte* lhs_data = reinterpret_cast<const std::byte*>(lhs.get());
22-
const std::byte* rhs_data = reinterpret_cast<const std::byte*>(rhs.get());
23-
for (ds::length_t index = 0; index < data_size; ++index) {
24-
if (lhs_data[index] < rhs_data[index]) {
25-
return true;
26-
}
27-
if (lhs_data[index] > rhs_data[index]) {
28-
return false;
29-
}
30-
}
31-
return false;
32-
}
33-
};
34-
3510
void run() {
3611
int temp_data_size = 1000;
3712
int temp_text_size = 1000;
3813
int single_result_size = 10000;
3914

15+
auto search = ds::search_t(temp_data_size, single_result_size);
16+
4017
// P -> Q, P |- Q
41-
auto mp = ds::text_to_rule(
42-
"(`P -> `Q)\n"
43-
"`P\n"
44-
"----------\n"
45-
"`Q",
46-
temp_data_size
47-
);
18+
search.add("(`P -> `Q) `P `Q");
4819
// p -> (q -> p)
49-
auto axiom1 = ds::text_to_rule(
50-
"------------------\n"
51-
"(`p -> (`q -> `p))\n",
52-
temp_data_size
53-
);
20+
search.add("(`p -> (`q -> `p))");
5421
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
55-
auto axiom2 = ds::text_to_rule(
56-
"--------------------------------------------------\n"
57-
"((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))\n",
58-
temp_data_size
59-
);
22+
search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))");
6023
// (!p -> !q) -> (q -> p)
61-
auto axiom3 = ds::text_to_rule(
62-
"----------------------------------\n"
63-
"(((! `p) -> (! `q)) -> (`q -> `p))\n",
64-
temp_data_size
65-
);
24+
search.add("(((! `p) -> (! `q)) -> (`q -> `p))");
6625

67-
auto premise = ds::text_to_rule("(! (! X))", temp_data_size);
68-
auto target = ds::text_to_rule("X", temp_data_size);
26+
// premise
27+
search.add("(! (! X))");
6928

70-
std::map<std::unique_ptr<ds::rule_t>, ds::length_t, PointerLess> rules;
71-
std::map<std::unique_ptr<ds::rule_t>, ds::length_t, PointerLess> facts;
72-
73-
std::set<std::unique_ptr<ds::rule_t>, PointerLess> temp_rules;
74-
std::set<std::unique_ptr<ds::rule_t>, PointerLess> temp_facts;
75-
76-
ds::length_t cycle = -1;
77-
rules.emplace(std::move(mp), cycle);
78-
facts.emplace(std::move(axiom1), cycle);
79-
facts.emplace(std::move(axiom2), cycle);
80-
facts.emplace(std::move(axiom3), cycle);
81-
facts.emplace(std::move(premise), cycle);
82-
83-
auto buffer = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(single_result_size)));
84-
85-
auto less = PointerLess();
29+
auto target = ds::text_to_rule("X", temp_data_size);
8630

8731
while (true) {
88-
temp_rules.clear();
89-
temp_facts.clear();
32+
bool success = false;
9033

91-
for (auto& [rule, rules_cycle] : rules) {
92-
for (auto& [fact, facts_cycle] : facts) {
93-
if (rules_cycle != cycle && facts_cycle != cycle) {
94-
continue;
95-
}
96-
buffer->match(rule.get(), fact.get(), reinterpret_cast<std::byte*>(buffer.get()) + single_result_size);
97-
if (!buffer->valid()) {
98-
continue;
99-
}
100-
if (buffer->premises_count() != 0) {
101-
// rule
102-
if (rules.find(buffer) != rules.end() || temp_rules.find(buffer) != temp_rules.end()) {
103-
continue;
104-
}
105-
auto new_rule = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(buffer->data_size())));
106-
memcpy(new_rule.get(), buffer.get(), buffer->data_size());
107-
temp_rules.emplace(std::move(new_rule));
108-
} else {
109-
// fact
110-
if (facts.find(buffer) != facts.end() || temp_facts.find(buffer) != temp_facts.end()) {
111-
continue;
112-
}
113-
auto new_fact = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(buffer->data_size())));
114-
memcpy(new_fact.get(), buffer.get(), buffer->data_size());
115-
if ((!less(new_fact, target)) && (!less(target, new_fact))) {
116-
printf("Found!\n");
117-
printf("%s", ds::rule_to_text(new_fact.get(), temp_text_size).get());
118-
return;
119-
}
120-
temp_facts.emplace(std::move(new_fact));
121-
}
34+
auto callback = [&target, &success, &temp_text_size](ds::rule_t* candidate) {
35+
if (candidate->data_size() != target->data_size()) {
36+
return false;
12237
}
123-
}
38+
auto data_size = candidate->data_size();
39+
auto equal = memcmp(candidate->head(), target->head(), data_size) == 0;
40+
if (equal) {
41+
printf("Found!\n");
42+
printf("%s", ds::rule_to_text(candidate, temp_text_size).get());
43+
success = true;
44+
return true;
45+
}
46+
return false;
47+
};
12448

125-
++cycle;
126-
for (auto& rule : temp_rules) {
127-
auto& movable_rule = const_cast<std::unique_ptr<ds::rule_t>&>(rule);
128-
rules.emplace(std::move(movable_rule), cycle);
129-
}
130-
for (auto& fact : temp_facts) {
131-
auto& movable_fact = const_cast<std::unique_ptr<ds::rule_t>&>(fact);
132-
facts.emplace(std::move(movable_fact), cycle);
49+
search.execute(callback);
50+
if (success) {
51+
break;
13352
}
13453
}
13554
}
@@ -139,7 +58,7 @@ void timer(std::function<void()> func) {
13958
func();
14059
auto end = std::chrono::high_resolution_clock::now();
14160
std::chrono::duration<double> duration = end - start;
142-
std::cout << "Execution time: " << duration.count() << " seconds\n" << std::flush;
61+
std::cout << "Execution time: " << duration.count() << " seconds" << std::endl;
14362
}
14463

14564
int main() {

‎examples/main.mjs‎

Lines changed: 32 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,43 @@
1-
import { buffer_size, rule_t } from "../tsds/tsds.mts";
1+
import { rule_t, search_t, buffer_size } from "../tsds/tsds.mts";
22

3-
buffer_size(1000);
4-
5-
// biome-ignore format: 保持多行对齐
6-
// P -> Q, P |- Q
7-
const mp = new rule_t(
8-
"(`P -> `Q)\n" +
9-
"`P\n" +
10-
"----------\n" +
11-
"`Q\n");
12-
13-
// biome-ignore format: 保持多行对齐
14-
// p -> (q -> p)
15-
const axiom1 = new rule_t(
16-
"(`p -> (`q -> `p))"
17-
);
18-
19-
// biome-ignore format: 保持多行对齐
20-
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
21-
const axiom2 = new rule_t(
22-
"((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"
23-
);
3+
function main() {
4+
const temp_data_size = 1000;
5+
const temp_text_size = 1000;
6+
const single_result_size = 10000;
247

25-
// biome-ignore format: 保持多行对齐
26-
// (!p -> !q) -> (q -> p)
27-
const axiom3 = new rule_t(
28-
"(((! `p) -> (! `q)) -> (`q -> `p))"
29-
);
8+
buffer_size(temp_text_size);
9+
const search = new search_t(temp_data_size, single_result_size);
3010

31-
const premise = new rule_t("(! (! X))");
32-
const target = new rule_t("X");
33-
const target_hash = target.key();
11+
// P -> Q, P |- Q
12+
search.add("(`P -> `Q) `P `Q\n");
13+
// p -> (q -> p)
14+
search.add("(`p -> (`q -> `p))");
15+
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
16+
search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))");
17+
// (!p -> !q) -> (q -> p)
18+
search.add("(((! `p) -> (! `q)) -> (`q -> `p))");
3419

35-
function main() {
36-
const rules = {};
37-
const facts = {};
20+
// premise
21+
search.add("(! (! X))");
3822

39-
let cycle = -1;
40-
rules[mp.key()] = [mp, cycle];
41-
facts[axiom1.key()] = [axiom1, cycle];
42-
facts[axiom2.key()] = [axiom2, cycle];
43-
facts[axiom3.key()] = [axiom3, cycle];
44-
facts[premise.key()] = [premise, cycle];
23+
const target = new rule_t("X");
4524

4625
while (true) {
47-
const temp_rules = {};
48-
const temp_facts = {};
49-
50-
for (const r_hash in rules) {
51-
for (const f_hash in facts) {
52-
const [rule, r_cycle] = rules[r_hash];
53-
const [fact, f_cycle] = facts[f_hash];
54-
if (r_cycle !== cycle && f_cycle !== cycle) {
55-
continue;
56-
}
57-
const candidate = rule.match(fact);
58-
if (candidate === null) {
59-
continue;
60-
}
61-
const candidate_hash = candidate.key();
62-
if (candidate.length() !== 0) {
63-
// rule
64-
if (candidate_hash in rules || candidate_hash in temp_rules) {
65-
continue;
66-
}
67-
temp_rules[candidate_hash] = candidate;
68-
} else {
69-
// fact
70-
if (candidate_hash in facts || candidate_hash in temp_facts) {
71-
continue;
72-
}
73-
if (candidate_hash === target_hash) {
74-
console.log("Found!");
75-
console.log(candidate.toString());
76-
return;
77-
}
78-
temp_facts[candidate_hash] = candidate;
79-
}
26+
let success = false;
27+
28+
const callback = (candidate) => {
29+
if (candidate.key() === target.key()) {
30+
console.log("Found!");
31+
console.log(candidate.toString());
32+
success = true;
33+
return true;
8034
}
81-
}
35+
return false;
36+
};
8237

83-
cycle++;
84-
for (const r_hash in temp_rules) {
85-
const rule = temp_rules[r_hash];
86-
rules[rule.key()] = [rule, cycle];
87-
}
88-
for (const f_hash in temp_facts) {
89-
const fact = temp_facts[f_hash];
90-
facts[fact.key()] = [fact, cycle];
38+
search.execute(callback);
39+
if (success) {
40+
break;
9141
}
9242
}
9343
}
@@ -96,5 +46,5 @@ for (let i = 0; i < 10; i++) {
9646
const begin = new Date();
9747
main();
9848
const end = new Date();
99-
console.log(`Time taken: ${(end - begin) / 1000}s`);
49+
console.log(`Execution time: ${(end - begin) / 1000} seconds`);
10050
}

0 commit comments

Comments
 (0)