I encountered a problem. Say I have this in the ATS code
stacst set_emp: set = "ext@smt_set_emp" and this in the smt2 code (define-const smt_set_emp (Set) ((as const (Set)) false)) `--constraint-export` is able to translate all static applications of `smt_emp` to `smt_set_emp`. *However, it emits an extra definition which I don't want to have.* (declare-fun smt_set_emp () Set) What is your usual use case? Maybe we should remove this from emitted code. On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote: > > > In ATS2-0.2.8, a static constant can now be declared with an external name: > > For instance: > > stacst sine_of_real : real -> real = "ext#sin" > > This is useful when constraints generated during typechecking are to be > exported > for solving externally. If a static constant is given an external name, > then the external > name is used in exported constraints (otherwise, a name like > sine_of_real!12345 is > used, where 12345 is the stamp attached to the static constant). > > Here are some examples that you can try (using the given Makefile): > > > https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST > > Cheers! > > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/0e7c266b-47a6-4890-8180-51bdeb81f43b%40googlegroups.com.
