Commit e1e3dd81 authored by Simon Prucker's avatar Simon Prucker
Browse files

Simplifiable tree structure for shrinking

parent 52797e16
Pipeline #14137 waiting for manual action with stages
module TArray = struct module TArray = struct
let any f arr = let any f arr =
let rec g idx = let rec g idx =
...@@ -168,4 +167,45 @@ module These = struct ...@@ -168,4 +167,45 @@ module These = struct
| These (_, b) -> Some b | These (_, b) -> Some b
end end
module Tree = struct
type 'a tree =
| Node of (('a tree) list) * (('a list) -> 'a) * int (*List of children * combinator function for already parsed children * height of subtree*)
| Leaf of 'a
let rec parse_back aTree = match aTree with
| Node (aTreeList, func, _) -> func (List.map parse_back aTreeList)
| Leaf a -> a
let checkIfGivenHeight expectedHeight aTree =
match aTree with
| Leaf _ -> (expectedHeight = 0)
| Node (_, _, height) -> (height = expectedHeight)
let rec simplify atree = match atree with
| Leaf _ -> None
| Node (aTreeList, func, height) ->
if (height = 1)
then Some (List.hd aTreeList)
else
let foundDeepest: bool ref = ref false in
let decrementHeight = (height - 1) in
let shrinkDeepest maxDepth aTree = if !foundDeepest then aTree else
match aTree with
| Leaf a -> Leaf a
| Node (_, _, depth) -> if (depth = maxDepth)
then
begin
foundDeepest := true;
Option.get (simplify aTree)
end
else aTree
in
let newChildren =
List.map (shrinkDeepest decrementHeight) aTreeList
in
let newDepth =
match (List.find_opt (checkIfGivenHeight decrementHeight) newChildren) with
| None -> decrementHeight
| Some _ -> height
in
Some (Node (newChildren, func, newDepth))
end
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -98,4 +98,14 @@ end ...@@ -98,4 +98,14 @@ end
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
module Tree :
sig
type 'a tree =
| Node of (('a tree) list) * (('a list) -> 'a) * int (*List of children * combinator function for already parsed children * height of subtree*)
| Leaf of 'a
val simplify : 'a tree -> 'a tree option
val parse_back : 'a tree -> 'a
end
(* vim: set et sw=2 sts=2 ts=8 : *) (* vim: set et sw=2 sts=2 ts=8 : *)
...@@ -88,8 +88,8 @@ let make_sorted (list:(F.formula list)) = ...@@ -88,8 +88,8 @@ let make_sorted (list:(F.formula list)) =
List.map (fun (f:F.formula) -> (0, f)) list List.map (fun (f:F.formula) -> (0, f)) list
(* Needs the formula as a sortedTable, sort set to 0 as by default. To be checked what's up with that. *) (* Needs the formula as a sortedTable, sort set to 0 as by default. To be checked what's up with that. *)
let onestepFunc_equals_tableau ?(num_runs = 18) name sized_formula_gen logic = let onestepFunc_equals_tableau ?(num_runs = 50) name sized_formula_gen logic =
"onestep func = tableau" >: to_ounit2_test (Test.make ~count:num_runs ~name:name "onestep func = tableau" >: to_ounit2_test ~rand: (Random.State.make_self_init ()) (Test.make ~count:num_runs ~name:name
( make ~print:F.string_of_formula (sized sized_formula_gen)) (fun (formula) -> ( make ~print:F.string_of_formula (sized sized_formula_gen)) (fun (formula) ->
(onestepFunc_equals_tableau_predicate logic (0, formula)) )) (onestepFunc_equals_tableau_predicate logic (0, formula)) ))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment