interval propagation: contradictions fail, finite ranges enumerate

1 files changed, 185 insertions, 10 deletions

diff --git a/lib/vm.ml b/lib/vm.ml
index 0d34e4a..a518aa5 100644
--- a/lib/vm.ml
+++ b/lib/vm.ml
@@ -97,6 +97,145 @@ module Make (W : World.WORLD) = struct
 
   let proven solutions = List.exists (fun (_, residue) -> residue = []) solutions
 
+  (* Interval propagation over waiting membership constraints. What
+     residuation returns inert, this looks at together: bounds with
+     an empty intersection fail the branch outright, and an integer
+     variable squeezed into a finite range converts to bounded
+     generation, the same admissible enumeration Between performs
+     explicitly. Sakura's cardinality analysis, inside the engine. *)
+  module Propagate = struct
+    let forced_label name =
+      match Label.of_string name with Ok l -> l | Error _ -> assert false
+
+    let value_l = forced_label "value"
+    let left_l = forced_label "left"
+    let right_l = forced_label "right"
+
+    type bound = { value : Q.t; strict : bool }
+
+    type info = {
+      integer : bool;
+      stringy : bool;
+      lower : bound option;
+      upper : bound option;
+    }
+
+    let no_info = { integer = false; stringy = false; lower = None; upper = None }
+
+    module M = Map.Make (String)
+
+    let note var f store =
+      M.update var
+        (fun info -> Some (f (Option.value ~default:no_info info)))
+        store
+
+    let stronger_lower a b =
+      if Q.gt a.value b.value then a
+      else if Q.lt a.value b.value then b
+      else { a with strict = a.strict || b.strict }
+
+    let stronger_upper a b =
+      if Q.lt a.value b.value then a
+      else if Q.gt a.value b.value then b
+      else { a with strict = a.strict || b.strict }
+
+    let add_lower bound info =
+      {
+        info with
+        lower =
+          Some
+            (match info.lower with
+            | None -> bound
+            | Some existing -> stronger_lower bound existing);
+      }
+
+    let add_upper bound info =
+      {
+        info with
+        upper =
+          Some
+            (match info.upper with
+            | None -> bound
+            | Some existing -> stronger_upper bound existing);
+      }
+
+    let numeric_value = function
+      | Pattern.Integer z -> Some (Q.of_bigint z)
+      | Pattern.Rational q -> Some q
+      | _ -> None
+
+    (* Read one waiting builtin goal into the store. Bindings arrive
+       already resolved, so a variable here is genuinely unbound. *)
+    let gather store (name, bindings) =
+      let value = Label.Map.find_opt value_l bindings
+      and left = Label.Map.find_opt left_l bindings
+      and right = Label.Map.find_opt right_l bindings in
+      match (name, value, left, right) with
+      | ("Integer" | "Natural"), Some (Pattern.Var x), _, _ ->
+          let store = note x (fun i -> { i with integer = true }) store in
+          if String.equal name "Natural" then
+            note x (add_lower { value = Q.zero; strict = false }) store
+          else store
+      | "String", Some (Pattern.Var x), _, _ ->
+          note x (fun i -> { i with stringy = true }) store
+      | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"),
+          _,
+          Some left,
+          Some right ) -> (
+          let strict =
+            String.equal name "LessThan" || String.equal name "GreaterThan"
+          in
+          let less = String.equal name "LessThan" || String.equal name "LessThanEqual" in
+          match (left, right) with
+          | Pattern.Var x, ground when Option.is_some (numeric_value ground) ->
+              let bound = { value = Option.get (numeric_value ground); strict } in
+              note x (if less then add_upper bound else add_lower bound) store
+          | ground, Pattern.Var x when Option.is_some (numeric_value ground) ->
+              let bound = { value = Option.get (numeric_value ground); strict } in
+              note x (if less then add_lower bound else add_upper bound) store
+          | _ -> store)
+      | _ -> store
+
+    (* Integer endpoints of a rational interval. *)
+    let lower_int { value; strict } =
+      let n = Q.num value and d = Q.den value in
+      if strict then Z.add (Z.fdiv n d) Z.one else Z.cdiv n d
+
+    let upper_int { value; strict } =
+      let n = Q.num value and d = Q.den value in
+      if strict then Z.sub (Z.cdiv n d) Z.one else Z.fdiv n d
+
+    type verdict = Fail | Enumerate of string * Z.t * Z.t | Unknown
+
+    let analyze constraints =
+      let store = List.fold_left gather M.empty constraints in
+      let contradictory _ info =
+        (info.stringy && (info.integer || info.lower <> None || info.upper <> None))
+        ||
+        match (info.lower, info.upper) with
+        | Some lo, Some hi ->
+            Q.gt lo.value hi.value
+            || (Q.equal lo.value hi.value && (lo.strict || hi.strict))
+            || (info.integer && Z.gt (lower_int lo) (upper_int hi))
+        | _ -> false
+      in
+      if M.exists contradictory store then Fail
+      else
+        match
+          M.choose_opt
+            (M.filter
+               (fun _ info ->
+                 info.integer && info.lower <> None && info.upper <> None)
+               store)
+        with
+        | Some (var, info) ->
+            Enumerate
+              ( var,
+                lower_int (Option.get info.lower),
+                upper_int (Option.get info.upper) )
+        | None -> Unknown
+  end
+
   let rec try_goal world subst goal =
     match goal with
     | Negated denial ->
@@ -200,16 +339,52 @@ module Make (W : World.WORLD) = struct
             List.concat_map
               (fun (subst, extra) -> search world subst (extra @ remaining))
               branches
-        | None ->
-            if
-              List.for_all
-                (fun goal ->
-                  match try_goal world subst goal with
-                  | Wait { residuatable } -> residuatable
-                  | Run _ -> false)
-                goals
-            then [ (subst, goals) ]
-            else raise (Stuck (List.map goal_name goals)))
+        | None -> (
+            (* Everything waits. Propagate over the waiting
+               membership constraints before residuating or
+               rejecting: they may be jointly unsatisfiable, or may
+               pin a variable into a finite range that unblocks the
+               rest. *)
+            let attempts = List.map (fun g -> (g, try_goal world subst g)) goals in
+            let membership =
+              List.filter_map
+                (fun (goal, attempt) ->
+                  match (goal, attempt) with
+                  | ( Positive (World.Apply (name, bindings)),
+                      Wait { residuatable = true } ) ->
+                      Some
+                        ( name,
+                          Label.Map.map (Pattern.Subst.resolve subst) bindings )
+                  | _ -> None)
+                attempts
+            in
+            match Propagate.analyze membership with
+            | Propagate.Fail -> []
+            | Propagate.Enumerate (var, lo, hi) ->
+                let rec enumerate v acc =
+                  if Z.gt v hi then acc
+                  else
+                    let branch =
+                      match
+                        Pattern.Subst.unify subst (Pattern.Var var)
+                          (Pattern.Integer v)
+                      with
+                      | Some subst -> search world subst goals
+                      | None -> []
+                    in
+                    enumerate (Z.succ v) (acc @ branch)
+                in
+                enumerate lo []
+            | Propagate.Unknown ->
+                if
+                  List.for_all
+                    (fun (_, attempt) ->
+                      match attempt with
+                      | Wait { residuatable } -> residuatable
+                      | Run _ -> false)
+                    attempts
+                then [ (subst, goals) ]
+                else raise (Stuck (List.map goal_name goals))))
 
   (* Solution variables: the free variables of the query. Whatever
      occurs only under a universal is bound per quantifier solution