Skip to content

Add search into the core library. #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hzhangxyz merged 1 commit into from
Jul 27, 2025
Merged

Add search into the core library. #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
137 changes: 28 additions & 109 deletions examples/main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,134 +2,53 @@
#include <cstring>
#include <functional>
#include <iostream>
#include <map>
#include <set>

#include <ds/ds.hh>
#include <ds/search.hh>
#include <ds/utility.hh>

struct PointerLess {
template<typename T>
bool operator()(const T& lhs, const T& rhs) const {
if (lhs->data_size() < rhs->data_size()) {
return true;
}
if (lhs->data_size() > rhs->data_size()) {
return false;
}
ds::length_t data_size = lhs->data_size();
const std::byte* lhs_data = reinterpret_cast<const std::byte*>(lhs.get());
const std::byte* rhs_data = reinterpret_cast<const std::byte*>(rhs.get());
for (ds::length_t index = 0; index < data_size; ++index) {
if (lhs_data[index] < rhs_data[index]) {
return true;
}
if (lhs_data[index] > rhs_data[index]) {
return false;
}
}
return false;
}
};

void run() {
int temp_data_size = 1000;
int temp_text_size = 1000;
int single_result_size = 10000;

auto search = ds::search_t(temp_data_size, single_result_size);

// P -> Q, P |- Q
auto mp = ds::text_to_rule(
"(`P -> `Q)\n"
"`P\n"
"----------\n"
"`Q",
temp_data_size
);
search.add("(`P -> `Q) `P `Q");
// p -> (q -> p)
auto axiom1 = ds::text_to_rule(
"------------------\n"
"(`p -> (`q -> `p))\n",
temp_data_size
);
search.add("(`p -> (`q -> `p))");
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
auto axiom2 = ds::text_to_rule(
"--------------------------------------------------\n"
"((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))\n",
temp_data_size
);
search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))");
// (!p -> !q) -> (q -> p)
auto axiom3 = ds::text_to_rule(
"----------------------------------\n"
"(((! `p) -> (! `q)) -> (`q -> `p))\n",
temp_data_size
);
search.add("(((! `p) -> (! `q)) -> (`q -> `p))");

auto premise = ds::text_to_rule("(! (! X))", temp_data_size);
auto target = ds::text_to_rule("X", temp_data_size);
// premise
search.add("(! (! X))");

std::map<std::unique_ptr<ds::rule_t>, ds::length_t, PointerLess> rules;
std::map<std::unique_ptr<ds::rule_t>, ds::length_t, PointerLess> facts;

std::set<std::unique_ptr<ds::rule_t>, PointerLess> temp_rules;
std::set<std::unique_ptr<ds::rule_t>, PointerLess> temp_facts;

ds::length_t cycle = -1;
rules.emplace(std::move(mp), cycle);
facts.emplace(std::move(axiom1), cycle);
facts.emplace(std::move(axiom2), cycle);
facts.emplace(std::move(axiom3), cycle);
facts.emplace(std::move(premise), cycle);

auto buffer = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(single_result_size)));

auto less = PointerLess();
auto target = ds::text_to_rule("X", temp_data_size);

while (true) {
temp_rules.clear();
temp_facts.clear();
bool success = false;

for (auto& [rule, rules_cycle] : rules) {
for (auto& [fact, facts_cycle] : facts) {
if (rules_cycle != cycle && facts_cycle != cycle) {
continue;
}
buffer->match(rule.get(), fact.get(), reinterpret_cast<std::byte*>(buffer.get()) + single_result_size);
if (!buffer->valid()) {
continue;
}
if (buffer->premises_count() != 0) {
// rule
if (rules.find(buffer) != rules.end() || temp_rules.find(buffer) != temp_rules.end()) {
continue;
}
auto new_rule = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(buffer->data_size())));
memcpy(new_rule.get(), buffer.get(), buffer->data_size());
temp_rules.emplace(std::move(new_rule));
} else {
// fact
if (facts.find(buffer) != facts.end() || temp_facts.find(buffer) != temp_facts.end()) {
continue;
}
auto new_fact = std::unique_ptr<ds::rule_t>(reinterpret_cast<ds::rule_t*>(operator new(buffer->data_size())));
memcpy(new_fact.get(), buffer.get(), buffer->data_size());
if ((!less(new_fact, target)) && (!less(target, new_fact))) {
printf("Found!\n");
printf("%s", ds::rule_to_text(new_fact.get(), temp_text_size).get());
return;
}
temp_facts.emplace(std::move(new_fact));
}
auto callback = [&target, &success, &temp_text_size](ds::rule_t* candidate) {
if (candidate->data_size() != target->data_size()) {
return false;
}
}
auto data_size = candidate->data_size();
auto equal = memcmp(candidate->head(), target->head(), data_size) == 0;
if (equal) {
printf("Found!\n");
printf("%s", ds::rule_to_text(candidate, temp_text_size).get());
success = true;
return true;
}
return false;
};

