Expose solver mappings to declare non-parametric datatypes

[filipeom]

This is to allow creating examples such as this:

(declare-datatype Ptr ((mk-ptr (loc Int) (ofs Int))))
(declare-const p1 (Ptr))
(assert (= p1 (mk-ptr 10 8)))
(assert (= (loc p1) 10))
(assert (= (ofs p1) 8))
(check-sat)
(get-model)

cc @hra687261 (and anyone who wants to help 😅). I'm not very comfortable with ADTs in SMT, so I would appreciate your help with this one. I left some of my questions below:

Do you thing the API for Adt and Adt.Cons are ok? In particular, do you think the get_constructor, get_recognizers, and get_accessors provide an awkward api? Maybe having val get_constructor : t -> cons_name:string -> Cons.t would be better? (Same logic for the others)

I like the Dolmen_std.Expr.Term.define_adt interface but I don't really understand how the API works. Do you have some example usages so I can finish the API for dolmen to have adt support in Alt-Ergo?

[hra687261]

In particular, do you think the get_constructor, get_recognizers, and get_accessors provide an awkward api?

Assuming that accessors are descructors and recognizers are testers, I am not exactly sure of how this API would be used.
Is the idea is to get all the accessors/recognizers and then select the right one to use?
If that is the case, then I agree it is a bit awkward, I think in practice you would have the name of one of them (as a string maybe) and you would want to get the corresponding term so I agree with this:

Maybe having val get_constructor : t -> cons_name:string -> Cons.t would be better? (Same logic for the others)

In the documentation there is the following example:

define_adt "list" [a] 
  [ "nil", [];
    "const", 
    [ (Ty.of_var a, Some "hd");
      (list(a), Some "tl"); 
    ];
  ]

So in your example it would be:

define_adt "Ptr" [] 
  [ "mk-ptr", 
    [ (Int, Some "loc");
      (Int, Some "ofs"); 
    ];
  ]

To create an instance of mk-ptr you would call: apply_cstr mk_ptr_cstr [] [10;8]

If you want, you can leave it as blank for now, I can add it later, you can create an issue and assign me.
Notably because I think we would need some kind of mapping from fields/constructors to the corresponding DTerm.Const.t constructor.

[filipeom]

Assuming that accessors are descructors and recognizers are testers, I am not exactly sure of how this API would be used.

Regarding terminology I used accessors and recognizers because those were the names of the z3 api 😅 Is destructors and testers the right terminology in SMT-LIB? I found selector and tester in page 65 of https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-04-09.pdf. What do you think we should use?

Is the idea is to get all the accessors/recognizers and then select the right one to use?

Yeah exactly. I added a test that shows this:

    let ptr_adt =
      Adt.make "Ptr"
        [ Adt.Cons.make "mk-ptr"
            ~fields:[ ("loc", Some Types.int); ("ofs", Some Types.int) ]
        ]
    in
    let ty = Adt.ty ptr_adt in
    let loc, ofs =
      let acessors = Adt.get_accessors ptr_adt |> List.hd in
      (List.nth acessors 0, List.nth acessors 1)
    in
    let mk_ptr = Adt.get_constructors ptr_adt |> List.hd in
    let p1 = const "p1" ty in
    let solver = Solver.make () in
    Solver.add solver
      [ eq p1 (Func.apply mk_ptr [ int 10; int 8 ])
      ; eq (Func.apply loc [ p1 ]) (int 10)
      ; eq (Func.apply ofs [ p1 ]) (int 8)
      ];

I find it a bit awkward to use I guess. Maybe I'll change it to:

val constructor : string -> t -> func_decl
val selector : string -> t -> func_decl 
val tester : string -> t -> func_decl 

And we can maybe use a List.assoc or a Map internally. I don't know if this would cause performance issues tho.

If you want, you can leave it as blank for now, I can add it later, you can create an issue and assign me.
Notably because I think we would need some kind of mapping from fields/constructors to the corresponding DTerm.Const.t constructor.

Okok, I will leave it blank for the time being

[hra687261]

Is destructors and testers the right terminology in SMT-LIB? I found selector and tester in page 65 of https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-04-09.pdf. What do you think we should use?

I am actually not sure, but that is what I always called them haha (terminology probably changes from a solver to another and from a language to another), but I think those of the SMT-LIB are good.

I find it a bit awkward to use I guess. Maybe I'll change it to:

val constructor : string -> t -> func_decl
val selector : string -> t -> func_decl 
val tester : string -> t -> func_decl 

I agree with this signature.

And we can maybe use a List.assoc or a Map internally. I don't know if this would cause performance issues tho.

I think we will need to do a sort of "type-checking" anyway to ensure that a given field or constructor is indeed defined for the type of the term on which it is applied, so a Map.find or List.assoc will probably be necessary.

[filipeom]

Thanks for the help @hra687261. If we find this API is not very good we can improve on in the future