From 21fccd728fe3d0fd9066646c4a7bde8713b3de2f Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 2 Aug 2019 22:27:25 +0200 Subject: [PATCH] refactor: internal engine now handles multiple copies of objects The parser still doesn't, but it's comparatively easy. After that we are done with #10. This implied a large amount of refactoring. The code is all the better. --- src/formula.ml | 4 +- src/main.ml | 666 +++++++++++++++++++++++++++--------------------- src/provable.ml | 53 +++- src/sat.ml | 4 + src/types.ml | 152 ++++++++--- 5 files changed, 549 insertions(+), 330 deletions(-) diff --git a/src/formula.ml b/src/formula.ml index 6214be5..0653fdb 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -35,7 +35,7 @@ let rec vars = function | Impl (x,y) -> Seq.flat_map vars (List.to_seq [x;y]) | Not x -> vars x -let pp pp_var f fmt = +let pp pp_var fmt f = let and_prec = 2 and or_prec = 3 and impl_prec = 1 @@ -45,7 +45,7 @@ let pp pp_var f fmt = match f with | One -> Format.fprintf fmt "1" | Zero -> Format.fprintf fmt "0" - | Var x -> pp_var x fmt + | Var x -> pp_var fmt x | And (x,y) when prec <= and_prec -> Format.fprintf fmt "%t && %t" (pp and_prec x) (pp and_prec y) | Or (x,y) when prec <= or_prec -> Format.fprintf fmt "%t || %t" (pp or_prec x) (pp or_prec y) | Impl (x,y) when prec <= impl_prec -> Format.fprintf fmt "%t --> %t" (pp (impl_prec+1)x) (pp impl_prec y) diff --git a/src/main.ml b/src/main.ml index fd333f1..c60c95a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -22,322 +22,405 @@ let (|||) = MLBDD.dor let anot = MLBDD.dnot let (-->) = MLBDD.imply -type formula = Item.t Atom.t Provable.timed Formula.t +module MultipliedOrIndexed = Either(MultipliedItem)(IndexedItem) +type formula = (MultipliedOrIndexed.t, IndexedItem.t) Atom.t Provable.timed Formula.t -module TimedLiteral = Sat.Literal(struct type t = Item.t Atom.t Provable.timed let equal = (=) let hash = Provable.hash (Atom.hash Item.hash) let pp = pp_timed_atom Item.pp end) -module TimedIndexedLiteral = Sat.Literal(struct type t = IndexedItem.t Atom.t Provable.timed let equal = (=) let hash = Provable.hash (Atom.hash IndexedItem.hash) let pp = pp_timed_atom IndexedItem.pp end) -(* XXX: Literal, should provide its comparison function *) -module TimedLiteralMap = Map.Make(struct type t = TimedLiteral.t let compare = compare end) -module LiteralsWithMults = struct - include TimedIndexedLiteral - type u = TimedLiteral.t +module IndexedAssignmentAtom = Atom.Make(MultipliedOrIndexed)(IndexedItem) +module TimedAtom = Provable.MakeTimed(IndexedAssignmentAtom) +module TimedLiteral = Sat.Literal(TimedAtom) - let compare = compare - let norm_u = TimedLiteral.norm +module TimedIndexedAtom = Provable.MakeTimed(Atom.Make(IndexedItem)(IndexedItem)) +module TimedIndexedLiteral = Sat.Literal(TimedIndexedAtom) +module TimedLiteralMap = Map.Make(TimedLiteral) + +module type CompileArg = sig + + val the_program : program - let decomp (n,l) = - ([n,Provable.map_timed (Atom.map (fun i -> (i,0))) l], 1) end -module Mult = Multiplicity.Make(LiteralsWithMults) -let invert_array (arr : Mult.L.t array) : int Mult.L.Map.t = - Array.to_seqi arr |> - Seq.fold_left (fun acc (i,a) -> Mult.L.Map.add a i acc) Mult.L.Map.empty +module Compile (P : CompileArg) = struct -let compile_formula man var_index (f : Mult.L.t Formula.t) : MLBDD.t = - let mk_var (l : Mult.L.t) : MLBDD.t = - match Mult.L.norm l with - | (a, Msat.Negated) -> MLBDD.dnot @@ MLBDD.ithvar man (Mult.L.Map.find a var_index) - | (a, Msat.Same_sign) -> MLBDD.ithvar man (Mult.L.Map.find a var_index) - in - let rec compile = let open Formula in function - | Zero -> MLBDD.dfalse man - | One -> MLBDD.dtrue man - | Var l -> mk_var l - | And (x,y) -> compile x &&& compile y - | Or (x,y) -> compile x ||| compile y - | Impl (x,y) -> MLBDD.imply (compile x) (compile y) - | Not x -> anot (compile x) - in - (* let _ = Logs.debug (fun m -> m "%t@." (Formula.pp (fun a fmt -> Format.fprintf fmt "%s" (print_timed_atom a)) f)) in *) - (* assert false *) - compile f - -let collect_program_atoms (p : program) : AtomSet.t = - let atoms : Item.t Atom.t Seq.t = - List.to_seq p.pool |> - Seq.flat_map (fun i -> - List.to_seq p.locations |> - Seq.flat_map (fun l -> List.to_seq [Atom.Assign(l,i)])) - in - AtomSet.of_seq atoms + let indexed (i:Item.t) : IndexedItem.t Seq.t = + let open OSeq in + let n = List.assoc i P.the_program.pool in + (0 --^ n) >>= fun j -> + return @@ IndexedItem.make i j -let gen_rule_name : unit -> string = - let count = ref 0 in - fun () -> - let r = "Rule " ^ string_of_int (!count) in - incr count; - r + module LiteralsWithMults = struct + include TimedIndexedLiteral + type u = TimedLiteral.t + let norm_u = TimedLiteral.norm -module Solver = Sat.Solver(Mult.L)(Mult.L.Map) + let decomp ((neg,l) : u) : (t list * int)= + let decomp_atom = function + | Atom.Have (MultipliedOrIndexed.Left (i,k)) -> + let individualised = + List.of_seq begin + let open OSeq in + indexed i >>= fun ii -> + return @@ Atom.Have ii + end + in + (individualised, k) + | a -> ([Atom.map (function MultipliedOrIndexed.Left _ -> assert false | Right i -> i) (fun i -> i) a], 1) + in + let decomp_timed_atom = function + | Provable.Action (s, i) -> [Provable.Action (s,i)], 1 + | Provable.At (a, i) -> + let (individualised, k) = decomp_atom a in + List.map (fun b -> Provable.At(b,i)) individualised, k + | Provable.Selection a -> + let (individualised, k) = decomp_atom a in + List.map (fun b -> Provable.Selection b) individualised, k + in + let (invidualised, k) = decomp_timed_atom l in + List.map (fun a -> (neg,a)) invidualised, k + end + module Mult = Multiplicity.Make(LiteralsWithMults) -(* XXX: This uses Bdd.set_max_var which is not at all a safe thing to - do! If I use the function twice, it will destroy the previous - bdd. *) -let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = - let assign (i : Item.t) (l : Location.t) : formula = - Formula.var (Provable.Selection (Atom.Assign(l,i))) - in - let clause (c : Clause.t) : Item.t Atom.t Provable.clause = - let open Provable in - let open Clause in - { - hyps=c.requires; - concl=c.goal; - name=gen_rule_name () - } - in - let range (p : program) (r : RangeConstraint.t) : formula = - let at_least = Formula.disj_map (fun l -> assign r.scrutinee l) r.range in - (* XXX: consider generating at_most/only constraint independently - from the range, on _all_ locations. *) - let at_most = - let distinct_pairs = - List.to_seq r.range |> - Seq.flat_map (fun l -> Seq.map (fun l' -> (l,l')) (List.to_seq r.range)) |> - Seq.filter (fun (l,l') -> l <> l') + let invert_array (arr : Mult.L.t array) : int Mult.L.Map.t = + Array.to_seqi arr |> + Seq.fold_left (fun acc (i,a) -> Mult.L.Map.add a i acc) Mult.L.Map.empty + + let compile_formula man var_index (f : Mult.L.t Formula.t) : MLBDD.t = + let mk_var (l : Mult.L.t) : MLBDD.t = + match Mult.L.norm l with + | (a, Msat.Negated) -> MLBDD.dnot @@ MLBDD.ithvar man (Mult.L.Map.find a var_index) + | (a, Msat.Same_sign) -> MLBDD.ithvar man (Mult.L.Map.find a var_index) + in + let rec compile = let open Formula in function + | Zero -> MLBDD.dfalse man + | One -> MLBDD.dtrue man + | Var l -> mk_var l + | And (x,y) -> compile x &&& compile y + | Or (x,y) -> compile x ||| compile y + | Impl (x,y) -> MLBDD.imply (compile x) (compile y) + | Not x -> anot (compile x) + in + compile f + + let collect_program_atoms (p : program) : AtomSet.t = + let atoms : (Item.t, Item.t) Atom.t Seq.t = + List.to_seq p.pool |> + Seq.flat_map (fun (i,_) -> + List.to_seq p.locations |> + Seq.flat_map (fun l -> List.to_seq [Atom.Assign(l,i)])) + in + AtomSet.of_seq atoms + + let gen_rule_name : unit -> string = + let count = ref 0 in + fun () -> + let r = "Rule " ^ string_of_int (!count) in + incr count; + r + + module Solver = Sat.Solver(Mult.L)(Mult.L.Map) + + let to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = + let assign (i : IndexedItem.t) (l : Location.t) : formula = + Formula.var (Provable.Selection (Atom.Assign(l,i))) + in + let clause (c : Clause.t) : (MultipliedOrIndexed.t, IndexedItem.t) Atom.t Provable.clause = + let open Provable in + let open Clause in + let cast = Atom.map (fun i-> MultipliedOrIndexed.Left i) (Empty.absurd) in + { + hyps=List.map cast c.requires; + concl= cast c.goal; + name=gen_rule_name () + } + in + let range (p : program) (r : RangeConstraint.t) : formula = + let at_least = Formula.conj_map_seq begin fun i -> + Formula.disj_map (fun l -> assign i l) r.range + end (indexed r.scrutinee) in - let open Formula in - conj_map (fun (l,l') -> not (assign r.scrutinee l && assign r.scrutinee l')) (List.of_seq distinct_pairs) + (* XXX: consider generating at_most/only constraint independently + from the range, on _all_ locations. *) + let at_most = + let ordered_pairs_of_locations = + let open OSeq in + begin + List.to_seq r.range >>= fun l -> + List.to_seq r.range >>= fun l' -> + return (l,l') + end |> + Seq.filter (fun (l,l') -> Location.compare l l' < 0) + in + (* Careful: these are largely order while the above are strictly ordered. *) + let ordered_pairs_of_items = + let open OSeq in + begin + indexed r.scrutinee >>= fun i -> + indexed r.scrutinee >>= fun i' -> + return (i,i') + end |> + Seq.filter (fun (i,i') -> IndexedItem.compare i i' <= 0) + in + let open Formula in + conj_seq begin + let open OSeq in + ordered_pairs_of_items >>= fun (i,i') -> + ordered_pairs_of_locations >>= fun (l,l') -> + return @@ not (assign i l' && assign i' l) + end + in + let only = + let other_locations = + List.to_seq p.locations |> + OSeq.filter (fun l -> not (List.mem l r.range)) + in + let open Formula in + let open OSeq in + conj_seq begin + indexed r.scrutinee >>= fun i -> + other_locations >>= fun l -> + return @@ not (assign i l) + end + in + Formula.(at_least && at_most && only) in - let only = - let other_locations = - p.locations |> - List.filter (fun l -> not (List.mem l r.range)) + let ranges_formula = Seq.map (range p) (List.to_seq p.range_constraints) in + let capacity (p : program) (l : Location.t) : formula = + let distinct_pairs = + let all_items = + List.to_seq p.pool + |> Seq.flat_map (fun (i,_) -> indexed i) + in + begin + let open OSeq in + all_items >>= fun i -> + all_items >>= fun i' -> + return (i, i') + end |> + Seq.filter (fun (i,i') -> not (IndexedItem.equal i i')) in let open Formula in - conj_map (fun l -> not (assign r.scrutinee l)) other_locations + conj_map (fun (i,i') -> not (assign i l && assign i' l)) (List.of_seq distinct_pairs) + (* XXX: There is probably a bug here: these are defined in terms + of items, I'm pretty sure they should be defined in terms of + indexed_items. *) in - Formula.(at_least && at_most && only) - in - let ranges_formula = Seq.map (range p) (List.to_seq p.range_constraints) in - let capacity (p : program) (l : Location.t) : formula = - let distinct_pairs = - List.to_seq p.pool |> - Seq.flat_map (fun i -> Seq.map (fun i' -> (i, i')) (List.to_seq p.pool)) |> - Seq.filter (fun (i,i') -> i <> i') + let capacities_formula = Seq.map (capacity p) (List.to_seq p.locations) in - let open Formula in - conj_map (fun (i,i') -> not (assign i l && assign i' l)) (List.of_seq distinct_pairs) - in - let capacities_formula = Seq.map (capacity p) (List.to_seq p.locations) - in - let logic_clauses = List.map clause p.logic in - let assign_clauses = - List.of_seq begin - List.to_seq p.pool |> - Seq.flat_map begin fun i -> - List.to_seq p.locations |> - Seq.map begin fun l -> + let logic_clauses = List.map clause p.logic in + let assign_clauses = + List.of_seq begin + let open OSeq in + List.to_seq p.pool >>= fun (i,_) -> + indexed i >>= fun ii -> + List.to_seq p.locations >>= fun l -> + return begin let open Provable in { - hyps = [ Atom.Reach l; Atom.Assign(l,i) ]; - concl = Atom.Have (i, 1); - name = gen_rule_name () + hyps = [ Atom.Reach l; Atom.Assign(l,ii) ]; + concl = Atom.Have (MultipliedOrIndexed.Right ii); + name = gen_rule_name () } end end - end - in - let module Prove = Provable.Make(AtomMap) in - let proof_system = Prove.convert { - clauses = logic_clauses @ assign_clauses; - goal = p.goal - } - in - let formulas = OSeq.flatten @@ OSeq.of_list - [ ranges_formula; - capacities_formula; - proof_system - ] - in - let clauses = formulas |> OSeq.flat_map TimedLiteral.cnf_seq in - let clauses = Mult.compile (List.of_seq clauses) in - let atoms = - OSeq.(formulas >>= Formula.vars) - |> TimedAtomSet.of_seq - |> TimedAtomSet.to_seq - |> Array.of_seq - in - let observable = - CCArray.filter (fun a -> match a with Provable.Selection _ -> true | _ -> false) atoms - |> Array.map (Provable.map_timed (Atom.map (fun i -> (i, 0)))) - |> Array.map TimedLiteral.of_atom - |> Array.map (fun a -> Mult.Individual a) - in - let var_index = invert_array observable in - let man = MLBDD.init () in - let solver = Solver.create () in - let _ = Solver.assume_clauses solver (List.to_seq clauses) in - (* NEXT: change observable to have elements of type Mult.atom. It's really the only way *) - Solver.successive_formulas solver observable + in + let module Prove = Provable.Make(IndexedAssignmentAtom.Map) in + let proof_system = Prove.convert { + clauses = logic_clauses @ assign_clauses; + goal = + let convert_multiple = function + | (i,1) -> MultipliedOrIndexed.Right (IndexedItem.make i 0) + (* XXX: it's actually incorrect if there are several copies of i. *) + | _ -> failwith "TODO: goals with multiplicities" + in + Atom.map convert_multiple Empty.absurd p.goal + } (function Atom.Assign _ -> true | _ -> false) + in + let _ = OSeq.iter (fun f -> Logs.debug (fun m -> m "Converted: %a@." (Formula.pp TimedAtom.pp) f)) proof_system in + let formulas = OSeq.flatten @@ OSeq.of_list + [ ranges_formula; + capacities_formula; + proof_system + ] + in + let clauses = formulas |> OSeq.flat_map TimedLiteral.cnf_seq in + let clauses = Mult.compile (List.of_seq clauses) in + (* XXX: the range and capacity formulas should directly be crafted in terms of the multiplicity transformation output. *) + let atoms = + OSeq.(formulas >>= Formula.vars) + |> TimedAtom.Set.of_seq + |> TimedAtom.Set.to_seq + |> Array.of_seq + in + let observable = + CCArray.filter (fun a -> match a with Provable.Selection (Atom.Assign _) -> true | _ -> false) atoms + |> Array.map (Provable.map_timed (Atom.map (fun _ -> assert false) (fun i -> i))) + |> Array.map TimedIndexedLiteral.of_atom + |> Array.map (fun a -> Mult.Individual a) + in + let var_index = invert_array observable in + let man = MLBDD.init () in + let solver = Solver.create () in + let _ = Solver.assume_clauses solver (List.to_seq clauses) in + (* NEXT: change observable to have elements of type Mult.atom. It's really the only way *) + Solver.successive_formulas solver observable |> Seq.map (compile_formula man var_index) |> OSeq.fold (|||) (MLBDD.dfalse man) , observable -let femto_example = - let open Clause in - (* A bit of early Alltp logic *) - (* items *) - let sword = "Sword" - (* locations *) - and well = "Karakiko Well" - and eastern_boss = "Eastern Boss" - in - let pool = [sword] in - let locations = [well; eastern_boss; ] in - let goal = Atom.Reach eastern_boss in - let range_constraints = [ - {RangeConstraint.scrutinee=sword; range=locations}; - ] in - let logic = [ - {goal=Reach eastern_boss; requires=[Have (sword, 1)]}; - {goal=Reach well; requires=[]}; - ] in - { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } - -let micro_example = - let open Clause in - (* A bit of early Alltp logic *) - (* items *) - let sword = "Sword" - and bow = "Bow" - (* locations *) - and well = "Karakiko Well" - and hideout = "Blind's Hideout" - and eastern_chest = "Eastern Small Chest" - and eastern_boss = "Eastern Boss" - in - let pool = [sword; bow] in - let locations = [well; hideout; eastern_chest; eastern_boss; ] in - let goal = Atom.Reach eastern_boss in - let range_constraints = [ - {RangeConstraint.scrutinee=sword; range=locations}; - {RangeConstraint.scrutinee=bow; range=locations}; - ] in - let logic = [ - {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1)]}; - {goal=Reach well; requires=[]}; - {goal=Reach hideout; requires=[]}; - {goal=Reach eastern_chest; requires=[]}; - ] in - { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } - -let mini_example = - let open Clause in - (* A bit of early Alltp logic *) - (* items *) - let sword = "Sword" - and bow = "Bow" - and eastern_big = "Eastern Big Key" - (* locations *) - and well = "Karakiko Well" - and hideout = "Blind's Hideout" - and eastern_chest = "Eastern Small Chest" - and eastern_big_chest = "Easter Big Chest" - and eastern_boss = "Eastern Boss" - in - let pool = [sword; bow; eastern_big] in - let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; ] in - let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in - let goal = Atom.Reach eastern_boss in - let range_constraints = [ - {RangeConstraint.scrutinee=sword; range=locations}; - {RangeConstraint.scrutinee=bow; range=locations}; - {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; - ] in - let logic = [ - {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; - {goal=Reach well; requires=[]}; - {goal=Reach hideout; requires=[]}; - {goal=Reach eastern_chest; requires=[Have (eastern_big, 1)]}; - {goal=Reach eastern_big_chest; requires=[]}; - ] in - { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } - -let example = - let open Clause in - (* A bit of early Alltp logic *) - (* items *) - let sword = "Sword" - and bow = "Bow" - and boots = "Boots" - and glove = "Power Glove" - and eastern_big = "Eastern Big Key" - and desert_big = "Desert Big Key" - (* locations *) - and well = "Karakiko Well" - and hideout = "Blind's Hideout" - and eastern_chest = "Eastern Small Chest" - and eastern_big_chest = "Easter Big Chest" - and eastern_boss = "Eastern Boss" - and desert_torch = "Desert Torch" - and desert_big_chest = "Desert Big Chest" - and desert_boss = "Desert Boss" - in - let pool = [sword; bow; boots; glove; eastern_big; desert_big] in - let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; desert_torch; desert_big_chest; desert_boss] in - let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in - let desert_palace = [desert_torch; desert_big_chest; desert_boss] in - let goal = Atom.Reach desert_boss in - let range_constraints = [ - {RangeConstraint.scrutinee=sword; range=locations}; - {RangeConstraint.scrutinee=bow; range=locations}; - {RangeConstraint.scrutinee=boots; range=locations}; - {RangeConstraint.scrutinee=glove; range=locations}; - {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; - {RangeConstraint.scrutinee=desert_big; range=desert_palace}; - ] in - let logic = [ - {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; - {goal=Reach desert_boss; requires=[Have (glove, 1); Have (sword, 1); Have (eastern_big, 1)]}; - {goal=Reach desert_torch; requires=[Have (boots, 1)]}; - {goal=Reach well; requires=[]}; - {goal=Reach hideout; requires=[]}; - {goal=Reach eastern_chest; requires=[]}; - {goal=Reach eastern_big_chest; requires=[Have (eastern_big, 1)]}; - {goal=Reach desert_big_chest; requires=[Have (desert_big, 1)]}; - ] in - { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } - -let print_to_dot legend b ~file = - (* Adapted from Jean-Christophe Filliâtre's bdd library*) - let open Format in - let module H1 = Hashtbl.Make(struct type t = MLBDD.t let equal = MLBDD.equal let hash = MLBDD.hash end) in - let c = open_out file in - let fmt = formatter_of_out_channel c in - fprintf fmt "digraph bdd {@\n"; - let visited = H1.create 1024 in - let rec visit b = - if not (H1.mem visited b) then begin - H1.add visited b (); - match MLBDD.inspectb b with + let femto_example = + let open Clause in + (* A bit of early Alltp logic *) + (* items *) + let sword = "Sword" + (* locations *) + and well = "Karakiko Well" + and eastern_boss = "Eastern Boss" + in + let pool = List.map (fun i -> (i,1)) [sword] in + let locations = [well; eastern_boss; ] in + let goal = Atom.Reach eastern_boss in + let range_constraints = [ + {RangeConstraint.scrutinee=sword; range=locations}; + ] in + let logic = [ + {goal=Reach eastern_boss; requires=[Have (sword, 1)]}; + {goal=Reach well; requires=[]}; + ] in + { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } + + let micro_example = + let open Clause in + (* A bit of early Alltp logic *) + (* items *) + let sword = "Sword" + and bow = "Bow" + (* locations *) + and well = "Karakiko Well" + and hideout = "Blind's Hideout" + and eastern_chest = "Eastern Small Chest" + and eastern_boss = "Eastern Boss" + in + let pool = List.map (fun i -> (i,1)) [sword; bow] in + let locations = [well; hideout; eastern_chest; eastern_boss; ] in + let goal = Atom.Reach eastern_boss in + let range_constraints = [ + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; + ] in + let logic = [ + {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1)]}; + {goal=Reach well; requires=[]}; + {goal=Reach hideout; requires=[]}; + {goal=Reach eastern_chest; requires=[]}; + ] in + { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } + + let mini_example = + let open Clause in + (* A bit of early Alltp logic *) + (* items *) + let sword = "Sword" + and bow = "Bow" + and eastern_big = "Eastern Big Key" + (* locations *) + and well = "Karakiko Well" + and hideout = "Blind's Hideout" + and eastern_chest = "Eastern Small Chest" + and eastern_big_chest = "Easter Big Chest" + and eastern_boss = "Eastern Boss" + in + let pool = List.map (fun i -> (i,1)) [sword; bow; eastern_big] in + let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; ] in + let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in + let goal = Atom.Reach eastern_boss in + let range_constraints = [ + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; + {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; + ] in + let logic = [ + {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; + {goal=Reach well; requires=[]}; + {goal=Reach hideout; requires=[]}; + {goal=Reach eastern_chest; requires=[Have (eastern_big, 1)]}; + {goal=Reach eastern_big_chest; requires=[]}; + ] in + { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } + + let example = + let open Clause in + (* A bit of early Alltp logic *) + (* items *) + let sword = "Sword" + and bow = "Bow" + and boots = "Boots" + and glove = "Power Glove" + and eastern_big = "Eastern Big Key" + and desert_big = "Desert Big Key" + (* locations *) + and well = "Karakiko Well" + and hideout = "Blind's Hideout" + and eastern_chest = "Eastern Small Chest" + and eastern_big_chest = "Easter Big Chest" + and eastern_boss = "Eastern Boss" + and desert_torch = "Desert Torch" + and desert_big_chest = "Desert Big Chest" + and desert_boss = "Desert Boss" + in + let pool = List.map (fun i -> (i,1)) [sword; bow; boots; glove; eastern_big; desert_big] in + let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; desert_torch; desert_big_chest; desert_boss] in + let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in + let desert_palace = [desert_torch; desert_big_chest; desert_boss] in + let goal = Atom.Reach desert_boss in + let range_constraints = [ + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; + {RangeConstraint.scrutinee=boots; range=locations}; + {RangeConstraint.scrutinee=glove; range=locations}; + {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; + {RangeConstraint.scrutinee=desert_big; range=desert_palace}; + ] in + let logic = [ + {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; + {goal=Reach desert_boss; requires=[Have (glove, 1); Have (sword, 1); Have (eastern_big, 1)]}; + {goal=Reach desert_torch; requires=[Have (boots, 1)]}; + {goal=Reach well; requires=[]}; + {goal=Reach hideout; requires=[]}; + {goal=Reach eastern_chest; requires=[]}; + {goal=Reach eastern_big_chest; requires=[Have (eastern_big, 1)]}; + {goal=Reach desert_big_chest; requires=[Have (desert_big, 1)]}; + ] in + { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } + + let print_to_dot legend b ~file = + (* Adapted from Jean-Christophe Filliâtre's bdd library*) + let open Format in + let module H1 = Hashtbl.Make(struct type t = MLBDD.t let equal = MLBDD.equal let hash = MLBDD.hash end) in + let c = open_out file in + let fmt = formatter_of_out_channel c in + fprintf fmt "digraph bdd {@\n"; + let visited = H1.create 1024 in + let rec visit b = + if not (H1.mem visited b) then begin + H1.add visited b (); + match MLBDD.inspectb b with | BFalse -> - fprintf fmt "%d [shape=box label=\"0\"];" (MLBDD.id b) + fprintf fmt "%d [shape=box label=\"0\"];" (MLBDD.id b) | BTrue -> - fprintf fmt "%d [shape=box label=\"1\"];" (MLBDD.id b) + fprintf fmt "%d [shape=box label=\"1\"];" (MLBDD.id b) | BIf (l, v, h) -> - (* add_rank v b; *) - fprintf fmt "%d [label=\"x%a\"];" (MLBDD.id b) (pp_timed_atom Item.pp) (legend.(v-1)); - fprintf fmt "%d -> %d;@\n" (MLBDD.id b) (MLBDD.id h); - fprintf fmt "%d -> %d [style=\"dashed\"];@\n" (MLBDD.id b) (MLBDD.id l); - visit h; visit l - end - in - visit b; - fprintf fmt "}@."; - close_out c + (* add_rank v b; *) + fprintf fmt "%d [label=\"x%a\"];" (MLBDD.id b) (Provable.pp_timed_atom Item.pp) (legend.(v-1)); + fprintf fmt "%d -> %d;@\n" (MLBDD.id b) (MLBDD.id h); + fprintf fmt "%d -> %d [style=\"dashed\"];@\n" (MLBDD.id b) (MLBDD.id l); + visit h; visit l + end + in + visit b; + fprintf fmt "}@."; + close_out c + +end let parse_file (filename : String.t) = let chan = open_in filename in @@ -357,7 +440,7 @@ let parse_file (filename : String.t) = let locs = interp_range_expression prog range_expr in let range = {RangeConstraint.scrutinee=item; range=locs} in { prog with - pool = item :: prog.pool; + pool = (item, 1) :: prog.pool; locations = locs @ prog.locations; range_constraints = range :: prog.range_constraints; } @@ -417,7 +500,8 @@ let _ = let _ = Logs.set_reporter (Logs_fmt.reporter ()) in let _ = Logs.set_level (Some Logs.Debug) in let example = parse_file "example.logic" in - let (bdd, legend) = compile_to_bdd example in + let module Comp = Compile(struct let the_program = example end) in + let (bdd, legend) = Comp.to_bdd example in let module Params = struct type t = int (* XXX: ints might not be enough *) @@ -434,7 +518,7 @@ let _ = let the_vars = Array.mapi (fun i _ -> i+1) legend let pp fmt i = - Format.fprintf fmt "%a" Mult.L.pp legend.(i) + Format.fprintf fmt "%a" Comp.Mult.L.pp legend.(i) end in let module Z = Zdd.Make(Params)(Vars) in diff --git a/src/provable.ml b/src/provable.ml index 7ada706..bfbd20a 100644 --- a/src/provable.ml +++ b/src/provable.ml @@ -65,7 +65,49 @@ let hash h = function | At (a,t) -> CCHash.(combine3 (int 1) (h a) (int t)) | Selection a -> CCHash.(combine2 (int 2) (h a)) -module StringSet = Set.Make(struct type t=string let compare=compare end) +let equal equal_atom t u = match t, u with + | Action (namet,tt), Action(nameu,tu) -> CCString.equal namet nameu && CCInt.equal tt tu + | At(at,tt), At(au,tu) -> equal_atom at au && CCInt.equal tt tu + | Selection at, Selection au -> equal_atom at au + | _ -> false + +let compare compare_atom t u = match t, u with + | Action (namet,tt), Action(nameu,tu) -> CCOrd.(string namet nameu (int, tt, tu)) + | Action _, _ -> -1 + | _, Action _ -> 1 + | At(at,tt), At(au,tu) -> CCOrd.(compare_atom at au (int, tt, tu)) + | At _, _ -> -1 + | _, At _ -> 1 + | Selection at, Selection au -> compare_atom at au + (* | Selection _, _ -> -1 + * | _, Selection _ -> 1 *) + +let pp_timed_atom pp_atom fmt = function + | Selection a -> pp_atom fmt a + | At(a,i) -> Format.fprintf fmt "%a @@%i" pp_atom a i + | Action (n, i) -> Format.fprintf fmt "%s @@%i" n i + +module MakeTimed(A:Types.Type) = struct + + module Core = struct + type t = A.t timed + + let equal = equal A.equal + let compare = compare A.compare + let hash = hash A.hash + + let pp = pp_timed_atom A.pp + end + + include Core + + module Set = Set.Make(Core) + module Map = Map.Make(Core) + +end + +(* XXX: how many copies of StringSet is there? *) +module StringSet = Set.Make(struct type t=string let compare=String.compare end) module Make (M : Map.S) = struct @@ -79,14 +121,15 @@ module Make (M : Map.S) = struct *) module type Params = sig - val timed : StringSet.t M.t + val selection : atom -> bool + val timed : StringSet.t M.t (* XXX: timed in an obsolete names, it is really the collection of conclusion of rules. *) val max_steps : int end module MainLoop (P : Params) = struct let at (i:int) (a : atom) : formula = - if M.mem a P.timed then Formula.var @@ At(a,i) + if not (P.selection a) then Formula.var @@ At(a,i) else Formula.var @@ Selection a let action_var (i:int) (name : string) : formula = @@ -123,7 +166,7 @@ module Make (M : Map.S) = struct Formula.((conj_map (at i) c.hyps && not (at i c.concl))--> name i c) end - let convert (prog : atom program) : formula Seq.t = + let convert (prog : atom program) (selection : atom -> bool) : formula Seq.t = let _ = Logs.debug (fun m -> m "%i@." (List.length prog.clauses)) in let add_add a n m = let upd = function @@ -137,7 +180,7 @@ module Make (M : Map.S) = struct List.fold_left (fun acc c -> add_add c.concl c.name acc) M.empty (prog.clauses) in let max_steps = List.length (prog.clauses) in - let module L = MainLoop (struct let timed=timed let max_steps=max_steps end) in + let module L = MainLoop (struct let timed=timed let max_steps=max_steps let selection=selection end) in let initial_state = Formula.conj_seq begin M.to_seq timed diff --git a/src/sat.ml b/src/sat.ml index 5a2a236..6b728a8 100644 --- a/src/sat.ml +++ b/src/sat.ml @@ -6,6 +6,7 @@ module type Atom = sig val equal : t -> t -> bool val hash : t -> int val pp : Format.formatter -> t -> unit + val compare : t -> t -> int end module Literal (A:Atom) = struct @@ -24,6 +25,9 @@ module Literal (A:Atom) = struct if n then A.pp fmt a else Format.fprintf fmt "~%a" A.pp a + let compare = + CCOrd.pair CCBool.compare A.compare + let neg (n,a) = (not n, a) let norm ((n,_) as l) = diff --git a/src/types.ml b/src/types.ml index bca861e..53e3eb4 100644 --- a/src/types.ml +++ b/src/types.ml @@ -1,3 +1,57 @@ +module type Type = sig + + (* Type with the basic functions used pervasively throughout the randomizer engine.*) + + type t + + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + + val pp : Format.formatter -> t -> unit +end + +module Empty = struct + + type t = { ef : 'a. 'a} + + let absurd v = v.ef + + let empty v _w = v.ef + let compare v _w = v.ef + let hash v = v.ef + + let pp _fmt v = v.ef + +end + +module Either (L:Type) (R:Type) = struct + + type t = + | Left of L.t + | Right of R.t + + let equal x y = match x,y with + | Left x, Left y -> L.equal x y + | Right x, Right y -> R.equal x y + | _ -> false + + let compare x y = match x,y with + | Left x, Left y -> L.compare x y + | Left _, _ -> -1 + | _, Left _ -> 1 + | Right x, Right y -> R.compare x y + + let hash = function + | Left x -> CCHash.(combine2 (int 0) (L.hash x)) + | Right x -> CCHash.(combine2 (int 1) (R.hash x)) + + let pp fmt = function + | Left x -> L.pp fmt x + | Right x -> R.pp fmt x + +end + module Variable = struct include CCString @@ -14,6 +68,24 @@ module Item = Variable module IndexedItem = struct + (* Stands for a number of copies of an item which may have several copies. *) + + type t = { item: Item.t; index: int } + + let make item index = { item; index } + + let compare {item=iteml; index=indexl} {item=itemr; index=indexr} = + CCOrd.(Item.compare iteml itemr (CCInt.compare, indexl, indexr)) + let equal {item=iteml; index=indexl} {item=itemr; index=indexr} = + Item.equal iteml itemr && CCInt.equal indexl indexr + + let hash {item; index} = CCHash.(combine2 (Item.hash item) (int index)) + + let pp fmt {item; index} = Format.fprintf fmt "%a_%i" Item.pp item index +end + +module MultipliedItem = struct + (* Stands for a specific copy of an item which may have several copies. *) type t = Item.t * int @@ -23,7 +95,9 @@ module IndexedItem = struct let hash (item,k) = CCHash.(combine2 (Item.hash item) (int k)) - let pp fmt (item,k) = Format.fprintf fmt "%a_%i" Item.pp item k + let pp fmt = function + | (item,1) -> Format.fprintf fmt "%a" Item.pp item + | (item,k) -> Format.fprintf fmt "%a * %i" Item.pp item k end module RangeConstraint = struct @@ -39,13 +113,13 @@ end module Atom = struct - type 'i t = + type ('p,'i) t = | Reach of Location.t - | Have of 'i * int + | Have of 'p (* XXX: The goal is to separate the `'i` in Have and the `'i` in Assign so that `Have` can be an item w/ multiplicity (we can drop the `int` from the constructor that way, and it will be better when we decompose in the multiplicity transformation, it will make more sense) and `Assign` can mention individualised items, because it's the only thing that would make sense. All that going into the provable transformation, which needs to be performed before the multiplicity transformation as it requires implicational clauses (including clauses involving assignment!).*) | Assign of Location.t * 'i (* Assign doesn't come from parsing: it appears in translations.*) - let compare item_compare al ar = match al, ar with + let compare possession_compare item_compare al ar = match al, ar with | Assign(locl,iteml), Assign(locr, itemr) -> CCPair.compare Location.compare item_compare (locl,iteml) (locr,itemr) | Assign _, _ -> -1 @@ -54,46 +128,65 @@ module Atom = struct Location.compare locl locr | Reach _, _ -> -1 | _, Reach _ -> 1 - | Have(iteml, kl), Have(itemr, kr) -> - CCPair.compare item_compare CCInt.compare (iteml, kl) (itemr, kr) - let equal item_equal al ar = match al, ar with + | Have iteml, Have itemr -> + possession_compare iteml itemr + let equal possession_equal item_equal al ar = match al, ar with | Assign(locl,iteml), Assign(locr, itemr) -> Location.equal locl locr && item_equal iteml itemr | Reach locl, Reach locr -> Location.equal locl locr - | Have(iteml,kl), Have(itemr,kr) -> - item_equal iteml itemr && CCInt.equal kl kr + | Have iteml, Have itemr -> + possession_equal iteml itemr | _ -> false - let hash hash_item = function + let hash hash_possession hash_item = function | Reach l -> CCHash.(combine2 (int 0) (Location.hash l)) - | Have (i, n) -> CCHash.(combine3 (int 1) (hash_item i) (int n)) + | Have i -> CCHash.(combine2 (int 1) (hash_possession i)) | Assign (l,i) -> CCHash.(combine3 (int 2) (Location.hash l) (hash_item i)) - let map f = function + let map f_possession f_item = function | Reach l -> Reach l - | Have (i, n) -> Have (f i, n) - | Assign (l, i) -> Assign (l, f i) + | Have i -> Have (f_possession i) + | Assign (l, i) -> Assign (l, f_item i) - let pp pp_item fmt = function + let pp pp_possession pp_item fmt = function | Reach l -> Format.fprintf fmt "reach: %a" Location.pp l - | Have (i,1) -> Format.fprintf fmt "have: %a" pp_item i - | Have (i,n) -> Format.fprintf fmt "have: %a * %i" pp_item i n + | Have i -> Format.fprintf fmt "have: %a" pp_possession i | Assign(l,i) -> Format.fprintf fmt "%a ∈ %a" pp_item i Location.pp l + module Make(P:Type)(I:Type) = struct + + module Core = struct + type nonrec t = (P.t, I.t) t + + let equal = equal P.equal I.equal + let compare = compare P.compare I.compare + let hash = hash P.hash I.hash + + let pp = pp P.pp I.pp + end + + include Core + + module Set = Set.Make(Core) + module Map = Map.Make(Core) + end + end module Clause = struct type t = { - goal: Item.t Atom.t; - requires: Item.t Atom.t list + goal: (MultipliedItem.t, Empty.t) Atom.t; + requires: (MultipliedItem.t, Empty.t) Atom.t list } end module StringMap = Map.Make(CCString) +(* XXX: everything below this deserves to be reorganised. *) + type program = { locations: Location.t list; (* Future plan for item: there can be more than one of an item in @@ -102,29 +195,24 @@ type program = { the corresponding range_constraints will be translated to formulas which ensure that the n variables are ordered (to avoid generating many semantically equal shuffles) *) - pool: Item.t list; + pool: (Item.t * int) list; range_constraints: RangeConstraint.t list; range_definitions: Location.t list StringMap.t; logic: Clause.t list; - goal: Item.t Atom.t + goal: (MultipliedItem.t, Empty.t) Atom.t } -let pp_timed_atom pp_item fmt = let open Provable in function - | Selection a -> Atom.pp pp_item fmt a - | At(a,i) -> Format.fprintf fmt "%a @ %i" (Atom.pp pp_item) a i - | Action (n, i) -> Format.fprintf fmt "%s @ %i" n i let pp_clause fmt {Clause.goal;requires} = - Format.fprintf fmt "%a :- @[%a@]" (Atom.pp Item.pp) goal (CCList.pp ~sep:"," (Atom.pp Item.pp)) requires + Format.fprintf fmt "%a :- @[%a@]" (Atom.pp MultipliedItem.pp Empty.pp) goal (CCList.pp ~sep:"," (Atom.pp MultipliedItem.pp Empty.pp)) requires let pp_program fmt prog = (* XXX: I'm not printing range_definitions *) let pp_locations = CCList.pp (fun fmt l -> Format.fprintf fmt "@[%s@]" l) in - let pp_pool = CCList.pp (fun fmt i -> Format.fprintf fmt "@[%s@]" i) in + let pp_pool = CCList.pp (fun fmt (i,n) -> Format.fprintf fmt "@[%s*%i@]" i n) in let pp_ranges = CCList.pp RangeConstraint.pp in let pp_logic = CCList.pp pp_clause in - let pp_goal fmt g = Format.fprintf fmt "%a." (Atom.pp Item.pp) g in + let pp_goal fmt g = Format.fprintf fmt "%a." (Atom.pp MultipliedItem.pp Empty.pp) g in Format.fprintf fmt "@[@[[Locations]@,%a@]@,@[[Pool]@,%a@]@,@[[Ranges]@,%a@]@,@[[Logic]@,%a@]@,@[[Goal]@,%a@]@]@." pp_locations prog.locations pp_pool prog.pool pp_ranges prog.range_constraints pp_logic prog.logic pp_goal prog.goal -module AtomSet = Set.Make (struct type t = Item.t Atom.t let compare = Atom.compare Item.compare end) -module AtomMap = Map.Make (struct type t = Item.t Atom.t let compare = Atom.compare Item.compare end) -module TimedAtomSet = Set.Make (struct type t = Item.t Atom.t Provable.timed let compare = compare end) -module TimedAtomMap = Map.Make (struct type t = Item.t Atom.t Provable.timed let compare = compare end) +module ItemAtom = Atom.Make(Item)(Item) +module AtomSet = ItemAtom.Set +module AtomMap = ItemAtom.Map