++cycle;
for (auto& rule : temp_rules) {
auto& movable_rule = const_cast<std::unique_ptr<ds::rule_t>&>(rule);
rules.emplace(std::move(movable_rule), cycle);
}
for (auto& fact : temp_facts) {
auto& movable_fact = const_cast<std::unique_ptr<ds::rule_t>&>(fact);
facts.emplace(std::move(movable_fact), cycle);
search.execute(callback);
if (success) {
break;
}
}
}
Expand All @@ -139,7 +58,7 @@ void timer(std::function<void()> func) {
func();
auto end = std::chrono::high_resolution_clock::now();
std::chrono::duration<double> duration = end - start;
std::cout << "Execution time: " << duration.count() << " seconds\n" << std::flush;
std::cout << "Execution time: " << duration.count() << " seconds" << std::endl;
}

int main() {
Expand Down
114 changes: 32 additions & 82 deletions examples/main.mjs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,93 +1,43 @@
import { buffer_size, rule_t } from "../tsds/tsds.mts";
import { rule_t, search_t, buffer_size } from "../tsds/tsds.mts";

buffer_size(1000);

// biome-ignore format: 保持多行对齐
// P -> Q, P |- Q
const mp = new rule_t(
"(`P -> `Q)\n" +
"`P\n" +
"----------\n" +
"`Q\n");

// biome-ignore format: 保持多行对齐
// p -> (q -> p)
const axiom1 = new rule_t(
"(`p -> (`q -> `p))"
);

// biome-ignore format: 保持多行对齐
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
const axiom2 = new rule_t(
"((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"
);
function main() {
const temp_data_size = 1000;
const temp_text_size = 1000;
const single_result_size = 10000;

// biome-ignore format: 保持多行对齐
// (!p -> !q) -> (q -> p)
const axiom3 = new rule_t(
"(((! `p) -> (! `q)) -> (`q -> `p))"
);
buffer_size(temp_text_size);
const search = new search_t(temp_data_size, single_result_size);

const premise = new rule_t("(! (! X))");
const target = new rule_t("X");
const target_hash = target.key();
// P -> Q, P |- Q
search.add("(`P -> `Q) `P `Q\n");
// p -> (q -> p)
search.add("(`p -> (`q -> `p))");
// (p -> (q -> r)) -> ((p -> q) -> (p -> r))
search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))");
// (!p -> !q) -> (q -> p)
search.add("(((! `p) -> (! `q)) -> (`q -> `p))");

function main() {
const rules = {};
const facts = {};
// premise
search.add("(! (! X))");

let cycle = -1;
rules[mp.key()] = [mp, cycle];
facts[axiom1.key()] = [axiom1, cycle];
facts[axiom2.key()] = [axiom2, cycle];
facts[axiom3.key()] = [axiom3, cycle];
facts[premise.key()] = [premise, cycle];
const target = new rule_t("X");

while (true) {
const temp_rules = {};
const temp_facts = {};

for (const r_hash in rules) {
for (const f_hash in facts) {
const [rule, r_cycle] = rules[r_hash];
const [fact, f_cycle] = facts[f_hash];
if (r_cycle !== cycle && f_cycle !== cycle) {
continue;
}
const candidate = rule.match(fact);
if (candidate === null) {
continue;
}
const candidate_hash = candidate.key();
if (candidate.length() !== 0) {
// rule
if (candidate_hash in rules || candidate_hash in temp_rules) {
continue;
}
temp_rules[candidate_hash] = candidate;
} else {
// fact
if (candidate_hash in facts || candidate_hash in temp_facts) {
continue;
}
if (candidate_hash === target_hash) {
console.log("Found!");
console.log(candidate.toString());
return;
}
temp_facts[candidate_hash] = candidate;
}
let success = false;

const callback = (candidate) => {
if (candidate.key() === target.key()) {
console.log("Found!");
console.log(candidate.toString());
success = true;
return true;
}
}
return false;
};

cycle++;
for (const r_hash in temp_rules) {
const rule = temp_rules[r_hash];
rules[rule.key()] = [rule, cycle];
}
for (const f_hash in temp_facts) {
const fact = temp_facts[f_hash];
facts[fact.key()] = [fact, cycle];
search.execute(callback);
if (success) {
break;
}
}
}
Expand All @@ -96,5 +46,5 @@ for (let i = 0; i < 10; i++) {
const begin = new Date();
main();
const end = new Date();
console.log(`Time taken: ${(end - begin) / 1000}s`);
console.log(`Execution time: ${(end - begin) / 1000} seconds`);
}
Loading