WIP: Add search into the core library.

TODO
- [X] C++ lib
- [X] Python lib
- [ ] Javascript lib
- [ ] C++ test
- [ ] Python test
- [ ] Javascript test

Author: hzhangxyz

examples/main.cc

@@ -2,134 +2,54 @@
 #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)\n"
+               "`P\n"
+               "----------\n"
+               "`Q\n");
     // 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
-    );
-
-    auto premise = ds::text_to_rule("(! (! X))", temp_data_size);
-    auto target = ds::text_to_rule("X", temp_data_size);
+    search.add("(((! `p) -> (! `q)) -> (`q -> `p))");
 
-    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;
+    // premise
+    search.add("(! (! X))");
 
-    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();
-
-        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));
-                }
+        bool success = false;
+        auto callback = [&target, &success, &temp_text_size](ds::rule_t* candidate) {
+            if (candidate->data_size() != target->data_size()) {
+                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);
+            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;
+        };
+        search.execute(callback);
+        if (success) {
+            break;
         }
     }
 }

examples/main.mjs

@@ -1,93 +1,40 @@
-import { buffer_size, rule_t } from "../tsds/tsds.mts";
+import { rule_t, search_t } 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 single_result_size = 10000;
 
-// biome-ignore format: 保持多行对齐
-// (!p -> !q) -> (q -> p)
-const axiom3 = new rule_t(
-    "(((! `p) -> (! `q)) -> (`q -> `p))"
-);
+    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;
         }
     }
 }

examples/main.py

@@ -1,80 +1,42 @@
 import time
 import pyds
 
-pyds.buffer_size(1000)
 
-# P -> Q, P |- Q
-mp = pyds.Rule("""
-(`P -> `Q)
-`P
-----------
-`Q
-""")
-
-# p -> (q -> p)
-axiom1 = pyds.Rule("""
-------------------
-(`p -> (`q -> `p))
-""")
-
-# (p -> (q -> r)) -> ((p -> q) -> (p -> r))
-axiom2 = pyds.Rule("""
---------------------------------------------------
-((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))
-""")
+def main():
+    temp_data_size = 1000
+    single_result_size = 10000
 
-# (!p -> !q) -> (q -> p)
-axiom3 = pyds.Rule("""
-----------------------------------
-(((! `p) -> (! `q)) -> (`q -> `p))
-""")
+    search = pyds.Search(temp_data_size, single_result_size)
 
-premise = pyds.Rule("(! (! X))")
-target = pyds.Rule("X")
+    # 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))")
 
+    # premise
+    search.add("(! (! X))")
 
-def main():
-    rules: dict[pyds.Rule, int] = {}
-    facts: dict[pyds.Rule, int] = {}
-
-    cycle = -1
-    rules[mp] = cycle
-    facts[axiom1] = cycle
-    facts[axiom2] = cycle
-    facts[axiom3] = cycle
-    facts[premise] = cycle
+    target = pyds.Rule("X")
 
     while True:
-        temp_rules: set[pyds.Rule] = set()
-        temp_facts: set[pyds.Rule] = set()
-
-        for rule, r_cycle in rules.items():
-            for fact, f_cycle in facts.items():
-                if r_cycle != cycle and f_cycle != cycle:
-                    continue
-                candidate = rule @ fact
-                if candidate is None:
-                    continue
-                if len(candidate) != 0:
-                    # Rule
-                    if candidate in rules or candidate in temp_rules:
-                        continue
-                    temp_rules.add(candidate)
-                else:
-                    # Fact
-                    if candidate in facts or candidate in temp_facts:
-                        continue
-                    if hash(candidate) == hash(target):
-                        print("Found!")
-                        print(candidate)
-                        return
-                    temp_facts.add(candidate)
-
-        cycle += 1
-        for rule in temp_rules:
-            rules[rule] = cycle
-        for fact in temp_facts:
-            facts[fact] = cycle
+        success = False
+
+        def callback(candidate: pyds.Rule) -> bool:
+            if candidate == target:
+                print("Found!")
+                print(candidate)
+                nonlocal success
+                success = True
+                return True
+            return False
+
+        search.execute(callback)
+        if success:
+            break
 
 
 for i in range(10):