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

Evaluator #47

Draft
wants to merge 102 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
102 commits
Select commit Hold shift + click to select a range
1865d0d
timing benchmarks
matteo-meluzzi Jun 14, 2023
530c278
enumeration benchmarks added
matteo-meluzzi Jun 16, 2023
91fd389
compatibility with 'old' herb
matteo-meluzzi Jun 17, 2023
7d092ee
enumeration tests with constraints
Jun 20, 2023
c6cb6f5
Fix benchmarks without constraints
RobbinBaauw Jun 20, 2023
c74af97
Improve constraints for benchmark
RobbinBaauw Jun 20, 2023
66c9a10
Add extra constraint benchmarks
RobbinBaauw Jun 20, 2023
70a6534
Rename benchmarks to proper name
RobbinBaauw Jun 20, 2023
63934b0
print results in latex
matteo-meluzzi Jun 21, 2023
7cc923a
added a grammar with less terminals
matteo-meluzzi Jun 21, 2023
7ffb1ac
grammars with constraints have correct ioexamples
matteo-meluzzi Jun 21, 2023
603c506
generate benchmarks had typo
matteo-meluzzi Jun 21, 2023
481d30c
added propagation count to result tables
matteo-meluzzi Jun 21, 2023
360c9bb
Prototype Benchmark dataset
THinnerichs Oct 16, 2023
aae71c5
Update prototype string benchmark
THinnerichs Oct 16, 2023
deda1a2
Move data to src
THinnerichs Oct 17, 2023
316d846
remove HerbInterpret from dependencies
THinnerichs Oct 17, 2023
c86af45
Add automatic include of sub-modules
THinnerichs Oct 17, 2023
1956c86
Add attempt at String transformation grammar
ReubenJ Oct 18, 2023
565a0a4
Add automatic include of sub-modules
THinnerichs Oct 17, 2023
be37f30
Reformat Strings transformations
THinnerichs Oct 18, 2023
93aecf2
Reformat Robots
THinnerichs Oct 18, 2023
1440a53
update utilities and dependencies
THinnerichs Oct 18, 2023
60d7ef1
Reformat grammars
THinnerichs Oct 19, 2023
2898fe3
Add bitoperations SyGuS benchmark
THinnerichs Oct 19, 2023
f50307a
Update io functionality
THinnerichs Oct 19, 2023
abf7774
Update fileparsing
THinnerichs Oct 19, 2023
36dafde
Add REadmes and updated IO handling
THinnerichs Nov 1, 2023
d88f113
Added documentation for SyGus's main module
THinnerichs Nov 1, 2023
a785a14
Add ARC benchmark data, grammar and interpret still missing
THinnerichs Nov 1, 2023
1ee9140
add ARC grammar and functions
THinnerichs Nov 6, 2023
3c4b1c7
Include primitives
THinnerichs Nov 6, 2023
1bc73da
Merge branch 'ARC_2019' into dev
THinnerichs Nov 6, 2023
d52a4b4
Update script for parsing ARC data
THinnerichs Nov 6, 2023
6f1c3c5
Add working grammar for String transformations
THinnerichs Nov 7, 2023
99d74e6
Commit merge
THinnerichs Nov 8, 2023
97a9b4c
Finalize Robots dataset
THinnerichs Nov 8, 2023
12ee3a1
Fixed String benchmark
THinnerichs Nov 8, 2023
b079500
Fix Robots benchmark
THinnerichs Nov 9, 2023
028a737
Upload Pixels dataset
THinnerichs Nov 9, 2023
dfd74b9
remove prolog files from Brute
THinnerichs Nov 9, 2023
c0c6a80
Add all examples to working examples
THinnerichs Nov 21, 2023
eaf791d
Fixed @make_public warnings, fixed ARC benchmark
THinnerichs Nov 24, 2023
c8435f5
Fix ARC benchmark typo
THinnerichs Nov 30, 2023
c260835
Clean up main dir, add convenience functions
THinnerichs Dec 14, 2023
ad095ec
Add all_problems functionality and mapping problems to their grammars
THinnerichs Dec 14, 2023
af8130c
Remove all_problems from each module, and substitute it with more gen…
THinnerichs Dec 14, 2023
30fe68c
Make state in Robots mutable
THinnerichs Dec 19, 2023
b6d0e68
Fix robot grammar to include multi-operation programs
Whebon Jan 9, 2024
488d4a7
Merge branch 'dev' of github.com:Herb-AI/HerbBenchmarks.jl into dev
Whebon Jan 9, 2024
6c2ca4d
Make all values actual values
THinnerichs Feb 1, 2024
8376e09
Fix bit function arity and unknown functions
THinnerichs Feb 1, 2024
14f4b5b
Merge pull request #15 from Herb-AI/fix_sygus_symbols
THinnerichs Feb 26, 2024
7206f8c
`HerbData.jl` -> `HerbSpecification.jl`
ReubenJ Feb 23, 2024
08d6c1b
Grammar -> AbstractGrammar according to HerbCore 0.2
THinnerichs Feb 27, 2024
62df519
Update tests to use `HerbSpecification.jl`
ReubenJ Feb 23, 2024
d90a88b
Migrate individual benchmarks to `HerbSpecification.jl`
ReubenJ Mar 4, 2024
c2b3060
Add re-add formatting of 1 IOExample per line
THinnerichs Mar 7, 2024
93f6d26
Merge pull request #22 from Herb-AI/migrate-to-herbspec
THinnerichs Mar 7, 2024
3c08d62
Update `HerbCore` to v0.3.0
ReubenJ Apr 16, 2024
9f2ea49
Move legacy files
stefstef00 Apr 16, 2024
dd47ef0
Extract and extent problem fetching
stefstef00 Apr 16, 2024
f60f174
Move benchmark generator
stefstef00 Apr 16, 2024
77ca727
Rename utils to export module
stefstef00 Apr 16, 2024
c1d1c47
Added unit tests for problem fetcher
stefstef00 Apr 16, 2024
22d6bba
Add Benchmark struct
stefstef00 Apr 16, 2024
39be995
Move file to utils folder
stefstef00 Apr 16, 2024
1ff3fd5
Move module exporter to src folder
stefstef00 Apr 16, 2024
c52d95c
Changed benchmark name type from String to Module
stefstef00 Apr 16, 2024
1c4f28b
Included benchmark type in fetching and added types
stefstef00 Apr 16, 2024
27e9281
Corrected module exports
stefstef00 Apr 16, 2024
8a8d6bf
Fix SyGuS benchmarks
THinnerichs Apr 25, 2024
5b4462b
Merge pull request #25 from Herb-AI/fix_sygus_grammars
ReubenJ Apr 26, 2024
3729b0c
Fix SyGuS string primitive; Fix @all_problem_pairs macro
THinnerichs Apr 26, 2024
77a3b4a
Merge pull request #26 from Herb-AI/fix_string_function_and_problem_m…
ReubenJ Apr 26, 2024
224b8ae
Fix _arg_x indices
THinnerichs May 2, 2024
ab7c99b
Moved benchmark datatype
stefstef00 May 7, 2024
2a15fc3
Added problem grammar pair datatype
stefstef00 May 7, 2024
9c9769f
Added program grammar pair datatype
stefstef00 May 7, 2024
d08b861
Moved benchmark runner
stefstef00 May 7, 2024
c20ec30
Update `HerbGrammar` -> `^0.3.0`
ReubenJ May 14, 2024
50be6f2
Fix SyGuS input arguments issue
THinnerichs May 24, 2024
3db288e
Merge branch 'dev' into restructure
stefstef00 Jun 10, 2024
d1aed0d
Added method to fetch all benchmarks
stefstef00 Jun 10, 2024
01d461b
Moved legacy files to other folder
stefstef00 Jun 10, 2024
cd54863
Removed legacy files
stefstef00 Jun 10, 2024
d3fe79e
Added a debug benchmark
stefstef00 Jun 18, 2024
86cff51
Added docs
stefstef00 Jun 18, 2024
fc78e61
Added evaluation result structures
stefstef00 Jun 18, 2024
71930c0
Added docs
stefstef00 Jun 18, 2024
4e33c7e
Synth function for benchmarks
stefstef00 Jun 18, 2024
b3c49ff
Add evaluation functions
stefstef00 Jun 18, 2024
42530a9
Include everything in the module
stefstef00 Jun 18, 2024
badb074
Added support for selecting specific problem ids
stefstef00 Jun 19, 2024
ac56b84
Added an empty constructor for BenchmarkResult to which results can b…
stefstef00 Jun 20, 2024
eda913b
Added support for storing evaluation results
stefstef00 Jun 20, 2024
3fcc4da
Rename "evaluate" to "evaluate_iterator"
stefstef00 Jun 24, 2024
2577ac5
Added support for regex problem filtering
stefstef00 Jun 24, 2024
7412653
ProblemResult metrics now include SolverStatistics metrics
stefstef00 Jun 24, 2024
dcaa0bf
Added a decomposed synth for easy overloading
stefstef00 Jun 24, 2024
a87325f
A tour of the benchmark evaluator
stefstef00 Jul 2, 2024
e3c3206
Rename
stefstef00 Jul 2, 2024
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
Prev Previous commit
Next Next commit
Add bitoperations SyGuS benchmark
THinnerichs committed Oct 19, 2023
commit 2898fe33b70e0bfeb44fe99b58eb4e5a703f4c03
2 changes: 1 addition & 1 deletion src/data/Robots_2020/Robots_2020.jl
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@ module Robots_2020
using HerbData

