Forward Solvers: Split local unknowns by digests

src/common/domains/printable.ml

@@ -470,6 +470,63 @@ struct
     | `Lifted2 x -> Base2.to_yojson x
 end
 
+module type Lift3Conf =
+sig
+  include Lift2Conf
+  val expand3: bool
+end
+
+module Lift3Conf (Conf: Lift3Conf) (Base1: S) (Base2: S) (Base3: S) =
+struct
+  open struct
+    module Base1 = PrefixName (struct let expand = Conf.expand1 end) (Base1)
+    module Base2 = PrefixName (struct let expand = Conf.expand2 end) (Base2)
+    module Base3 = PrefixName (struct let expand = Conf.expand3 end) (Base3)
+  end
+
+  type t = [`Bot | `Lifted1 of Base1.t | `Lifted2 of Base2.t | `Lifted3 of Base3.t | `Top] [@@deriving eq, ord, hash]
+  include Std
+  open Conf
+
+  let pretty () (state:t) =
+    match state with
+    | `Lifted1 n ->  Base1.pretty () n
+    | `Lifted2 n ->  Base2.pretty () n
+    | `Lifted3 n ->  Base3.pretty () n
+    | `Bot -> text bot_name
+    | `Top -> text top_name
+
+  let show state =
+    match state with
+    | `Lifted1 n ->  Base1.show n
+    | `Lifted2 n ->  Base2.show n
+    | `Lifted3 n ->  Base3.show n
+    | `Bot -> bot_name
+    | `Top -> top_name
+
+  let relift x = match x with
+    | `Lifted1 n -> `Lifted1 (Base1.relift n)
+    | `Lifted2 n -> `Lifted2 (Base2.relift n)
+    | `Lifted3 n -> `Lifted3 (Base3.relift n)
+    | `Bot | `Top -> x
+
+  let name () = "lifted " ^ Base1.name () ^ " and " ^ Base2.name () ^ " and " ^ Base3.name ()
+
+  let printXml f = function
+    | `Bot       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" bot_name
+    | `Top       -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" top_name
+    | `Lifted1 x -> Base1.printXml f x
+    | `Lifted2 x -> Base2.printXml f x
+    | `Lifted3 x -> Base3.printXml f x
+
+  let to_yojson = function
+    | `Bot -> `String bot_name
+    | `Top -> `String top_name
+    | `Lifted1 x -> Base1.to_yojson x
+    | `Lifted2 x -> Base2.to_yojson x
+    | `Lifted3 x -> Base3.to_yojson x
+end
+
 module type ProdConfiguration =
 sig
   val expand_fst: bool
@@ -571,6 +628,56 @@ struct
   let arbitrary () = QCheck.triple (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ())
 end
 
