search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Support AC modifier in SMT input format #783

Open Halbaroth opened 1 year ago

Halbaroth commented 1 year ago

While I was porting the documentation of AE from Sphinx to odoc, I noticed there is no support for the ac modifier in the SMT-LIB input format.

I create this issue as a remainder.

I am not sure how to implement this properly.

bclement-ocp commented 1 year ago

The ac modifier does not exist in the SMT-LIB language, and there is no support for modifiers on function declarations. I think that the most natural way (for users) to implement this (while preserving soundness for other solvers) would be to support modifiers on commutativity/associativity assertions:

(declare-fun f (A A) A)
(assert (! (forall ((x A) (y A)) (= (f x y) (f y x))) :ae-comm f))
(assert (! (forall ((x A) (y A) (z A)) (= (f x (f y z)) (f (f x y) z))) :ae-assoc f))

We could implement this by checking that the assertion with :ae-comm f (resp. :ae-assoc f) is a commutativity (resp. associativity) axiom for f, and if there are both (valid) associativity and commutativity axioms for a declared function f, we create a new AC symbol @f and add the assertion:

(assert (forall ((x A) (y A)) (= (f x y) (@f x y))

Although I believe we would need a way to force this to be a rewriting from f to @f for AC(X) to work properly.