include("data.jl")
include("Data_generation.jl")
include("data_generation.jl")

generated_data_path = "generated_data.jl"
if isfile(generated_data_path)
File renamed without changes.
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
module String_transformations_2020

using HerbCore
using HerbData
using HerbGrammar

include("data.jl")

70 changes: 70 additions & 0 deletions src/data/SyGuS/PBE_BV_Track_2018/PBE_BV_Track_2018.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
module PBE_BV_Track_2018

using HerbCore
using HerbData
using HerbGrammar

include("data.jl")
include("grammars.jl")

include("bit_functions.jl")

export
format_bit_operations_grammars


function format_bit_operations_grammars(filename::AbstractString)
lines::Vector{String} = []
file = open(filename, "r")

for line in eachline(file)
if !isempty(line) && occursin(" = ", line)
split_line = split(line, " = ")

# Check for grammar definition
if occursin("@cfgrammar", split_line[2])
line = replace(line, "-", "_")
else
if startswith(split_line[2], 'x')
line = "$(split_line[1]) = _arg_1"
end
if startswith(split_line[2], '(')
symbol_list = split(split_line[2][2:end-1], ' ')
func = replace(symbol_list[1],
"bvneg" => "bvneg_cvc",
"bvnot" => "bvnot_cvc",
"bvadd" => "bvadd_cvc",
"bvsub" => "bvsub_cvc",
"bvxor" => "bvxor_cvc",
"bvand" => "bvand_cvc",
"bvor" => "bvor_cvc",
"bvshl" => "bvshl_cvc",
"bvlshr" => "bvlshr_cvc",
"bvashr" => "bvashr_cvc",
"bvnand" => "bvnand_cvc",
"bvnor" => "bvnor_cvc",
"ehad" => "ehad_cvc",
"arba" => "arba_cvc",
"shesh" => "shesh_cvc",
"smol" => "bvnor_cvc",
"im" => "im_cvc",
)

