Skip to content

Commit

Permalink
feat(shostak): Transparent abstracted constants
Browse files Browse the repository at this point in the history 
This patch introduces a new type of leaf in the Shostak module, called
*abstract leaves*. Abstract leaves behave like constant terms, and are
intended to replace the `X.term_embed (E.fresh_name ty)` pattern where
possible.

An abstract leaf is created by calling `X.abstract` on an existing
semantic value `r`. The abstract leaf `X.abstract r` is automatically
defined to be equal to `r` when processed by the `Uf` and `Ccx` modules.

The benefits of abstract leaves over fresh term constants are twofold:

 - With fresh constants, when the same semantic value is abstracted
   multiple times, a new constant is created for each abstraction.
   Semantically, this is correct; however, this causes the introduction
   of unnecessary constants in the union-find that will just end up in
   the same equivalence class. With abstract leaves, abstracting the
   same semantic value multiple times always returns the same constant.

 - With fresh constants, an additional equation between the new constant
   and the original term to abstract must be kept and processed
   separately. Since abstract leaves embed their definition, the
   additional equations can be introduced automatically by the `Uf` and
   `Ccx` modules and do not need to be carried separately.

Abstract leaves are currently only used by the AC theory. In the future,
it is intended to be used as a basis for implementing application of
interpreted-but-not-solvable functions to semantic values (so that for
instance we can denote `bv2nat(r)` where `r` is a semantic value). While
it would be straightforward to adapt abstract leaves to be able to
create terminal leaves for `bv2nat(r)` (without definitional equations),
we want congruence closure and computation (so that `bv2nat(x @ y)`
automatically becomes `bv2nat(x) * 2^n + bv2nat(y)`) to work for such
leaves. This require additional adaptations to CC(X), and is expected to
need abstract leaves to enforce an AC(X)-compatible ordering.
  • Loading branch information
@bclement-ocp
bclement-ocp committed Aug 7, 2024
1 parent 6424e77 commit 6c3ae05
Show file tree
Hide file tree
Showing 12 changed files with 180 additions and 122 deletions.
50 changes: 16 additions & 34 deletions src/lib/reasoners/ac.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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; \
Expand Down
9 changes: 2 additions & 7 deletions src/lib/reasoners/arith.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
9 changes: 8 additions & 1 deletion src/lib/reasoners/ccx.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ?*)
Expand Down
10 changes: 5 additions & 5 deletions src/lib/reasoners/intervalCalculus.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
75 changes: 64 additions & 11 deletions src/lib/reasoners/shostak.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand All @@ -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);
Expand All @@ -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 < Term < Abstract < Ac *)
let theory_num x = match x with
| Ac _ -> -1
| Term _ -> -2
| Arith _ -> -3
| Records _ -> -4
| Bitv _ -> -5
| Abstract _ -> -2
| Term _ -> -3
| Arith _ -> -4
| Records _ -> -5
| Bitv _ -> -6
| Adt _ -> -7

let compare_tag a b = theory_num a - theory_num b
Expand All @@ -278,6 +327,9 @@ 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) ->
let c = compare_abs_kind kx ky in
if c <> 0 then c else CX.str_cmp x y
| Ac x, Ac y -> AC.compare x y
| va, vb -> compare_tag va vb

Expand Down Expand Up @@ -322,7 +374,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
Expand All @@ -338,7 +390,7 @@ struct
| Symbols.(True | False), [] -> true
| _ -> false
end
| Ac _ -> false
| Abstract _ | Ac _ -> false

let subst p v r =
if equal p v then r
Expand All @@ -348,6 +400,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 =
Expand Down Expand Up @@ -416,7 +469,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 =
Expand Down Expand Up @@ -448,7 +501,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 =
Expand Down Expand Up @@ -483,7 +536,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
Expand Down
Loading

0 comments on commit 6c3ae05

Please sign in to comment.