Skip to content

Fixed DFS traversal #18

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

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Fixed DFS traversal #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d0382f0
some annotations
Mar 23, 2022
0d9372b
an attempt at fixing search order
Mar 23, 2022
1486a6f
fixed dfs
Mar 23, 2022
490646c
a bit of cleaning
Mar 25, 2022
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
3 changes: 3 additions & 0 deletions Project.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@ uuid = "5d8bcb5e-2b2c-4a96-a2b1-d40b3d3c344f"
authors = ["Xuan <[email protected]>"]
version = "0.1.12"

[deps]
DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"

[compat]
julia = "1.0"

Expand Down
2 changes: 2 additions & 0 deletions src/Julog.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module Julog

using DataStructures

include("structs.jl")
include("parse.jl")
include("utils.jl")
Expand Down
26 changes: 18 additions & 8 deletions src/main.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ function _unify!(src::Compound, dst::Term, src_stack, dst_stack)
end

"Handle built-in predicates"
function handle_builtins!(queue, clauses, goal, term; options...)
function handle_builtins!(queue::MutableLinkedList{GoalTree}, clauses::ClauseTable{T}, goal::GoalTree, term::Term; options...) where {T <: AbstractClause}
funcs = get(options, :funcs, Dict())
occurs_check = get(options, :occurs_check, false)
vcount = get(options, :vcount, Ref(UInt(0)))
Expand Down Expand Up @@ -264,7 +264,8 @@ function handle_builtins!(queue, clauses, goal, term; options...)
return true
elseif term.name == :cut
# Remove all other goals and succeed
empty!(queue)
#empty!(queue)
delete!(queue, 1:length(queue))
return true
elseif term.name == :fail
# Fail and skip goal
Expand Down Expand Up @@ -318,6 +319,7 @@ function resolve(goals::Vector{<:Term}, clauses::Vector{T}; options...) where {
return resolve(goals, index_clauses(clauses); options...)
end


function resolve(goals::Vector{<:Term}, clauses::ClauseTable{T}; options...) where {T <: AbstractClause}
# Unpack options
env = Subst(get(options, :env, []))
Expand All @@ -327,11 +329,12 @@ function resolve(goals::Vector{<:Term}, clauses::ClauseTable{T}; options...) wh
search = get(options, :search, :bfs)::Symbol
vcount = get(options, :vcount, Ref(UInt(0)))::Ref{UInt}
# Construct top level goal and put it on the queue
queue = [GoalTree(Const(false), nothing, Vector{Term}(goals), 1, env, Subst())]
subst = []
queue = MutableLinkedList{GoalTree}()
Copy link
Owner

@ztangent ztangent Mar 30, 2022

Choose a reason for hiding this comment

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

Is there a reason why you switched to using MutableLinkedLists? I believe Julia arrays have (amortized) constant time for pushes and pops at both the start and end of the array (see this thread), so I would only want to switch to a MutableLinkedList if there are clear performance gains on the existing benchmarks.

Copy link
Owner

@ztangent ztangent Mar 30, 2022

Choose a reason for hiding this comment

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

I think if we're going to change data structures (which I'd do as a separate PR), it seems better to use a Deque, which appears to have faster performance for pushfirst! and popfirst!: https://juliacollections.github.io/DataStructures.jl/latest/deque/

However, I think this doesn't really matter for DFS, since we can rewrite everything to use only push! and pop! from the end of a Vector.

push!(queue, GoalTree(Const(false), nothing, Vector{Term}(goals), 1, env, Subst()))
subst = Subst[]
# Iterate across queue of goals
while length(queue) > 0
goal = (search == :dfs) ? pop!(queue) : popfirst!(queue)
goal = popfirst!(queue)
@debug string("Goal: ", Clause(goal.term, goal.children), " ",
"Env: ", goal.env)
if goal.active > length(goal.children)
Expand Down Expand Up @@ -367,7 +370,7 @@ function resolve(goals::Vector{<:Term}, clauses::ClauseTable{T}; options...) wh
parent.env = compose!(parent.env, vmap)
# Advance parent to next subgoal and put it back on the queue
parent.active += 1
push!(queue, parent)
(search==:dfs) ? pushfirst!(queue, parent) : push!(queue, parent)
continue
end
# Examine current subgoal
Expand All @@ -381,7 +384,7 @@ function resolve(goals::Vector{<:Term}, clauses::ClauseTable{T}; options...) wh
if success
@debug string("Done, returning to parent.")
goal.active += 1
push!(queue, goal)
(search==:dfs) ? pushfirst!(queue, goal) : push!(queue, goal)
end
continue
end
Expand All @@ -391,16 +394,23 @@ function resolve(goals::Vector{<:Term}, clauses::ClauseTable{T}; options...) wh
# Iterate across clause set with matching heads
matched_clauses = retrieve_clauses(clauses, term, funcs)
matched = false
local_queue = MutableLinkedList{GoalTree}() # maintain a local queue for the depth first search; the new goals should be added to the global queue in this order to the front
Copy link
Owner

@ztangent ztangent Mar 30, 2022

Choose a reason for hiding this comment

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

I worry about creating a local queue leading to performance slow downs because we're now allocating a queue at every iteration of the search -- is there a way to avoid using a local queue?

for c in matched_clauses
# Freshen variables in clause
c = freshen!(c, Subst(), vcount)
# If term unifies with head of a clause, add it as a subgoal
unifier = unify(term, c.head, occurs_check, funcs)
if isnothing(unifier) continue end
child = GoalTree(c.head, goal, copy(c.body), 1, unifier, vmap)
push!(queue, child)
(search==:dfs) ? push!(local_queue, child) : push!(queue, child)
matched = true
end

#update the global queue with the local one
while (search==:dfs) && length(local_queue) > 0
pushfirst!(queue, pop!(local_queue))
end

Copy link
Owner

@ztangent ztangent Mar 30, 2022

Choose a reason for hiding this comment

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

Instead of pushing each child to the local queue, then transferring the items to the global queue, why we just pushfirst! directly to the global queue?

Copy link
Owner

@ztangent ztangent Mar 30, 2022

Choose a reason for hiding this comment

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

Oh, after giving it more thought, I think I understand why doing it this way leads to different behavior.

Rather than using a local queue though, I think what we can do is replace the line:

for c in matched_clauses

with

for c in Iterators.reverse(matched_clauses)

This will iterate over the matched clauses in reverse order, allowing us to pushfirst! directly to the global queue.

Copy link
Author

@sebdumancic sebdumancic Mar 31, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

Right, this is a much better solution! Better not to change data structures if not necessary.
I was searching for the most efficient data structure for front/back adding, but I like this solution much more.

if !matched @debug string("Failed, no matching clauses.") end
end
# Goals were satisfied if we found valid substitutions
Expand Down