expr = func * "(" * join(symbol_list[2:end], ", ") * ")"

line = "$(split_line[1]) = $(expr)"
end
end
end
push!(lines, line)
end
close(file)

file = open(filename, "w")
for line in lines
println(file, line)
end
close(file)
end

end # module PBE_BV_Track_2018
22 changes: 22 additions & 0 deletions src/data/SyGuS/PBE_BV_Track_2018/bit_functions.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
# Defined in SMT-LIB

bvneg_cvc(n::UInt) = -n
bvnot_cvc(n::UInt) = ~n
bvadd_cvc(n1::UInt, n2::UInt) = n1 + n2
bvsub_cvc(n1::UInt, n2::UInt) = n1 - n2
bvxor_cvc(n1::UInt, n2::UInt) = n1 n2 #xor
bvand_cvc(n1::UInt, n2::UInt) = n1 & n2
bvor_cvc(n1::UInt, n2::UInt) = n1 | n2
bvshl_cvc(n1::UInt, n2::Int) = n1 << n2
bvlshr_cvc(n1::UInt, n2::Int) = n1 >>> n2
bvashr_cvc(n1::UInt, n2::Int) = n1 >> n2
bvnand_cvc(n1::UInt, n2::UInt) = n1 n2 #nand
bvnor_cvc(n1::UInt, n2::UInt) = n1 n2 #nor

# CUSTOM functions

ehad_cvc(n::UInt) = bvlshr_cvc(n, 1)
arba_cvc(n::UInt) = bvlshr_cvc(n, 4)
shesh_cvc(n::UInt) = bvlshr_cvc(n, 16)
smol_cvc(n::UInt) = bvshl_cvc(n, 1)
im_cvc(x::UInt, y::UInt, z::UInt) = x == UInt(1) ? y : z
188,592 changes: 188,592 additions & 0 deletions src/data/SyGuS/PBE_BV_Track_2018/data.jl

