Skip to content
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.

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

Indexing via discrimination tree #205

Merged
merged 57 commits into from
Nov 23, 2023
Merged

Indexing via discrimination tree #205

merged 57 commits into from
Nov 23, 2023

Conversation

FissoreD
Copy link
Collaborator

No description provided.

@gares
Copy link
Contributor

gares commented Nov 16, 2023

Looks much better than this morning. Do the tests pass if we always use the DT index?

@FissoreD
Copy link
Collaborator Author

Most tests pass, but not all yet. I should look deeper to spot the bug.
There are some slow down in performance especially for tests like crypt.
Even if I think this particular test is not a good use case for indexing with trie, at least in the current implementation
where we do not limit the height/depth of the path representing the goal, I suppose
lot of time is spent during the creation of the path corresponding to the goal.
There are 5 timeout:

TIMEOUT  lyp (type checker for λΥP)                elpi
TIMEOUT  map (defined list) (stdlib map reference)   elpi
TIMEOUT  map (rbtree) (stdlib map)                   elpi
TIMEOUT  mu (standard Prolog benchmark)              elpi
TIMEOUT  set (stdlib set)                            elpi

And three failures:

KO       eta_as (eta expansion of as clause)         elpi
KO       trace-browser-chr (trace generation)        elpi
KO       uvar_keyword (uvar kwd status at the meta level) elpi

src/data.ml Outdated
@@ -181,6 +181,7 @@ and type t = (clause * int) list = struct
type t = elt list [@@deriving show]

let get_time_stamp = snd
let equal a b = a = b
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you should use the timestamp as a unique id, here you are comparing the clause "code" which can be large.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I totally agree

src/runtime.ml Show resolved Hide resolved
src/data.ml Outdated Show resolved Hide resolved
src/data.ml Outdated Show resolved Hide resolved
src/discrimination_tree.ml Outdated Show resolved Hide resolved
src/discrimination_tree.ml Show resolved Hide resolved
@gares gares merged commit 4ce8dea into LPCIC:master Nov 23, 2023
9 of 10 checks passed
@FissoreD FissoreD deleted the discr-tree branch May 27, 2024 16:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants