Update ASP solver and fully test it

Author: Issa Hanou

src/HerbConstraints.jl

@@ -59,10 +59,6 @@ include("solver/uniform_solver/uniform_solver.jl")
 include("solver/uniform_solver/uniform_treemanipulations.jl")
 include("solver/domainutils.jl")
 
-include("solver/uniform_solver/asp/asp_tree_transformations.jl")
-include("solver/uniform_solver/asp/asp_constraint_transformations.jl")
-include("solver/uniform_solver/asp/asp_uniform_tree_solver.jl")
-
 include("patternmatch.jl")
 include("lessthanorequal.jl")
 include("makeequal.jl")
@@ -81,6 +77,10 @@ include("grammarconstraints/contains_subtree.jl")
 include("grammarconstraints/forbidden_sequence.jl")
 include("grammarconstraints/unique.jl")
 
+include("solver/uniform_solver/asp/asp_tree_transformations.jl")
+include("solver/uniform_solver/asp/asp_constraint_transformations.jl")
+include("solver/uniform_solver/asp/asp_uniform_tree_solver.jl")
+
 export
     AbstractGrammarConstraint,
     AbstractLocalConstraint,

src/solver/uniform_solver/asp/asp_constraint_transformations.jl

@@ -95,6 +95,7 @@ is_smaller(X,Y) :- node(X,XV), node(Y,YV), XV = YV, S = #sum {Z: child(X,Z,XC),
 :- node(X1,5),child(X1,1,X),child(X1,2,Y),child(X1,3,Z) not is_smaller(Y,Z).
 """
 function to_ASP(grammar::AbstractGrammar, constraint::Ordered, constraint_index::Int64)
+    # TODO use order property of constraint
     output = "is_smaller(X,Y) :- node(X,XV),node(Y,YV),XV < YV.\n"
     output *= "is_smaller(X,Y) :- node(X,XV),node(Y,YV),XV = YV,S = #sum { Z : child(X,Z,XC),child(Y,Z,YC),is_smaller(XC,YC) }, M = #max { Z : child(X,Z,XC) }, S = M.\n"
 

src/solver/uniform_solver/asp/asp_uniform_tree_solver.jl

@@ -1,23 +1,64 @@
-struct ASPSolver <: Solver
+using Clingo_jll
+
+mutable struct ASPSolver <: Solver
     grammar::AbstractGrammar
-    tree::Union{RuleNode,StateHole}
+    tree::Union{RuleNode,UniformHole,StateHole}
     solutions::Vector{Dict{Int64,Int64}} #vector of dictionaries with key=node and value=matching rule index
-    tmp_file_name::String
+    isfeasible::Bool
+    statistics::Union{TimerOutput, Nothing}
+end
+
+"""
+    ASPSolver(grammar::AbstractGrammar, fixed_shaped_tree::AbstractRuleNode)
+"""
+function ASPSolver(grammar::AbstractGrammar, fixed_shaped_tree::AbstractRuleNode; with_statistics=false)
+    @assert !contains_nonuniform_hole(fixed_shaped_tree) "$(fixed_shaped_tree) contains non-uniform holes"
+    statistics = @match with_statistics begin
+        ::TimerOutput => with_statistics
+        ::Bool => with_statistics ? TimerOutput("ASP Solver") : nothing
+        ::Nothing => nothing
+    end
+    solver = ASPSolver(grammar, fixed_shaped_tree,  Vector{Dict{Int32,Int32}}(), false, statistics)
+    solve(solver)
+    return solver
 end
 
 get_name(::ASPSolver) = "ASPSolver"
 
-get_tree(solver::ASPSolver) = solver.tree
+"""
+    get_grammar(solver::ASPSolver)
+
+Get the grammar.
+"""
+function get_grammar(solver::ASPSolver)::AbstractGrammar
+    return solver.grammar
+end
 
-get_grammar(solver::ASPSolver) = solver.grammar
+"""
+    get_tree(solver::ASPSolver)
+
+Get the root of the tree. This remains the same instance throughout the entire search.
+"""
+function get_tree(solver::ASPSolver)::AbstractRuleNode
+    return solver.tree
+end
 
-get_filename(solver::ASPSolver) = solver.tmp_file_name
+"""
+    isfeasible(solver::ASPSolver)
 
-get_resultsfile(solver::ASPSolver) = replace(get_filename(solver), ".lp" => "_res.lp")
+Returns true if no inconsistency has been detected.
+"""
+function isfeasible(solver::ASPSolver)
+    return solver.isfeasible
+end
 
-ASPSolver(grammar, tree) = ASPSolver(grammar, tree, Vector{Dict{Int32,Int32}}(), "__tmp_asp_file.lp")
+"""
+    solve(solver::ASPSolver)
 
-function solve(solver::ASPSolver, write_to_file::Bool=false)
+Generate all solutions for the given tree using ASP solver Clingo.
+"""
+function solve(solver::ASPSolver)
+    @timeit_debug solver.statistics "generate ASP tree" begin end
     string_tree, _ = tree_to_ASP(get_tree(solver), get_grammar(solver), 1)
     constraints = to_ASP(get_grammar(solver))
     asp_input = """
@@ -32,37 +73,31 @@ $constraints
 """
     buffer = IOBuffer(asp_input)
     asp_output = IOBuffer()
+    @timeit_debug solver.statistics "run Clingo" begin end
     run(pipeline(ignorestatus(`$(Clingo_jll.clingo()) --models 0`), stdin=buffer, stdout=asp_output))
     extract_solutions(solver, split(String(take!(asp_output)), "\n"))
-    if write_to_file
-        # Write the asp program to a file
-        open(get_filename(solver), "w") do file
-            write(file, String(take!(buffer)))
-        end
-        # Write the asp output to a file
-        open(get_resultsfile(solver), "w") do file
-            write(file, String(take!(asp_output)))
-        end
-    end
-end
-
-function extract_solutions_from_file(solver::ASPSolver)
-    open(get_resultsfile(solver), "r") do file
-        extract_solutions(solver, eachline(file))
-    end
 end
 
+"""
+    extract_solutions(solver::ASPSolver, output_lines)
+Extract solutions from the output of Clingo and store them in the `solutions` field of the solver.
+"""
 function extract_solutions(solver::ASPSolver, output_lines)
-    current_solution = Dict{Int64,Int64}()
+    @timeit_debug solver.statistics "extract solutions" begin end
     for line in output_lines
         if startswith(line, "node")
+            current_solution = Dict{Int64,Int64}()
             node_assignments = split(line, " ")
             for node in node_assignments
                 m = match(r"node\((\d+),(\d+)\)", node)
                 current_solution[parse(Int, m.captures[1])] = parse(Int, m.captures[2])
             end
             push!(solver.solutions, current_solution)
         elseif startswith(line, "SATISFIABLE")
+            solver.isfeasible = true
+            break
+        elseif startswith(line, "UNSATISFIABLE")
+            solver.isfeasible = false
             break
         end
     end

test/test_asp_solver.jl

@@ -242,29 +242,52 @@ subtree(c1) :- node(X1,4),child(X1,1,X2),node(X2,D2),allowed(c1x2,D2),child(X1,2
     end
 
     @testset "ASPSolver" begin
-        @testset "asp_solver" begin
+        @testset "asp_solver_uniform_holes" begin
+            g = @csgrammar begin
+                S = 1 | x
+                S = S + S
+                S = S * S
+            end
+            addconstraint!(g, Unique(1))
+            addconstraint!(g, Unique(2))
+
+            tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                UniformHole(BitVector((1, 1, 0, 0)), []),
+                UniformHole(BitVector((1, 1, 0, 0)), [])
+            ])
+
+            solver = ASPSolver(g, tree)
+            @test length(solver.solutions) == 4
+
+            @test Dict{Int64,Int64}(1 => 3, 2 => 1, 3 => 2) in solver.solutions
+            @test Dict{Int64,Int64}(1 => 3, 2 => 2, 3 => 1) in solver.solutions
+            @test Dict{Int64,Int64}(1 => 4, 2 => 1, 3 => 2) in solver.solutions
+            @test Dict{Int64,Int64}(1 => 4, 2 => 2, 3 => 1) in solver.solutions
+        end
+
+        @testset "asp_solver_filled_tree" begin
             g = @csgrammar begin
                 S = 1 | x
                 S = S + S
                 S = S * S
             end
 
             tree = RuleNode(3, [
-                RuleNode(1),
                 RuleNode(4, [
                     RuleNode(1),
                     RuleNode(2)
-                ])
+                ]),
+                RuleNode(3, [
+                    RuleNode(1),
+                    RuleNode(2)
+                ]),            
             ])
 
             solver = ASPSolver(g, tree)
-            solve(solver)
             @test length(solver.solutions) == 1
-            expected_solution = Dict{Int64,Int64}(1 => 3, 2 => 1, 3 => 4, 4 => 1, 5 => 2)
-            @test solver.solutions[1] == expected_solution
         end
-
-        @testset "asp_solver_write_file" begin
+        
+        @testset "asp_solver_filled_tree_constraints" begin
             g = @csgrammar begin
                 S = 1 | x
                 S = S + S
@@ -273,22 +296,55 @@ subtree(c1) :- node(X1,4),child(X1,1,X2),node(X2,D2),allowed(c1x2,D2),child(X1,2
             addconstraint!(g, Unique(1))
             addconstraint!(g, Unique(2))
 
-            tree = RuleNode(4, [
-                UniformHole(BitVector((1, 1, 0, 0)), []),
-                UniformHole(BitVector((1, 1, 0, 0)), [])
+            tree = RuleNode(3, [
+                RuleNode(4, [
+                    RuleNode(1),
+                    RuleNode(2)
+                ]),
+                RuleNode(3, [
+                    RuleNode(1),
+                    RuleNode(2)
+                ]),            
             ])
 
             solver = ASPSolver(g, tree)
-            solve(solver, true)
+            @test length(solver.solutions) == 0
+            @test isfeasible(solver) == false
+        end
+        
+        @testset "asp_solver_non_uniform" begin
+            g = @csgrammar begin
+                S = 1 | x
+                S = S + S
+                S = S * S
+            end
+
+            tree = Hole(BitVector([1, 1, 1, 1]))
+
+            try
+                solver = ASPSolver(g, tree)
+            catch AssertionError
+                @test true
+            end
+        end
+        
+        @testset "asp_solver_properties" begin
+            g = @csgrammar begin
+                S = 1 | x
+                S = S + S
+                S = S * S
+            end
 
-            extract_solutions_from_file(solver)
-            @test length(solver.solutions) == 2
-            
-            expected_solution_1 = Dict{Int64,Int64}(1 => 4, 2 => 1, 3 => 2)
-            expected_solution_2 = Dict{Int64,Int64}(1 => 4, 2 => 2, 3 => 1)
+            tree = UniformHole(BitVector((0, 0, 1, 1)), [
+                UniformHole(BitVector((1, 1, 0, 0)), []),
+                UniformHole(BitVector((1, 1, 0, 0)), [])
+            ])
 
-            @test solver.solutions[1] == expected_solution_1 || solver.solutions[1] == expected_solution_2
-            @test solver.solutions[2] == expected_solution_1 || solver.solutions[2] == expected_solution_2
+            solver = ASPSolver(g, tree)
+            @test get_grammar(solver) === g
+            @test get_tree(solver) === tree
+            @test isfeasible(solver) === true
+            @test get_name(solver) == "ASPSolver"
         end
     end
 end