Iterator doesn't iterate?

[THinnerichs]

I am trying to generate programs over a specific benchmark. As the grammar is too wide, I am using constraints to find only programs that contain the input.

Setup

The benchmark

module BUSTLE_benchmark

using HerbGrammar
using HerbBenchmarks
using HerbBenchmarks.PBE_SLIA_Track_2019

grammar_bustle_SLIA = @cfgrammar begin
    Start = ntString | ntInt | ntBool

    # String expressions
    ntString = "" | " " | "," | "." | "!" | "?" | "(" | ")" | "[" | "]" | "<" | ">" | "{" | "}" | "-" | "+" | "_" | "/" | "\$" | "#" | ":" | ";" | "@" | "%" | "0"
    ntString = concat_cvc(ntString, ntString)
    ntString = left_bustle(ntString, ntInt)
    ntString = right_bustle(ntString, ntInt)
    ntString = substr_cvc(ntString, ntInt, ntInt)
    ntString = replace_bustle(ntString, ntInt, ntInt, ntString) #BUSTLE replace
    ntString = trim_bustle(ntString) # BUSTLE trim
    ntString = repeat(ntString, ntInt) #BUSTLE repeat
    ntString = substitute_bustle(ntString, ntString, ntString) #BUSTLE Substitute
    ntString = substitute_bustle(ntString, ntString, ntString, ntInt) #BUSTLE Substitute
    ntString = int_to_str_cvc(ntInt) #BUSTLE ToText
    ntString = lowercase(ntString)
    ntString = uppercase(ntString)
    ntString = capitalize_bustle(ntString)
    ntString = ntBool ? ntString : ntString
    ntString = Input
    Input = _arg_1
    Input = _arg_2
    Input = _arg_3
    Input = _arg_4

    # Integer expressions
    ntInt = 0 | 1 | 2 | 3 | 99 
    ntInt = ntInt + ntInt
    ntInt = ntInt - ntInt
    ntInt = indexof_cvc(ntString, ntString, nothing)
    ntInt = indexof_cvc(ntString, ntString, ntInt)
    ntInt = len_cvc(ntString)
    ntInt = Int(Input)

    ntBool = ntString == ntString
    ntBool = ntInt > ntInt
    ntBool = ntInt >= ntInt
end

capitalize_bustle(s::String) = join(uppercasefirst.(split(s)), " ")
replace_bustle(s1::String, i1::Int, i2::Int, s2::String) = replace_cvc(s1, substr_cvc(s1, i1, i2), s2)
left_bustle(s::String, i::Int) = s[1:i]
right_bustle(s::String, i::Int) = s[end-i+1:end]
trim_bustle(s::String) = strip(s)
substitute_bustle(s::String, to_replace::String, replace_by::String, count::Int) = replace(s, to_replace => replace_by, count=count)
substitute_bustle(s::String, to_replace::String, replace_by::String) = replace(s, to_replace => replace_by)

export 
    grammar_bustle_SLIA,

    capitalize_bustle, 
    replace_bustle,
    left_bustle,
    right_bustle,

    trim_bustle, 
    substitute_bustle,

    concat_cvc, 
    substr_cvc, 
    int_to_str_cvc, 
    indexof_cvc, 
    indexof_cvc, 
    len_cvc
end

function get_all_problem_grammar_pairs(BUSTLE_benchmark)
    problems = get_all_problems(HerbBenchmarks.PBE_SLIA_Track_2019)  
    return [ProblemGrammarPair(BUSTLE_benchmark, problem.name, problem, grammar_bustle_SLIA) for problem in problems]
end

(re-implementation of the BUSTLE grammar for SyGuS)

Then I run

julia> grammar = BUSTLE_benchmark.grammar_bustle_SLIA
1: Start = ntString
2: Start = ntInt
3: Start = ntBool
4: ntString =
5: ntString =
6: ntString = ,
7: ntString = .
8: ntString = !
9: ntString = ?
10: ntString = (
11: ntString = )
12: ntString = [
13: ntString = ]
14: ntString = <
15: ntString = >
16: ntString = {
17: ntString = }
18: ntString = -
19: ntString = +
20: ntString = _
21: ntString = /
22: ntString = $
23: ntString = #
24: ntString = :
25: ntString = ;
26: ntString = @
27: ntString = %
28: ntString = 0
29: ntString = concat_cvc(ntString, ntString)
30: ntString = left_bustle(ntString, ntInt)
31: ntString = right_bustle(ntString, ntInt)
32: ntString = substr_cvc(ntString, ntInt, ntInt)
33: ntString = replace_bustle(ntString, ntInt, ntInt, ntString)
34: ntString = trim_bustle(ntString)
35: ntString = repeat(ntString, ntInt)
36: ntString = substitute_bustle(ntString, ntString, ntString)
37: ntString = substitute_bustle(ntString, ntString, ntString, ntInt)
38: ntString = int_to_str_cvc(ntInt)
39: ntString = lowercase(ntString)
40: ntString = uppercase(ntString)
41: ntString = capitalize_bustle(ntString)
42: ntString = if ntBool
    ntString
