Skip to content

Commit

Permalink
Merge pull request #20 from Herb-AI/feat/value-equality
Browse files Browse the repository at this point in the history
Value equality
  • Loading branch information
ReubenJ authored Nov 15, 2024
2 parents 9d06378 + 947278c commit d30a745
Show file tree
Hide file tree
Showing 4 changed files with 50 additions and 11 deletions.
2 changes: 2 additions & 0 deletions Project.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ authors = ["Tilman Hinnerichs <[email protected]>"]
version = "0.1.1"

[deps]
AutoHashEquals = "15f4f7f2-30c1-5605-9d31-71845cf9641f"

[compat]
AutoHashEquals = "2.1,2.2"
julia = "1.8"
2 changes: 2 additions & 0 deletions src/HerbSpecification.jl
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module HerbSpecification

using AutoHashEquals

include("problem.jl")

export
Expand Down
14 changes: 6 additions & 8 deletions src/problem.jl
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ An input-output example.
`in` is a [`Dict`](@ref) of `{Symbol,Any}` where the symbol represents a variable in a program.
`out` can be anything.
"""
struct IOExample{InType, OutType}
@auto_hash_equals struct IOExample{InType, OutType}
in::Dict{Symbol, InType}
out::OutType
end
Expand All @@ -16,7 +16,7 @@ end
A trace defining a wanted program execution for program synthesis.
@TODO combine with Gen.jl
"""
struct Trace{T}
@auto_hash_equals struct Trace{T}
exec_path::Vector{T}
end

Expand All @@ -27,7 +27,7 @@ abstract type AbstractFormalSpecification end
A specification based on a logical formula defined by a SMT solver.
"""
struct SMTSpecification{F} <: AbstractFormalSpecification
@auto_hash_equals struct SMTSpecification{F} <: AbstractFormalSpecification
formula::F
end

Expand All @@ -46,7 +46,7 @@ abstract type AbstractDependentTypeSpecification <: AbstractTypeSpecification en
Defines a specification
"""
struct AgdaSpecification{F} <: AbstractDependentTypeSpecification
@auto_hash_equals struct AgdaSpecification{F} <: AbstractDependentTypeSpecification
formula::F
end

Expand All @@ -65,7 +65,7 @@ Program synthesis problem defined by an [`AbstractSpecification`](@ref)s. Has a
!!! warning
Please care that concrete `Problem` types with different values of `T` are never subtypes of each other.
"""
struct Problem{T <: AbstractSpecification}
@auto_hash_equals struct Problem{T <: AbstractSpecification}
name::AbstractString
spec::T

Expand All @@ -82,7 +82,7 @@ end
Program synthesis problem defined by an specification and a metric. The specification has to be based on input/output examples, while the function needs to return a numerical value.
"""
struct MetricProblem{T <: AbstractVector{<:IOExample}, F}
@auto_hash_equals struct MetricProblem{T <: AbstractVector{<:IOExample}, F}
name::AbstractString
cost_function::F
spec::T
Expand All @@ -105,5 +105,3 @@ Overwrite `Base.getindex` to allow for slicing of input/output-based problems.
"""
Base.getindex(p::Problem{<:AbstractVector{<:IOExample}}, indices) = Problem(p.name, p.spec[indices])
Base.getindex(p::MetricProblem{<:AbstractVector{<:IOExample}}, indices) = MetricProblem(p.name, p.cost_function, p.spec[indices])


43 changes: 40 additions & 3 deletions test/test_ioproblem.jl
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,37 @@

@test io_example.in == input_dict
@test io_example.out == output_value
@testset "Test Equality" begin
e₁ = IOExample(Dict(:x => 1), 1)
e₂ = IOExample(Dict(:x => 1), 1)
@test e₁ == e₂
end
end

@testset "Trace Tests" begin
t₁ = Trace([:x => 1, :x => 2, :x => 3])
t₂ = Trace([:x => 1, :x => 2, :x => 3])
@test t₁ == t₂
end

@testset "SMTSpecification Tests" begin
example_formula = identity
smt₁ = SMTSpecification(example_formula)
smt₂ = SMTSpecification(example_formula)
@test smt₁ == smt₂
end

@testset "AgdaSpecification Tests" begin
example_formula = identity
agda₁ = AgdaSpecification(example_formula)
agda₂ = AgdaSpecification(example_formula)
@test agda₁ == agda₂
end

# Tests for Problem
@testset "Problem Tests" begin
# Example specs to use in the below tests.
specs = [
[
[
IOExample(Dict(:var1 => 1, :var2 => 2), 3),
IOExample(Dict(:var1 => 4, :var2 => 5), 6),
IOExample(Dict(:var1 => 7, :var2 => 8), 9),
Expand Down Expand Up @@ -50,6 +74,12 @@ end
@test subproblem.name == problem_name
end
end

@testset "Test Equality" begin
p₁ = Problem([IOExample(Dict(:x => 1), 1)])
p₂ = Problem([IOExample(Dict(:x => 1), 1)])
@test p₁ == p₂
end
end

# Tests for MetricProblem
Expand Down Expand Up @@ -87,5 +117,12 @@ end
@test isa(submetric2, MetricProblem)
@test submetric2.spec == spec[2:3]
@test submetric2.name == name
@test submetric2.cost_function === cost_function
@test submetric2.cost_function === cost_function

@testset "Test Equality" begin
cost_function = () -> 1
mp₁ = MetricProblem(cost_function , [IOExample(Dict(:x => 1), 1)])
mp₂ = MetricProblem(cost_function , [IOExample(Dict(:x => 1), 1)])
@test mp₁ == mp₂
end
end

0 comments on commit d30a745

Please sign in to comment.