+module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) =
+struct
+  type t = Base1.t * Base2.t * Base3.t * Base4.t [@@deriving eq, ord, hash, relift]
+  include Std
+
+  let show (x,y,z,w) =
+    let first  = Base1.show x in
+    let second = Base2.show y in
+    let third  = Base3.show z in
+    let fourth = Base4.show w in
+    "(" ^ first ^ ", " ^ second ^ ", " ^ third ^ ", " ^ fourth ^ ")"
+
+  let pretty () (x,y,z,w) =
+    text "("
+    ++ text (Base1.name ())
+    ++ text ":"
+    ++ align
+    ++ Base1.pretty () x
+    ++ unalign
+    ++ text ", "
+    ++ text (Base2.name ())
+    ++ text ":"
+    ++ align
+    ++ Base2.pretty () y
+    ++ unalign
+    ++ text ", "
+    ++ text (Base3.name ())
+    ++ text ":"
+    ++ align
+    ++ Base3.pretty () z
+    ++ unalign
+    ++ text ", "
+    ++ text (Base4.name ())
+    ++ text ":"
+    ++ align
+    ++ Base4.pretty () w
+    ++ unalign
+    ++ text ")"
+
+  let printXml f (x,y,z,w) =
+    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y (XmlUtil.escape (Base3.name ())) Base3.printXml z (XmlUtil.escape (Base4.name ())) Base4.printXml w
+
+  let to_yojson (x, y, z, w) =
+    `Assoc [ (Base1.name (), Base1.to_yojson x); (Base2.name (), Base2.to_yojson y); (Base3.name (), Base3.to_yojson z); (Base4.name (), Base4.to_yojson w) ]
+
+  let name () = Base1.name () ^ " * " ^ Base2.name () ^ " * " ^ Base3.name () ^ " * " ^ Base4.name ()
+
+  let arbitrary () = QCheck.tup4 (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ())
+end
+
 module PQueue (Base: S) =
 struct
   type t = Base.t BatDeque.dq

src/config/options.schema.json

@@ -2497,6 +2497,12 @@
               "description": "How often a contribution should simply overwrite the old one when incomparible instead of widening",
               "type": "integer",
               "default": 0
+            },
+            "digests": {
+              "title": "solvers.fwd.digests",
+              "description": "Whether the constraint system to be solved should use digests to realize path-sensitivity.",
+              "type": "boolean",
+              "default": true
             }
           },
           "additionalProperties": false

src/domain/lattice.ml

@@ -381,6 +381,95 @@ end
 
 module Lift2 = Lift2Conf (Printable.DefaultConf)
 
+module Lift3Conf (Conf: Printable.Lift3Conf) (Base1: PO) (Base2: PO) (Base3: PO) =
+struct
+  include Printable.Lift3Conf (Conf) (Base1) (Base2) (Base3)
+
+  let bot () = `Bot
+  let is_bot x = x = `Bot
+  let top () = `Top
+  let is_top x = x = `Top
+
+  let leq x y =
+    match (x,y) with
+    | (_, `Top) -> true
+    | (`Top, _) -> false
+    | (`Bot, _) -> true
+    | (_, `Bot) -> false
+    | (`Lifted1 x, `Lifted1 y) -> Base1.leq x y
+    | (`Lifted2 x, `Lifted2 y) -> Base2.leq x y
+    | (`Lifted3 x, `Lifted3 y) -> Base3.leq x y
+    | _ -> false
+
+  let pretty_diff () ((x:t),(y:t)): Pretty.doc =
+    match x, y with
+    | `Lifted1 x, `Lifted1 y -> Base1.pretty_diff () (x, y)
+    | `Lifted2 x, `Lifted2 y -> Base2.pretty_diff () (x, y)
+    | `Lifted3 x, `Lifted3 y -> Base3.pretty_diff () (x, y)
+    | _ when leq x y -> Pretty.text "No Changes"
+    | _ -> Pretty.dprintf "%a instead of %a" pretty x pretty y
+
+  let join x y =
+    match (x,y) with
+    | (`Top, _) -> `Top
+    | (_, `Top) -> `Top
+    | (`Bot, x) -> x
+    | (x, `Bot) -> x
+    | (`Lifted1 x, `Lifted1 y) -> begin
+        try `Lifted1 (Base1.join x y)
+        with TopValue -> `Top
+      end
+    | (`Lifted2 x, `Lifted2 y) -> begin
+        try `Lifted2 (Base2.join x y)
+        with TopValue -> `Top
+      end
+    | (`Lifted3 x, `Lifted3 y) -> begin
+        try `Lifted3 (Base3.join x y)
+        with TopValue -> `Top
+      end
+    | _ -> `Top
+
+  let meet x y =
+    match (x,y) with
+    | (`Bot, _) -> `Bot
+    | (_, `Bot) -> `Bot
+    | (`Top, x) -> x
+    | (x, `Top) -> x
+    | (`Lifted1 x, `Lifted1 y) -> begin
+        try `Lifted1 (Base1.meet x y)
+        with BotValue -> `Bot
+      end
+    | (`Lifted2 x, `Lifted2 y) -> begin
+        try `Lifted2 (Base2.meet x y)
+        with BotValue -> `Bot
+      end
+    | (`Lifted3 x, `Lifted3 y) -> begin
+        try `Lifted3 (Base3.meet x y)
+        with BotValue -> `Bot
+      end
+    | _ -> `Bot
+
+  let widen x y =
+    match (x,y) with
+    | (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.widen x y)
+    | (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.widen x y)
+    | (`Lifted3 x, `Lifted3 y) -> `Lifted3 (Base3.widen x y)
+    | _ -> y
+
+  let narrow x y =
+    match (x,y) with
+    | (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.narrow x y)
+    | (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.narrow x y)
+    | (`Lifted3 x, `Lifted3 y) -> `Lifted3 (Base3.narrow x y)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
+    | _ -> x
+end
+
+module Lift3 = Lift3Conf (Printable.DefaultConf)
+
+
+
 module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
 struct
   open struct (* open to avoid leaking P and causing conflicts *)