feat(shostak): Transparent abstracted constants

src/lib/reasoners/ac.ml

@@ -183,10 +183,10 @@ module Make (X : Sig.X) = struct
      presentation in the paper to accomodate those differences, globally,
      between the implementation and theoretical description of AC(X).
 
-     More precisely, `abstract2` will abstract terms that *contain* AC leaves
-     when they appear as argument of an AC symbol. This ensures that AC terms
-     satisfy the T_AC definition from page 22 of the paper, although
-     correctness of the corresponding abstraction process has not been proven.
+     More precisely, `abstract2` will abstract all AC leaves that appear in the
+     arguments of an AC symbol. This ensures that AC terms satisfy the T_AC
+     definition from page 22 of the paper, although correctness of the
+     corresponding abstraction process has not been formally proven.
      See also https://github.com/OCamlPro/alt-ergo/issues/989
 
      [1]: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories:
@@ -196,42 +196,24 @@ module Make (X : Sig.X) = struct
             Volume 8, Issue 3.
           doi:10.2168/LMCS-8(3:16)2012
           https://arxiv.org/pdf/1207.3262.pdf *)
-  let abstract2 sy t r acc =
-    if List.exists (is_other_ac_symbol sy) (X.leaves r) then
-      match X.ac_extract r, Expr.term_view t with
-      | Some ac, { f = Name { hs; kind = Ac; _ } ; xs; ty; _ } ->
-        (* It should have been abstracted when building [r] *)
-        assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in
-        let aro_t = Expr.mk_term aro_sy xs ty  in
-        let eq = Expr.mk_eq ~iff:false aro_t t in
-        X.term_embed aro_t, eq::acc
-      | Some ac, { f = Op Mult; xs; ty; _ } ->
-        (* It should have been abstracted when building [r] *)
-        assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal "@*" in
-        let aro_t = Expr.mk_term aro_sy xs ty  in
-        let eq = Expr.mk_eq ~iff:false aro_t t in
-        X.term_embed aro_t, eq::acc
-      | _, { ty; _ } ->
-        let k = Expr.fresh_ac_name ty in
-        let eq = Expr.mk_eq ~iff:false k t in
-        X.term_embed k, eq::acc
-
-    else
-      r, acc
+  let rec abstract2 sy r =
+    match List.find (is_other_ac_symbol sy) (X.leaves r) with
+    | ac_lv ->
+      (* Abstraction in depth: [f(x, y) + 1] -> [@ac(f(x, y) + 1]
+         and not [@ac(f(x, y) + 1)]. *)
+      abstract2 sy (X.subst ac_lv (X.abstract ~kind:Ac ac_lv) r)
+    | exception Not_found -> r
 
   let make t =
     match Expr.term_view t with
     | { Expr.f = sy; xs = [a;b]; ty; _ } when Sy.is_ac sy ->
       let ra, ctx1 = X.make a in
       let rb, ctx2 = X.make b in
-      let ra, ctx = abstract2 sy a ra (ctx1 @ ctx2) in
-      let rb, ctx = abstract2 sy b rb ctx in
-      let rxs = [ ra,1 ; rb,1 ] in
-      X.ac_embed {h=sy; l=compact (fold_flatten sy (fun x -> x) rxs); t=ty;
-                  distribute = true},
-      ctx
+      let l = flatten sy (rb, 1) @@ flatten sy (ra, 1) [] in
+      let l = List.map (fun (r, n) -> (abstract2 sy r, n)) l in
+      let l = compact (fold_flatten sy (fun x -> x) l) in
+      X.ac_embed {h=sy; l; t=ty;distribute = true},
+      ctx1 @ ctx2
     | {xs; _} ->
       Printer.print_err
         "AC theory expects only terms with 2 arguments; \

src/lib/reasoners/arith.ml

@@ -452,12 +452,7 @@ module Shostak
       List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l
 
   let contains_a_fresh_alien xp =
-    List.exists
-      (fun x ->
-         match X.term_extract x with
-         | Some t, _ -> E.is_fresh_ac_name t
-         | _ -> false
-      ) (X.leaves xp)
+    List.exists (X.is_abstract ~kind:Ac) (X.leaves xp)
 
   let has_ac p kind =
     List.exists
@@ -540,7 +535,7 @@ module Shostak
     List.fold_left
       (fun (l, sb) (b, y) ->
          if X.ac_extract y != None && X.str_cmp y x > 0 then
-           let k = X.term_embed (E.fresh_ac_name Ty.Tint) in
+           let k = X.abstract ~kind:Ac y in
            (b, k) :: l, (y, embed k)::sb
          else (b, y) :: l, sb)
       ([], []) l

src/lib/reasoners/ccx.ml

@@ -489,7 +489,14 @@ module Main : S = struct
       let { E.xs; _ } = E.term_view t in
       let env = List.fold_left (fun env t -> add_term env facts t ex) env xs in
       (* we update uf and use *)
-      let nuf, ctx  = Uf.add env.uf t in
+      let nuf, abs, ctx  = Uf.add env.uf t in
+      (* process definitional equality of abstracted terms *)
+      List.iter (fun r ->
+          match X.abstract_extract r with
+          | Some r' ->
+            add_fact facts (LSem (LR.mkv_eq r r'), Ex.empty, Th_util.Other)
+          | None -> assert false
+        ) abs;
       Debug.make_cst t ctx;
       List.iter (fun a -> add_fact facts (LTerm a, ex, Th_util.Other)) ctx;
       (*or Ex.empty ?*)

src/lib/reasoners/intervalCalculus.ml

@@ -2234,7 +2234,7 @@ let domain_matching _lem_name tr sbt env uf optimized =
            | E.Interval (t, lb, ub) ->
              let tt = E.apply_subst sbt t in
              assert (E.is_ground tt);
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              let rr, _ex = Uf.find uf tt in
              let p = poly_of rr in
              let p', c', d = P.normal_form_pos p in
@@ -2247,15 +2247,15 @@ let domain_matching _lem_name tr sbt env uf optimized =
 
            | E.NotTheoryConst t ->
              let tt = E.apply_subst sbt t in
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              if X.leaves (fst (Uf.find uf tt)) == [] ||
                 X.leaves (fst (X.make tt)) == [] then
                raise (Sem_match_fails env);
              idoms, maps_to, env, uf
 
            | E.IsTheoryConst t ->
              let tt = E.apply_subst sbt t in
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              let r, _ = X.make tt in
              if X.leaves r != [] then raise (Sem_match_fails env);
              idoms, maps_to, env, uf
@@ -2265,8 +2265,8 @@ let domain_matching _lem_name tr sbt env uf optimized =
              let y = E.apply_subst sbt y in
              if not (terms_linear_dep env [x;y]) then
                raise (Sem_match_fails env);
-             let uf, _ = Uf.add uf x in
-             let uf, _ = Uf.add uf y in
+             let uf, _, _ = Uf.add uf x in
+             let uf, _, _ = Uf.add uf y in
              idoms, maps_to, env, uf
         )(Var.Map.empty, [], env, uf) tr.E.semantic
     in

src/lib/reasoners/shostak.ml

@@ -27,6 +27,22 @@
 
 (*** Combination module of Shostak theories ***)
 
+let equal_abs_kind k1 k2 =
+  match k1, k2 with
+  | Sig.Ac, Sig.Ac -> true
+
+let hash_abs_kind k =
+  match k with
+  | Sig.Ac -> 1
+
+let compare_abs_kind k1 k2 =
+  match k1, k2 with
+  | Sig.Ac, Sig.Ac -> 0
+
+let pp_abs_kind ppf k =
+  match k with
+  | Sig.Ac -> Fmt.pf ppf "ac"
+
 [@@@ocaml.warning "-60"]
 module rec CX : sig
   include Sig.X
@@ -51,6 +67,7 @@ struct
 
   type rview =
     | Term of Expr.t
+    | Abstract of Sig.abs_kind * CX.r
     | Ac of AC.t
     | Arith of ARITH.t
     | Records of RECORDS.t
@@ -72,6 +89,7 @@ struct
         | Bitv t -> fprintf fmt "%a" BITV.print t
         | Adt t -> fprintf fmt "%a" ADT.print t
         | Term t -> fprintf fmt "%a" Expr.print t
+        | Abstract (k, t) -> fprintf fmt "@@%a(%a)" pp_abs_kind k CX.print t
         | Ac t -> fprintf fmt "%a" AC.print t
       end
       else begin
@@ -86,6 +104,8 @@ struct
           fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t
         | Term t ->
           fprintf fmt "FT:[%a]" Expr.print t
+        | Abstract (k, t) ->
+          fprintf fmt "K:%a[%a]" pp_abs_kind k CX.print t
         | Ac t ->
           fprintf fmt "Ac:[%a]" AC.print t
       end
@@ -165,6 +185,8 @@ struct
         | Bitv x -> 3 + 10 * BITV.hash x
         | Adt x -> 6 + 10 * ADT.hash x
         | Ac ac -> 9 + 10 * AC.hash ac
+        | Abstract (k, t) ->
+          7 + 10 * (5003 * (hash_abs_kind k) + CX.hash t)
         | Term t -> 8 + 10 * Expr.hash t
       in
       abs res
@@ -176,6 +198,8 @@ struct
       | Bitv x, Bitv y -> BITV.equal x y
       | Adt x, Adt y -> ADT.equal x y
       | Term x, Term y -> Expr.equal x y
+      | Abstract (kx, x), Abstract (ky, y) ->
+        equal_abs_kind kx ky && CX.equal x y
       | Ac x, Ac y -> AC.equal x y
       | _ -> false
 
@@ -214,6 +238,16 @@ struct
 
   let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)}
 
