The built-in solver in ATS is very limited in its handling of datasorts
like the following one:
datasort item =
| a
| b
| c
In practice, I try to use integers instead:
sortdef item = int
#define item_a 0
#define item_b 1
#define item_c 2
On Tue, Apr 17, 2018 at 4:12 PM, M88 <abysgr...@gmail.com> wrote:
> I've been experimenting with Z3 and it's proven to be very useful. I
> would like to keep using the built-in constraint solver for various reasons.
>
> Perhaps this is a novice question, but how does one establish equality
> within a datasort?
>
> For example, given datasort
>
> datasort item
> | a
> | b
> | c
>
> How can I establish that a == a ?
>
> I can use scase, but that is only optimal for a small number of branches.
> It would be nice to use sif.
>
> I can declare a static function like
> stacst item_id : (item) -> int
> stacst item_eq : (item,item) -> bool
>
> extern praxi item_uniq : [
> item_id(a) == 1;
> item_id(b) == 2;
> item_id(c) == 3
> ] void
>
> extern praxi item_eq_praxi{a,b:item} : [
> item_eq(a,b) == (item_id(a) == item_id(b))
> ] void
>
> But the constraint solver still gives me errors, because either
> item_eq(a,b) == (a == b) does not resolve (eg, in a sif branch), or
> vice-versa (eg, in nested scase).
>
>
> On Sunday, April 8, 2018 at 7:47:12 AM UTC-4, gmhwxi wrote:
>>
>>
>> There are two styles of theorem-proving in ATS:
>>
>> http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-boo
>> l-vs-prop/index.html
>>
>> To avoid explicit quantifier elimination performed by the following code,
>>
>> prval () = isCA1_praxi{cB_1}()
>> prval () = isCA1_praxi{cB_2}()
>> prval () = isCA1_praxi{cB_3}()
>>
>> you can try:
>>
>> prval() = $solver_assert(isCA1_praxi)
>>
>> and then use Z3 to solve the generated constraints. Doing so means that you
>> are at the mercy
>>
>> of Z3's quantifier elimination heuristics or (black) magic.
>>
>>
>>
>> On Sat, Apr 7, 2018 at 9:09 PM, M88 <abys...@gmail.com> wrote:
>>
>>>
>>> It seems that isCA1_praxi should be declared
>>>> as follows:
>>>>
>>>> praxi
>>>> isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void
>>>>
>>>
>>> Yes, this makes sense -- I am looking for universal quantification.
>>>
>>> I suppose the issue here is how it would be invoked. Would I
>>> still need to invoke the proof as follows?
>>>
>>> prval () = isCA1_praxi{cB_1}()
>>> prval () = isCA1_praxi{cB_2}()
>>> prval () = isCA1_praxi{cB_3}()
>>>
>>> ********
>>>
>>> After giving this some thought, I realized I could invoke the proof
>>> within a constructor, omitting the need to explicitly specify each
>>> "catB."
>>>
>>> fun makeCA1 {cb:catB}() : [sa:sortA | isCA1(sa) ] typeA(sa)
>>>
>>> What tripped me up at first is that the return value of each constructor
>>> should specify the constraint "isCA1" if I use this approach, whereas
>>> the former let me invoke the proofs globally.
>>>
>>>
>>> On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>>>>>
>>>>>
>>>>> I was looking into the rock-paper-scissors example (here
>>>>> <https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs>
>>>>> and here
>>>>> <https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.dats>)
>>>>> and I found it very useful for learning how to define predicates in the
>>>>> statics.
>>>>>
>>>>> I had made an attempt something similar, but using independent
>>>>> datasorts as parameters.
>>>>>
>>>>> For example:
>>>>>
>>>>> datasort catA =
>>>>> | cA_1
>>>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>>>> | cA_2
>>>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>>>> | cA_3
>>>>>
>>>>> datasort catB =
>>>>> | cB_1
>>>>> | cB_2
>>>>> | cB_3
>>>>>
>>>>> datasort sortA =
>>>>> | sA_1 of (catA, catB)
>>>>> | sA_2
>>>>> | sA_3
>>>>>
>>>>> // only sortA is used to define types. Eg,
>>>>> abst@ype typeA(sortA)
>>>>>
>>>>> I ran into a few issues. I arrived at a solution, but I thought it
>>>>> could be cleaner.
>>>>>
>>>>> First, I discovered that I wasn't able to define equalities with
>>>>> datasorts. Eg, {sa:sortA | sa == sA_2}. It would typecheck, but the
>>>>> constraints could not be solved. I suppose this makes sense, considering
>>>>> the definition of ==. Does ATS supply a way to determine equalities on
>>>>> datasorts? Is there another feature that would make this unnecessary?
>>>>>
>>>>> As an alternative, I decided to declare a static predicate, as in the
>>>>> rock-paper-scissors example:
>>>>>
>>>>> stacst isCA1 : sortA -> bool
>>>>>
>>>>> // This works, but becomes quite verbose.
>>>>> praxi isCA1_praxi ():
>>>>> [
>>>>> isCA1(sA_1(cA_1
>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_1)) &&
>>>>> isCA1(sA_1(cA_1
>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_2)) &&
>>>>> isCA1(sA_1(cA_1
>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_3))
>>>>> ] void
>>>>>
>>>>> The verbosity isn't an issue in this example, but becomes pretty
>>>>> unmanageable as the relationships get more complex. I would like to say,
>>>>> "for any catB". I tried using universal and existential quantification,
>>>>> but the constraints would not solve. I would like to avoid passing catB
>>>>> explicitly.
>>>>>
>>>>> Is there a way to reduce it to something like this:
>>>>>
>>>>> // The constraints will not solve:
>>>>> praxi isCA1_praxi ():
>>>>> [ cb: catB |
>>>>> isCA1(sA_1(cA_1
>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cb))
>>>>> ] void
>>>>>
>>>>> Perhaps I am abusing datasorts -- suggestions for other approaches are
>>>>> welcome.
>>>>>
>>>>>
>>>>> --
>>> 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-user...@googlegroups.com.
>>> To post to this group, send email to ats-lan...@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/ms
>>> gid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40go
>>> oglegroups.com
>>> <https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>>
>> --
> 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/82adac20-edf8-4974-ad88-32455de26f16%
> 40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAPPSPLoc2h47U-k1S1Ai3R3gA13%3Dahk3hkwqH0_3UWidBscWHw%40mail.gmail.com.