Large diffs are not rendered by default.

11,298 changes: 11,298 additions & 0 deletions src/data/SyGuS/PBE_BV_Track_2018/grammars.jl

Large diffs are not rendered by default.

134 changes: 65 additions & 69 deletions src/data/SyGuS/PBE_SLIA_Track_2019/PBE_SLIA_Track_2019.jl
Original file line number Diff line number Diff line change
@@ -1,81 +1,77 @@
module PBE_SLIA_Track_2019

using HerbData
using HerbCore
using HerbData
using HerbGrammar

using SExpressions

# include("data.jl")

export
parse_sygus_grammar,
parse_sygus_problem,
parse_synth_fun,
parse_example_constraint


function parse_sygus_grammar(filename::AbstractString)::Grammar
symbol_list = SExpressions.Parser.parsefile(filename)
grammar = Nothing

for expr in symbol_list
if expr[1] == Symbol("synth-fun")
return parse_synth_fun(expr)
include("data.jl")
include("grammars.jl")

include("string_functions.jl")

export
format_string_grammars


function format_string_grammars(filename::AbstractString)
lines::Vector{String} = []
file = open(filename, "r")

for line in eachline(file)
if !isempty(line) && occursin(" = ", line)
split_line = split(line, " = ")

# Check for grammar definition
if occursin("@cfgrammar", split_line[2])
line = replace(line, "-" => "_")
elseif length(split_line) == 1 # check for empty right side
line *= "\"\""
else
if (occursin("ntString", split_line[1])
&& !startswith(split_line[2], '(')
&& !occursin('"', split_line[2])
&& !occursin("_arg", split_line[2]))
line = "$(split_line[1]) = \"$(split_line[2])\""
end
if startswith(split_line[2], '(')
symbol_list = split(split_line[2][2:end-1], ' ')
func = replace(symbol_list[1],
"str.++" => "concat_cvc",
"str.replace" => "replace_cvc",
"str.at" => "at_cvc",
"int.to.str" => "int_to_str_cvc",
"str.substr" => "substr_cvc",
"str.len" => "len_cvc",
"str.to.int" => "str_to_int_cvc",
"str.indexof" => "indexof_cvc",
"str.prefixof" => "prefixof_cvc",
"str.suffixof" => "suffixof_cvc",
"str.contains" => "contains_cvc",
"str.<" => "lt_cvc",
"str.<=" => "leq_cvc",
"str.isdigit" => "isdigit_cvc",
)
if func ["=", "+", "-"]
func = func == "=" ? "==" : func
expr = symbol_list[2] * " $(func) " * symbol_list[3]
elseif func == "ite"
expr = "$(symbol_list[2]) ? $(symbol_list[3]) : $(symbol_list[4])"
else
expr = func * "(" * join(symbol_list[2:end], ", ") * ")"
end
line = "$(split_line[1]) = $(expr)"
end
end
end
push!(lines, line)
end
close(file)

throw(ArgumentError("No grammar found in '$filename'"))
end

function parse_sygus_problem(filename::AbstractString)::Problem
symbol_list = SExpressions.Parser.parsefile(filename)
examples::Vector{Example} = Vector{Example}()

for expr in symbol_list
if expr[1] == Symbol("constraint") && expr[2][1] == :(=)
push!(examples, parse_example_constraint(expr))
end
file = open(filename, "w")
for line in lines
println(file, line)
end
return Problem(examples)
end

function parse_synth_fun(sexpr::SExpressions.Lists.Cons)::Grammar
return_grammar = @cfgrammar begin end

if sexpr[1] !== Symbol("synth-fun")
throw(ArgumentError("'$(sexpr[1])' is not a 'synth-fun'"))
end

for rule in sexpr[5]
for val in rule[3]
add_rule!(return_grammar, :($(rule[1]) = $(val)))
end
end

return return_grammar
end


"""
Parses SyGuS example of the form (constraint (= (f arg1 arg2 ...) output)).
Returns IOExample with inputs named arg1, arg2, ...
"""
function parse_example_constraint(sexpr::SExpressions.Lists.Cons)
# take the X of (constraint X)
sexpr = sexpr[2]
# take Function call and Output of (= FunctionCall Output)
functionCall = sexpr[2]
output = sexpr[3]

inputs = Dict{Symbol,Any}()

