Use new intepret generator

Author: THinnerichs

Project.toml

@@ -7,6 +7,7 @@ version = "0.2.3"
 FilePathsBase = "48062228-2e41-5def-b9a4-89aafe57970f"
 HerbCore = "2b23ba43-8213-43cb-b5ea-38c12b45bd45"
 HerbGrammar = "4ef9e186-2fe5-4b24-8de7-9f7291f24af7"
+HerbInterpret = "5bbddadd-02c5-4713-84b8-97364418cca7"
 HerbSpecification = "6d54aada-062f-46d8-85cf-a1ceaf058a06"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078"
@@ -17,6 +18,7 @@ Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
 [compat]
 HerbCore = "^0.3.0"
 HerbGrammar = "0.6"
+HerbInterpret = "0.2.1"
 HerbSpecification = "^0.2.0"
 ParserCombinator = "2.2.1"
 julia = "^1.8"

src/data/SyGuS/PBE_SLIA_Track_2019/string_functions.jl

@@ -31,46 +31,3 @@ 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
-
-
-"""
-    interpret_sygus(prog::AbstractRuleNode, grammar_tags::Dict{Int,Any}, input::Dict{Symbol,Any})
-
-Custom intepret function for the SyGuS SLIA benchmark.
-"""
-function interpret_sygus(prog::AbstractRuleNode, grammar_tags::Dict{Int,Any}, input::Dict{Symbol,Any})
-    r = get_rule(prog)
-    c = get_children(prog)
-
-    MLStyle.@match grammar_tags[r] begin
-        :concat_cvc => concat_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags))
-        :replace_cvc => replace_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags), interpret_sygus(c[3], grammar_tags))
-        :at_cvc => at_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags))
-        :int_to_str_cvc => int_to_str_cvc(interpret_sygus(c[1], grammar_tags))
-        :substr_cvc => substr_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags), interpret_sygus(c[3], grammar_tags))
-        :len_cvc => len_cvc(interpret_sygus(c[1], grammar_tags))
-        :str_to_int_cvc => str_to_int_cvc(interpret_sygus(c[1], grammar_tags))
-        :indexof_cvc => indexof_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags), interpret_sygus(c[3], grammar_tags))
-        :prefixof_cvc => prefixof_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags))
-        :suffixof_cvc => suffixof_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags))
-        :contains_cvc => contains_cvc(interpret_sygus(c[1], grammar_tags), interpret_sygus(c[2], grammar_tags))
-
-        :+ => interpret_sygus(c[1], grammar_tags) + interpret_sygus(c[2], grammar_tags)
-        :- => interpret_sygus(c[1], grammar_tags) - interpret_sygus(c[2], grammar_tags)
-        :(==) => interpret_sygus(c[1], grammar_tags) == interpret_sygus(c[2], grammar_tags)
-
-        :IF => interpret_sygus(c[1], grammar_tags) ? interpret_sygus(c[2], grammar_tags) : interpret_sygus(c[3], grammar_tags)
-
-        _ =>
-            begin
-                tag = grammar_tags[r]
-                if tag isa Symbol && occursin("_arg_", String(tag))
-                    # This is an input variable; look it up in the environment
-                    return input[tag]
-                else
-                    # default behavior
-                    return tag
-                end
-            end
-    end
-end