Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(AC): Abstract AC arguments that contain other AC symbols #990

Merged
merged 2 commits into from
Mar 14, 2024
Merged

fix(AC): Abstract AC arguments that contain other AC symbols #990

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7d9cec2
fix(AC): Abstract AC arguments that contain other AC symbols
bclement-ocp Nov 29, 2023
38a33ba
Add paper doi
bclement-ocp Mar 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 48 additions & 7 deletions src/lib/reasoners/ac.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,26 +163,67 @@ module Make (X : Sig.X) = struct
let fold_flatten sy f =
List.fold_left (fun z (rt,n) -> flatten sy ((f rt),n) z) []

let abstract2 sy t r acc =
let is_other_ac_symbol sy r =
match X.ac_extract r with
| Some ac when Sy.equal sy ac.h -> r, acc
| None -> r, acc
| Some _ -> match Expr.term_view t with
| { Expr.f = Sy.Name { hs; kind = Sy.Ac; _ }; xs; ty; _ } ->
| Some ac -> not (Sy.equal sy ac.h)
| None -> false

(* This implements a variant of the term abstraction process described in
section 6 of the AC(X) paper [1].

The abstraction process given in the paper requires to abstract all AC
symbols appearing in a non-AC context, but the implementation does not
know about the context at the time the abstraction is performed (note that
rules Abstract1 and Abstract2 are concerned with *equations* while the
abstraction process here occurs at the time of building semantic values,
Comment on lines +177 to +178
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I understand well, in the paper we first define a set of terms T and equations s = t with s, t \in T and we consider a subset of equations (named abstracted equations (technically it's not a subset as we introduce abstract variables from a fresh set K)) on which the multiset order should ensure the termination of the AC(X) procedure.

In the implementation, we never produce the superset of equations because the terms (named semantic values in the implementation) are abstracted by construction?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is something like that, yes — in the paper we first build the equations and then perform term abstraction until all equations are in "abstracted form" (note that being abstracted is a condition on the equation, not on the term). But in the implementation we abstract terms when building semantic values, and so we must make sure that all possible equations between arbitrary semantic values are in abstracted form.

In particular, this implies (definition of T_AC) that AC symbols that appear at any depth inside the arguments of another AC symbol must be abstracted, which is what this PR enforces.

There might be additional properties that we need to enforce to ensure completeness; for instance, it is still possible to build equalities between uninterpreted/AC terms which should not be allowed as per the paper (one at least must be abstracted as per Definition 6.1). I think that this turns out OK because comparison between AC semantic values/terms starts by comparing the head symbol, and everything behaves as if the term with smallest head symbol was always abstracted in a consistent way — but I have done no proof and could easily be wrong.

which is earlier). Further, the implementation seems to implicitly rely on
term ordering (older terms are ordered before newer terms, so in
particular subterms are always smaller than terms that contains them) to
cheaply prevent loops rather than introducing all the abstracted variables
that the theoretical presentation in the paper would require.

So the implementation below of the Abstract2 rules deviates from the
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.
See also https://github.com/OCamlPro/alt-ergo/issues/989

[1]: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories:
Design and Implementation.
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala.
lmcs:1034 - Logical Methods in Computer Science, September 14, 2012,
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess this is the only important line in this PR :)

Let's u and v two distinct AC symbols (for sake of simplicity, say that u and v are binary integer operators).
Consider the expressions A := u(v(x, y), z) and B := u(v(x, y) + t, z).

In the previous implementation, we abstracted the subterm v(x, y) in the former case but we don't in the latter one.

In the new implementation, we'll abstract both of them because v(x, y) is now a leaf of an argument of u and u is distinct of v.

If we replace the operator + by a non-ac uninterpreted symbol, we don't abstract the subterm v(x, y), right? For instance we don't abstract v(x, y) in the term u(h(v(x, y), t), z) where h is a non-ac uninterpreted operator.

I guess the notation Σ_∅ in 𝒯_∅ in the paper denotes the interpreted symbols?

We don't need to abstract uninterpreted symbols here because, by definition they are already abstracted, so there is no relation between h(x, y) and h(y, x) that can induce an infinity path in the reduction algorithm?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes exactly — uninterpreted terms do not take part in this process because with semantic values we never look inside uninterpreted terms to see that they actually contain AC symbols. Instead, if we merge AC terms, say we have h(v(x, v(y, z))) and h(v(v(x, y), z)), the AC theory will normalize v(x, v(y, z)) and v(v(x, y), z) (as semantic values) to the same representative, it will be picked up by CC(X) to prove equality of the two h terms. But we never actually look inside or indeed rewrite inside uninterpreted terms.

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
| { Expr.f = Sy.Op Sy.Mult; xs; ty; _ } ->
| 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
| { Expr.ty; _ } ->
| _, { ty; _ } ->
let k = Expr.fresh_name ty in
let eq = Expr.mk_eq ~iff:false k t in
X.term_embed k, eq::acc

else
r, acc

let make t =
match Expr.term_view t with
| { Expr.f = sy; xs = [a;b]; ty; _ } when Sy.is_ac sy ->
Expand Down
292 changes: 292 additions & 0 deletions tests/dune.inc
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 4 additions & 0 deletions tests/issues/964.ae
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
logic ac u : int, int -> int
logic ac v : int, int -> int

goal g : v(0, 1) = u(-v(0, 1), 2)
2 changes: 2 additions & 0 deletions tests/issues/964.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

unknown
Loading