+  let abstract ~kind arg =
+    (* No need to nest abstractions
+       XXX: would it be OK to abstract terms into themselves? *)
+    let arg =
+      match arg.v with
+      | Abstract (_, arg) -> arg
+      | _ -> arg
+    in
+    hcons { v = Abstract (kind, arg); id = -1000 (* dummy *) }
+
   let extract1 = function { v=Arith r; _ } -> Some r | _ -> None
   let extract2 = function { v=Records r; _ } -> Some r | _ -> None
   let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None
@@ -223,13 +257,26 @@ struct
     | { v = Ac t; _ }   -> Some t
     | _ -> None
 
+  let is_abstract ?kind = function
+    | { v = Abstract (k, _); _ } -> (
+        match kind with
+        | None -> true
+        | Some k' -> equal_abs_kind k k'
+      )
+    | _ -> false
+
+  let abstract_extract = function
+    | { v = Abstract (_, r); _ } -> Some r
+    | _ -> None
+
   let term_extract r =
     match r.v with
     | Arith _ -> ARITH.term_extract r
     | Records _ -> RECORDS.term_extract r
     | Bitv _ -> BITV.term_extract r
     | Adt _ -> ADT.term_extract r
     | Ac _ -> None, false (* SYLVAIN : TODO *)
+    | Abstract _ -> None, false
     | Term t -> Some t, true
 
   let to_model_term r =
