Update interpret_sygus

Author: THinnerichs

src/data/SyGuS/PBE_SLIA_Track_2019/string_functions.jl

@@ -32,26 +32,13 @@ leq_cvc(str1::String, str2::String) = cmp(str1, str2) <= 0
 
 isdigit_cvc(str::String) = tryparse(Int, str) !== nothing
 
+
 """
-Gets the relevant symbol to easily match grammar rules to operations in `interpret` function
-"""
-function get_relevant_tags(grammar::ContextSensitiveGrammar)
-        tags = Dict{Int,Any}()
-        for (ind, r) in pairs(grammar.rules)
-                tags[ind] = if typeof(r) != Expr
-                        r
-                else
-                        @match r.head begin
-                                :block => :OpSeq
-                                :call => r.args[1]
-                                :if => :IF
-                        end
-                end
-        end
-        return tags
-end
+    interpret_sygus(prog::AbstractRuleNode, grammar_tags::Dict{Int,Any}, input::Dict{Symbol,Any})
 
-function interpret_sygus(prog::AbstractRuleNode, grammar_tags::Dict{Int,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)
 
@@ -74,6 +61,16 @@ function interpret_sygus(prog::AbstractRuleNode, grammar_tags::Dict{Int,Any})
 
         :IF => interpret_sygus(c[1], grammar_tags) ? interpret_sygus(c[2], grammar_tags) : interpret_sygus(c[3], grammar_tags)
 
-        _ => grammar_tags[r]
+        _ =>
+            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