else
    ntString
end
43: ntString = Input
44: Input = _arg_1
45: Input = _arg_2
46: Input = _arg_3
47: Input = _arg_4
48: ntInt = 0
49: ntInt = 1
50: ntInt = 2
51: ntInt = 3
52: ntInt = 99
53: ntInt = ntInt + ntInt
54: ntInt = ntInt - ntInt
55: ntInt = indexof_cvc(ntString, ntString, nothing)
56: ntInt = indexof_cvc(ntString, ntString, ntInt)
57: ntInt = len_cvc(ntString)
58: ntInt = Int(Input)
59: ntBool = ntString == ntString
60: ntBool = ntInt > ntInt
61: ntBool = ntInt >= ntInt

Then I add constraints to contain the inputs

julia> for i in 1:3
           addconstraint!(grammar, Contains(findfirst(rule -> occursin("_arg_$i", string(rule)), grammar.rules)))
       end

which gives me the correct Contains constraints.

Now I init my iterator.

 iter = DFSIterator(grammar, :Start, max_depth=8)

(Also doesn't work with BFSIterator and RandomSearchIterator.

Issue

Now when I try to run it with

 julia> for h in iter
           println(rulenode2expr(h, grammar))
       end

or with iterate(iter), I do not get a single program. However, if I only add 2 constraints using for i in 1:2 instead (see above), I get all the programs I need.

If I use the regular SyGuS.SLIA grammar for this problem everything works flawlessly. Maybe its the grammar width?

[ReubenJ]

When you say you don't get a single program, are you saying the iterator is fully exhausted without a single program? Or is it just that it doesn't find any program quickly?

[Whebon]

It gets stuck in search and doesn't terminate.

I think the issue is that the program space is too large. For max_depth = 3, there are already 115643 programs. For max_depth= 4, I had to kill the search at ~100s millions of programs. So max_depth= 8 is not feasible.

Especially a DFS is very tough, because then the first UniformTree to iterate over is already very large.

[Whebon]

Example of the issue

One of the UniformTrees we iterate over is:

replace_bustle(substitute_bustle(tS, tS, tS, tI), len_cvc(tS), Int(Input), Input) Where tS is one of the 25 terminal strings. Where tI is one of the 3 terminal integers. Where Input is one of the 4 inputs. Making for a total of 25*25*25*3*25*4*4 = 18750000 complete programs.

However, since we enforce 3 contains constraints for 3 different Inputs, 0 of these programs are actually valid.

Unfortunately, this deduction can not be made until one of the 2 Input holes is filled. The hole heuristic is set to left-most, so we will first enumerate all combinations of tS, tS, tS, tI, tS, before we fill in one an Input to conclude the tree is infeasible. In other words, we do a lot of work just to conclude the entire uniform tree is infeasible.

Possible Solution

Implement a ContainsAll([44, 45, 46]) constraint that can immediately recognize that replace_bustle(substitute_bustle(tS, tS, tS, tI), len_cvc(tS), Int({44, 45, 46, 47}), {44, 45, 46, 47}) is infeasible.

[Whebon]

You say it also doesn't work with BFSIterator, but I do get some programs that way (until it starts to attempt to enumerate large invalid uniform trees like in the example above).

[THinnerichs]

When you say you don't get a single program, are you saying the iterator is fully exhausted without a single program? Or is it just that it doesn't find any program quickly?

It doesn't return any program at all for me. Speaking code:

julia> for h in iter
          println(rulenode2expr(h, grammar))
      end

never prints anything.

[THinnerichs]

You say it also doesn't work with BFSIterator, but I do get some programs that way (until it starts to attempt to enumerate large invalid uniform trees like in the example above).

Hm, that is odd. I literally get no solution at all running it for 30s. No additional constraints, plain setup as above.