for arg_index in 2:length(functionCall)
inputs[Symbol("arg$(arg_index-1)")] = functionCall[arg_index]
end

return IOExample(inputs, output)
close(file)
end

end # module PBE_SLIA_Track_2019
724 changes: 362 additions & 362 deletions src/data/SyGuS/PBE_SLIA_Track_2019/data.jl

Large diffs are not rendered by default.

830 changes: 415 additions & 415 deletions src/data/SyGuS/PBE_SLIA_Track_2019/grammars.jl

Large diffs are not rendered by default.

33 changes: 0 additions & 33 deletions src/data/SyGuS/PBE_SLIA_Track_2019/run.jl

This file was deleted.

33 changes: 33 additions & 0 deletions src/data/SyGuS/PBE_SLIA_Track_2019/string_functions.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
# CVC5 functions

## String typed
concat_cvc(str1::String, str2::String) = str1 * str2

replace_cvc(mainstr::String, to_replace::String, replace_with::String) = replace(mainstr, to_replace => replace_with)

at_cvc(str::String, index::Int) = str[index]

int_to_str_cvc(n::Int) = "$n"

substr_cvc(str::String, start_index::Int, end_index::Int) = str[start_index:end_index]

# Int typed
len_cvc(str::String) = length(str)

str_to_int_cvc(str::String) = parse(Int64, str)

indexof_cvc(str::String, substring::String, index::Int) = (n = findfirst(str, substring); n == nothing ? -1 : (n[1] >= index ? -1 : n[1]))

# Bool typed
prefixof_cvc(prefix::String, str::String) = startswith(str, prefix)

suffixof_cvc(suffix::String, str::String) = endswith(str, suffix)

contains_cvc(str::String, contained::String) = contains(str, contained)

lt_cvc(str1::String, str2::String) = cmp(str1, str2) < 0

leq_cvc(str1::String, str2::String) = cmp(str1, str2) <= 0

isdigit_cvc(str::String) = tryparse(Int, str) !== nothing

80 changes: 80 additions & 0 deletions src/data/SyGuS/SyGuS.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
module SyGuS

using HerbData
using HerbCore
using HerbGrammar

using SExpressions


export
parse_sygus_grammar,
parse_sygus_problem,
parse_synth_fun,
parse_example_constraint


function parse_sygus_grammar(filename::AbstractString)::Grammar
symbol_list = SExpressions.Parser.parsefile(filename)
grammar = Nothing

for expr in symbol_list
if expr[1] == Symbol("synth-fun")
return parse_synth_fun(expr)
end
end

throw(ArgumentError("No grammar found in '$filename'"))
end

function parse_sygus_problem(filename::AbstractString)::Problem
symbol_list = SExpressions.Parser.parsefile(filename)
examples::Vector{Example} = Vector{Example}()

for expr in symbol_list
if expr[1] == Symbol("constraint") && expr[2][1] == :(=)
push!(examples, parse_example_constraint(expr))
end
end
return Problem(examples)
end

function parse_synth_fun(sexpr::SExpressions.Lists.Cons)::Grammar
return_grammar = @cfgrammar begin end

if sexpr[1] !== Symbol("synth-fun")
throw(ArgumentError("'$(sexpr[1])' is not a 'synth-fun'"))
end

for rule in sexpr[5]
for val in rule[3]
add_rule!(return_grammar, :($(rule[1]) = $(val)))
end
end

return return_grammar
end


"""
Parses SyGuS example of the form (constraint (= (f arg1 arg2 ...) output)).
Returns IOExample with inputs named arg1, arg2, ...
"""
function parse_example_constraint(sexpr::SExpressions.Lists.Cons)
# take the X of (constraint X)
sexpr = sexpr[2]
# take Function call and Output of (= FunctionCall Output)
functionCall = sexpr[2]
output = sexpr[3]

inputs = Dict{Symbol,Any}()

for arg_index in 2:length(functionCall)
inputs[Symbol("_arg_$(arg_index-1)")] = functionCall[arg_index]
end

return IOExample(inputs, output)
end

end # module SyGuS
9 changes: 9 additions & 0 deletions src/data/SyGuS/citation.bib
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
@misc{SyGuS2019,
author = {Padhi, Saswat and Abhishek, Udupa and Fu, Andi and Polgreen, Elizabeth and Reynolds, Andrew},
title = {Benchmarks for SyGuS Competition},
year = {2019},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/SyGuS-Org/benchmarks}},
commit = {13c8deb68a873635879c9a69bc78caebd340f646}
}