@@ -240,7 +287,7 @@ struct
       | Bitv _ -> BITV.to_model_term r
       | Adt _ -> ADT.to_model_term r
       | Term t when Expr.is_model_term t -> Some t
-      | Ac _ | Term _ -> None
+      | Abstract _ | Ac _ | Term _ -> None
     in
     Option.bind res @@ fun t ->
     assert (Expr.is_model_term t);
@@ -256,15 +303,17 @@ struct
     | { v = Adt t; _ } -> ADT.type_info t
     | { v = Ac x; _ } -> AC.type_info x
     | { v = Term t; _ } -> Expr.type_info t
+    | { v = Abstract (_, t); _ } -> CX.type_info t
 
   (* Constraint that must be maintained:
-     all theories should have Xi < Term < Ac *)
+     all theories should have Xi < Abstract < Term < Ac *)
   let theory_num x = match x with
     | Ac _ -> -1
     | Term  _ -> -2
-    | Arith _ -> -3
-    | Records _ -> -4
-    | Bitv _ -> -5
+    | Abstract _ -> -3
+    | Arith _ -> -4
+    | Records _ -> -5
+    | Bitv _ -> -6
     | Adt _ -> -7
 
   let compare_tag a b = theory_num a - theory_num b
@@ -278,6 +327,11 @@ struct
       | Bitv _, Bitv _ -> BITV.compare a b
       | Adt _, Adt _ -> ADT.compare a b
       | Term x, Term y -> Expr.compare x y
+      | Abstract (kx, x), Abstract (ky, y) ->
+        (* Make sure that new abstractions are smaller, i.e.
+           old abstractions are rewritten into new abstractions. *)
+        let c = Int.compare y.id x.id in
+        if c <> 0 then c else compare_abs_kind kx ky
       | Ac x, Ac y -> AC.compare x y
       | va, vb -> compare_tag va vb
 
@@ -322,7 +376,7 @@ struct
     | Bitv t -> BITV.leaves t
     | Adt t -> ADT.leaves t
     | Ac t -> r :: (AC.leaves t)
-    | Term _ -> [r]
+    | Term _ | Abstract _ -> [r]
 
   let is_constant r =
     match r.v with
@@ -338,7 +392,7 @@ struct
         | Symbols.(True | False), [] -> true
         | _ -> false
       end
-    | Ac _ -> false
+    | Abstract _ | Ac _ -> false
 
   let subst p v r =
     if equal p v then r
@@ -348,6 +402,7 @@ struct
       | Bitv t -> BITV.subst p v t
       | Adt t -> ADT.subst p v t
       | Ac t -> if equal p r then v else AC.subst p v t
+      | Abstract _ -> if equal p r then v else r
       | Term _ -> if equal p r then v else r
 
   let make t =
@@ -416,7 +471,7 @@ struct
      ADT.is_mine_symb sb)
 
   let is_a_leaf r = match r.v with
-    | Term _ | Ac _ -> true
+    | Term _ | Ac _ | Abstract _ -> true
     | _ -> false
 
   let color ac =
@@ -448,7 +503,7 @@ struct
     | Records a -> RECORDS.abstract_selectors a acc
     | Bitv a -> BITV.abstract_selectors a acc
     | Adt a -> ADT.abstract_selectors a acc
-    | Term _ -> a, acc
+    | Term _ | Abstract _ -> a, acc
     | Ac a -> AC.abstract_selectors a acc
 
   let abstract_equality a b =
@@ -483,7 +538,7 @@ struct
     let sbs =
       List.filter (fun (p,_) ->
           match p.v with
-          | Ac _ -> true | Term _ -> SX.mem p original
+          | Ac _ | Abstract _ -> true | Term _ -> SX.mem p original
           | _ ->
             Printer.print_err "%a" CX.print p;
             assert false